refactor(library/algebra): fix theorem names
This commit is contained in:
Johannes Hölzl
Leonardo de Moura
parent
f7ea9a5f64
commit
6d6a00f48b
4 changed files with 57 additions and 57 deletions
library
|
|
@ -276,7 +276,7 @@ end complete_lattice
|
|||
section
|
||||
open eq.ops complete_lattice
|
||||
|
||||
definition complete_lattice_fun [instance] {A B : Type} [complete_lattice B] :
|
||||
definition complete_lattice_fun [instance] (A B : Type) [complete_lattice B] :
|
||||
complete_lattice (A → B) :=
|
||||
⦃ complete_lattice, lattice_fun,
|
||||
Inf := λS x, Inf ((λf, f x) ' S),
|
||||
|
|
@ -308,7 +308,7 @@ definition complete_lattice_Prop [instance] : complete_lattice Prop :=
|
|||
H _ Ht true.intro
|
||||
⦄
|
||||
|
||||
lemma sInter_eq_fun_Inf {A : Type} (S : set (set A)) : ⋂₀ S = @Inf (A → Prop) _ S :=
|
||||
lemma sInter_eq_Inf_fun {A : Type} (S : set (set A)) : ⋂₀ S = @Inf (A → Prop) _ S :=
|
||||
funext (take x,
|
||||
calc
|
||||
(⋂₀ S) x = ∀₀ P ∈ S, P x : rfl
|
||||
|
|
@ -322,19 +322,19 @@ funext (take x,
|
|||
end
|
||||
... = @Inf (A → Prop) _ S x : rfl)
|
||||
|
||||
lemma sUnion_eq_fun_Sup {A : Type} (S : set (set A)) : ⋃₀ S = @Sup (A → Prop) _ S :=
|
||||
lemma sUnion_eq_Sup_fun {A : Type} (S : set (set A)) : ⋃₀ S = @Sup (A → Prop) _ S :=
|
||||
funext (take x,
|
||||
calc
|
||||
(⋃₀ S) x = ∃₀ P ∈ S, P x : rfl
|
||||
... = (∃₀ P ∈ S, P x = true) :
|
||||
begin
|
||||
begin
|
||||
apply bounded_exists_congr,
|
||||
intros,
|
||||
rewrite eq_true
|
||||
end
|
||||
... = @Sup (A → Prop) _ S x : rfl)
|
||||
|
||||
definition complete_lattice_set [instance] {A : Type} : complete_lattice (set A) :=
|
||||
definition complete_lattice_set [instance] (A : Type) : complete_lattice (set A) :=
|
||||
⦃ complete_lattice,
|
||||
le := subset,
|
||||
le_refl := @le_refl (A → Prop) _,
|
||||
|
|
@ -350,10 +350,10 @@ definition complete_lattice_set [instance] {A : Type} : complete_lattice (set A)
|
|||
sup_le := @sup_le (A → Prop) _,
|
||||
Inf := sInter,
|
||||
Sup := sUnion,
|
||||
le_Inf := begin intros X S H, rewrite sInter_eq_fun_Inf, apply (@le_Inf (A → Prop) _), exact H end,
|
||||
Inf_le := begin intros X S H, rewrite sInter_eq_fun_Inf, apply (@Inf_le (A → Prop) _), exact H end,
|
||||
le_Sup := begin intros X S H, rewrite sUnion_eq_fun_Sup, apply (@le_Sup (A → Prop) _), exact H end,
|
||||
Sup_le := begin intros X S H, rewrite sUnion_eq_fun_Sup, apply (@Sup_le (A → Prop) _), exact H end
|
||||
le_Inf := begin intros X S H, rewrite sInter_eq_Inf_fun, apply (@le_Inf (A → Prop) _), exact H end,
|
||||
Inf_le := begin intros X S H, rewrite sInter_eq_Inf_fun, apply (@Inf_le (A → Prop) _), exact H end,
|
||||
le_Sup := begin intros X S H, rewrite sUnion_eq_Sup_fun, apply (@le_Sup (A → Prop) _), exact H end,
|
||||
Sup_le := begin intros X S H, rewrite sUnion_eq_Sup_fun, apply (@Sup_le (A → Prop) _), exact H end
|
||||
⦄
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -27,42 +27,42 @@ definition is_greatest (S : set A) (a : A) := a ∈ S ∧ a ∈ upper_bounds S
|
|||
|
||||
definition monotone (f : A → B) := ∀⦃a b⦄, a ≤ b → f a ≤ f b
|
||||
|
||||
lemma is_least_unique (Ha : is_least S a) (Hb : is_least S a') : a = a' :=
|
||||
lemma eq_of_is_least_of_is_least (Ha : is_least S a) (Hb : is_least S a') : a = a' :=
|
||||
le.antisymm
|
||||
begin apply (and.elim_right Ha), apply (and.elim_left Hb) end
|
||||
begin apply (and.elim_right Hb), apply (and.elim_left Ha) end
|
||||
|
||||
lemma is_least_unique_iff (Ha : is_least S a) : is_least S a' ↔ a = a' :=
|
||||
iff.intro (is_least_unique Ha) begin intro H, cases H, apply Ha end
|
||||
lemma is_least_iff_eq_of_is_least (Ha : is_least S a) : is_least S a' ↔ a = a' :=
|
||||
iff.intro (eq_of_is_least_of_is_least Ha) begin intro H, cases H, apply Ha end
|
||||
|
||||
lemma is_greatest_unique (Ha : is_greatest S a) (Hb : is_greatest S a') : a = a' :=
|
||||
lemma eq_of_is_greatest_of_is_greatest (Ha : is_greatest S a) (Hb : is_greatest S a') : a = a' :=
|
||||
le.antisymm
|
||||
begin apply (and.elim_right Hb), apply (and.elim_left Ha) end
|
||||
begin apply (and.elim_right Ha), apply (and.elim_left Hb) end
|
||||
|
||||
lemma is_greatest_unique_iff (Ha : is_greatest S a) : is_greatest S a' ↔ a = a' :=
|
||||
iff.intro (is_greatest_unique Ha) begin intro H, cases H, apply Ha end
|
||||
lemma is_greatest_iff_eq_of_is_greatest (Ha : is_greatest S a) : is_greatest S a' ↔ a = a' :=
|
||||
iff.intro (eq_of_is_greatest_of_is_greatest Ha) begin intro H, cases H, apply Ha end
|
||||
|
||||
definition is_lub (S : set A) := is_least (upper_bounds S)
|
||||
definition is_glb (S : set A) := is_greatest (lower_bounds S)
|
||||
|
||||
lemma is_lub_unique : is_lub S a → is_lub S a' → a = a' :=
|
||||
!is_least_unique
|
||||
lemma eq_of_is_lub_of_is_lub : is_lub S a → is_lub S a' → a = a' :=
|
||||
!eq_of_is_least_of_is_least
|
||||
|
||||
lemma is_lub_unique_iff : is_lub S a → (is_lub S a' ↔ a = a') :=
|
||||
!is_least_unique_iff
|
||||
lemma is_lub_iff_eq_of_is_lub : is_lub S a → (is_lub S a' ↔ a = a') :=
|
||||
!is_least_iff_eq_of_is_least
|
||||
|
||||
lemma is_glb_unique : is_glb S a → is_glb S a' → a = a' :=
|
||||
!is_greatest_unique
|
||||
lemma eq_of_is_glb_of_is_glb : is_glb S a → is_glb S a' → a = a' :=
|
||||
!eq_of_is_greatest_of_is_greatest
|
||||
|
||||
lemma is_glb_unique_iff : is_glb S a → (is_glb S a' ↔ a = a') :=
|
||||
!is_greatest_unique_iff
|
||||
lemma is_glb_iff_eq_of_is_glb : is_glb S a → (is_glb S a' ↔ a = a') :=
|
||||
!is_greatest_iff_eq_of_is_greatest
|
||||
|
||||
lemma upper_bounds_image (Hf : monotone f) (Ha : a ∈ upper_bounds S) : f a ∈ upper_bounds (f ' S) :=
|
||||
forall_image_implies_forall (take x H, Hf (Ha `x ∈ S`))
|
||||
lemma mem_upper_bounds_image (Hf : monotone f) (Ha : a ∈ upper_bounds S) : f a ∈ upper_bounds (f ' S) :=
|
||||
bounded_forall_image_of_bounded_forall (take x H, Hf (Ha `x ∈ S`))
|
||||
|
||||
lemma lower_bounds_image (Hf : monotone f) (Ha : a ∈ lower_bounds S) : f a ∈ lower_bounds (f ' S) :=
|
||||
forall_image_implies_forall (take x H, Hf (Ha `x ∈ S`))
|
||||
lemma mem_lower_bounds_image (Hf : monotone f) (Ha : a ∈ lower_bounds S) : f a ∈ lower_bounds (f ' S) :=
|
||||
bounded_forall_image_of_bounded_forall (take x H, Hf (Ha `x ∈ S`))
|
||||
|
||||
end order
|
||||
|
||||
|
|
@ -110,30 +110,30 @@ funext (take x, le.antisymm (monotone_u !decreasing_l_u) !increasing_u_l)
|
|||
lemma l_u_l_eq_l : l ∘ u ∘ l = l :=
|
||||
funext (take x, le.antisymm !decreasing_l_u (monotone_l !increasing_u_l))
|
||||
|
||||
lemma u_upper_bounds {S : set A} {b : B} (H : b ∈ upper_bounds (l ' S)) : u b ∈ upper_bounds S :=
|
||||
lemma u_mem_upper_bounds {S : set A} {b : B} (H : b ∈ upper_bounds (l ' S)) : u b ∈ upper_bounds S :=
|
||||
take c, suppose c ∈ S, le_u (H (!mem_image_of_mem `c ∈ S`))
|
||||
|
||||
lemma l_lower_bounds {S : set B} {a : A} (H : a ∈ lower_bounds (u ' S)) : l a ∈ lower_bounds S :=
|
||||
lemma l_mem_lower_bounds {S : set B} {a : A} (H : a ∈ lower_bounds (u ' S)) : l a ∈ lower_bounds S :=
|
||||
take c, suppose c ∈ S, l_le (H (!mem_image_of_mem `c ∈ S`))
|
||||
|
||||
lemma l_preserves_lub {S : set A} {a : A} (H : is_lub S a) : is_lub (l ' S) (l a) :=
|
||||
lemma is_lub_l_image {S : set A} {a : A} (H : is_lub S a) : is_lub (l ' S) (l a) :=
|
||||
and.intro
|
||||
(upper_bounds_image monotone_l (and.elim_left `is_lub S a`))
|
||||
(take b Hb, l_le (and.elim_right `is_lub S a` _ (u_upper_bounds Hb)))
|
||||
(mem_upper_bounds_image monotone_l (and.elim_left `is_lub S a`))
|
||||
(take b Hb, l_le (and.elim_right `is_lub S a` _ (u_mem_upper_bounds Hb)))
|
||||
|
||||
lemma u_preserves_glb {S : set B} {b : B} (H : is_glb S b) : is_glb (u ' S) (u b) :=
|
||||
lemma is_glb_u_image {S : set B} {b : B} (H : is_glb S b) : is_glb (u ' S) (u b) :=
|
||||
and.intro
|
||||
(lower_bounds_image monotone_u (and.elim_left `is_glb S b`))
|
||||
(take a Ha, le_u (and.elim_right `is_glb S b` _ (l_lower_bounds Ha)))
|
||||
(mem_lower_bounds_image monotone_u (and.elim_left `is_glb S b`))
|
||||
(take a Ha, le_u (and.elim_right `is_glb S b` _ (l_mem_lower_bounds Ha)))
|
||||
|
||||
lemma l_is_glb {a : A} : is_glb { b | a ≤ u b } (l a) :=
|
||||
lemma is_glb_l {a : A} : is_glb { b | a ≤ u b } (l a) :=
|
||||
begin
|
||||
apply and.intro,
|
||||
{ intro b, apply l_le },
|
||||
{ intro b H, apply H, apply increasing_u_l }
|
||||
end
|
||||
|
||||
lemma u_is_lub {b : B} : is_lub { a | l a ≤ b } (u b) :=
|
||||
lemma is_lub_u {b : B} : is_lub { a | l a ≤ b } (u b) :=
|
||||
begin
|
||||
apply and.intro,
|
||||
{ intro a, apply le_u },
|
||||
|
|
@ -144,21 +144,21 @@ end
|
|||
|
||||
/- Constructing Galois connections -/
|
||||
|
||||
lemma id {A : Type} [weak_order A] : @galois_connection A A _ _ id id :=
|
||||
protected lemma id {A : Type} [weak_order A] : @galois_connection A A _ _ id id :=
|
||||
take a b, iff.intro (λx, x) (λx, x)
|
||||
|
||||
lemma dual {A B : Type} [woA : weak_order A] [woB : weak_order B]
|
||||
protected lemma dual {A B : Type} [woA : weak_order A] [woB : weak_order B]
|
||||
(l : A → B) (u : B → A) (gc : galois_connection l u) :
|
||||
@galois_connection B A (weak_order_dual woB) (weak_order_dual woA) u l :=
|
||||
take a b,
|
||||
begin
|
||||
apply iff.symm,
|
||||
rewrite dual,
|
||||
rewrite dual,
|
||||
rewrite le_dual_eq_le,
|
||||
rewrite le_dual_eq_le,
|
||||
exact gc,
|
||||
end
|
||||
|
||||
lemma compose {A B C : Type} [weak_order A] [weak_order B] [weak_order C]
|
||||
protected lemma compose {A B C : Type} [weak_order A] [weak_order B] [weak_order C]
|
||||
(l1 : A → B) (u1 : B → A) (l2 : B → C) (u2 : C → B)
|
||||
(gc1 : galois_connection l1 u1) (gc2 : galois_connection l2 u2) :
|
||||
galois_connection (l2 ∘ l1) (u1 ∘ u2) :=
|
||||
|
|
@ -167,10 +167,10 @@ by intros; rewrite gc2; rewrite gc1
|
|||
section
|
||||
variables {A B : Type} {f : A → B}
|
||||
|
||||
lemma image_preimage : galois_connection (image f) (preimage f) :=
|
||||
protected lemma image_preimage : galois_connection (image f) (preimage f) :=
|
||||
@image_subset_iff A B f
|
||||
|
||||
lemma preimage_kern_image : galois_connection (preimage f) (kern_image f) :=
|
||||
protected lemma preimage_kern_image : galois_connection (preimage f) (kern_image f) :=
|
||||
begin
|
||||
intros X Y, apply iff.intro, all_goals (intro H x Hx),
|
||||
{ intro x' eq, apply H, cases eq, exact Hx },
|
||||
|
|
@ -191,12 +191,12 @@ variables {A : Type} (S : set A) {a b : A} [complete_lattice A]
|
|||
lemma is_lub_sup : is_lub '{a, b} (sup a b) :=
|
||||
and.intro
|
||||
begin
|
||||
xrewrite [+forall_insert_iff, bounded_forall_empty_iff, and_true],
|
||||
xrewrite [+bounded_forall_insert_iff, bounded_forall_empty_iff, and_true],
|
||||
exact (and.intro !le_sup_left !le_sup_right)
|
||||
end
|
||||
begin
|
||||
intro x Hx,
|
||||
xrewrite [+forall_insert_iff at Hx, bounded_forall_empty_iff at Hx, and_true at Hx],
|
||||
xrewrite [+bounded_forall_insert_iff at Hx, bounded_forall_empty_iff at Hx, and_true at Hx],
|
||||
apply sup_le,
|
||||
apply (and.elim_left Hx),
|
||||
apply (and.elim_right Hx),
|
||||
|
|
@ -205,13 +205,13 @@ and.intro
|
|||
lemma is_lub_Sup : is_lub S (⨆S) :=
|
||||
and.intro (take x, le_Sup) (take x, Sup_le)
|
||||
|
||||
lemma is_lub_Sup_iff {a : A} : is_lub S a ↔ (⨆S) = a :=
|
||||
!is_lub_unique_iff !is_lub_Sup
|
||||
lemma is_lub_iff_Sup_eq {a : A} : is_lub S a ↔ (⨆S) = a :=
|
||||
!is_lub_iff_eq_of_is_lub !is_lub_Sup
|
||||
|
||||
lemma is_glb_Inf : is_glb S (⨅S) :=
|
||||
and.intro (take a, Inf_le) (take a, le_Inf)
|
||||
|
||||
lemma is_glb_Inf_iff : is_glb S a ↔ (⨅S) = a :=
|
||||
!is_glb_unique_iff !is_glb_Inf
|
||||
lemma is_glb_iff_Inf_eq : is_glb S a ↔ (⨅S) = a :=
|
||||
!is_glb_iff_eq_of_is_glb !is_glb_Inf
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -460,7 +460,7 @@ definition weak_order_dual {A : Type} (wo : weak_order A) : weak_order A :=
|
|||
le_trans := take a b c `b ≤ a` `c ≤ b`, le.trans `c ≤ b` `b ≤ a`,
|
||||
le_antisymm := take a b `b ≤ a` `a ≤ b`, le.antisymm `a ≤ b` `b ≤ a` ⦄
|
||||
|
||||
lemma dual {A : Type} (wo : weak_order A) (a b : A) :
|
||||
lemma le_dual_eq_le {A : Type} (wo : weak_order A) (a b : A) :
|
||||
@le _ (@weak_order.to_has_le _ (weak_order_dual wo)) a b =
|
||||
@le _ (@weak_order.to_has_le _ wo) b a :=
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -339,7 +339,7 @@ theorem forall_of_forall_insert {P : X → Prop} {a : X} {s : set X}
|
|||
∀ x, x ∈ s → P x :=
|
||||
λ x xs, H x (!mem_insert_of_mem xs)
|
||||
|
||||
lemma forall_insert_iff {P : X → Prop} {a : X} {s : set X} :
|
||||
lemma bounded_forall_insert_iff {P : X → Prop} {a : X} {s : set X} :
|
||||
(∀₀x ∈ insert a s, P x) ↔ P a ∧ (∀₀x ∈ s, P x) :=
|
||||
begin
|
||||
apply iff.intro, all_goals (intro H),
|
||||
|
|
@ -585,8 +585,8 @@ theorem complement_complement_image (S : set (set X)) :
|
|||
complement ' (complement ' S) = S :=
|
||||
by rewrite [-image_compose, complement_compose_complement, image_id]
|
||||
|
||||
lemma forall_image_implies_forall {f : X → Y} {S : set X} {P : Y → Prop} (H : ∀₀ x ∈ S, P (f x)) :
|
||||
∀₀ y ∈ f ' S, P y :=
|
||||
lemma bounded_forall_image_of_bounded_forall {f : X → Y} {S : set X} {P : Y → Prop}
|
||||
(H : ∀₀ x ∈ S, P (f x)) : ∀₀ y ∈ f ' S, P y :=
|
||||
begin
|
||||
intro x' Hx;
|
||||
cases Hx with x Hx;
|
||||
|
|
@ -596,9 +596,9 @@ begin
|
|||
assumption
|
||||
end
|
||||
|
||||
lemma forall_image_iff {f : X → Y} {S : set X} {P : Y → Prop} :
|
||||
lemma bounded_forall_image_iff {f : X → Y} {S : set X} {P : Y → Prop} :
|
||||
(∀₀ y ∈ f ' S, P y) ↔ (∀₀ x ∈ S, P (f x)) :=
|
||||
iff.intro (take H x Hx, H _ (!mem_image_of_mem `x ∈ S`)) forall_image_implies_forall
|
||||
iff.intro (take H x Hx, H _ (!mem_image_of_mem `x ∈ S`)) bounded_forall_image_of_bounded_forall
|
||||
|
||||
lemma image_insert_eq {f : X → Y} {a : X} {S : set X} :
|
||||
f ' insert a S = insert (f a) (f ' S) :=
|
||||
|
|
@ -622,7 +622,7 @@ definition preimage {A B:Type} (f : A → B) (Y : set B) : set A := { x | f x
|
|||
|
||||
lemma image_subset_iff {A B : Type} {f : A → B} {X : set A} {Y : set B} :
|
||||
f ' X ⊆ Y ↔ X ⊆ preimage f Y :=
|
||||
@forall_image_iff A B f X Y
|
||||
@bounded_forall_image_iff A B f X Y
|
||||
|
||||
/- collections of disjoint sets -/
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue