From 6d6a00f48b3de007da706799ed9b2a71b80680e7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= Date: Wed, 6 Jan 2016 16:13:39 +0100 Subject: [PATCH] refactor(library/algebra): fix theorem names --- library/algebra/complete_lattice.lean | 18 +++--- library/algebra/galois_connection.lean | 82 +++++++++++++------------- library/algebra/order.lean | 2 +- library/data/set/basic.lean | 12 ++-- 4 files changed, 57 insertions(+), 57 deletions(-) diff --git a/library/algebra/complete_lattice.lean b/library/algebra/complete_lattice.lean index 4b4120452..8c8138047 100644 --- a/library/algebra/complete_lattice.lean +++ b/library/algebra/complete_lattice.lean @@ -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 diff --git a/library/algebra/galois_connection.lean b/library/algebra/galois_connection.lean index 16e585271..f4628303d 100644 --- a/library/algebra/galois_connection.lean +++ b/library/algebra/galois_connection.lean @@ -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 diff --git a/library/algebra/order.lean b/library/algebra/order.lean index 8161ba764..90d82c15e 100644 --- a/library/algebra/order.lean +++ b/library/algebra/order.lean @@ -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 diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean index a6f8669e7..7162596ff 100644 --- a/library/data/set/basic.lean +++ b/library/data/set/basic.lean @@ -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 -/