From 518a77587a12ff98d07b95303924a5137025593c Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Tue, 16 Feb 2016 13:56:01 -0500 Subject: [PATCH] refactor(library/data/{set,finset},library/*): use compl for set and finset complement --- library/data/finset/comb.lean | 22 ++-- library/data/hf.lean | 6 +- library/data/set/basic.lean | 102 +++++++++--------- library/theories/analysis/metric_space.lean | 12 +-- library/theories/analysis/real_limit.lean | 2 +- library/theories/group_theory/finsubg.lean | 4 +- library/theories/group_theory/subgroup.lean | 4 +- .../measure_theory/sigma_algebra.lean | 24 ++--- library/theories/topology/basic.lean | 30 +++--- 9 files changed, 103 insertions(+), 103 deletions(-) diff --git a/library/data/finset/comb.lean b/library/data/finset/comb.lean index 595f6899eb..bc7b16df4c 100644 --- a/library/data/finset/comb.lean +++ b/library/data/finset/comb.lean @@ -77,7 +77,7 @@ ext (take y, iff.intro (suppose y ∈ image f s, show y ∈ image f (insert a s), from mem_image_of_mem_image_of_subset this !subset_insert))) -lemma image_compose {C : Type} [deceqC : decidable_eq C] {f : B → C} {g : A → B} {s : finset A} : +lemma image_comp {C : Type} [deceqC : decidable_eq C] {f : B → C} {g : A → B} {s : finset A} : image (f∘g) s = image f (image g s) := ext (take z, iff.intro (suppose z ∈ image (f∘g) s, @@ -216,27 +216,27 @@ section complement variables {A : Type} [deceqA : decidable_eq A] [h : fintype A] include deceqA h -definition complement (s : finset A) : finset A := univ \ s -prefix [priority finset.prio] - := complement +definition compl (s : finset A) : finset A := univ \ s +prefix [priority finset.prio] - := compl -theorem mem_complement {s : finset A} {x : A} (H : x ∉ s) : x ∈ -s := +theorem mem_compl {s : finset A} {x : A} (H : x ∉ s) : x ∈ -s := mem_diff !mem_univ H -theorem not_mem_of_mem_complement {s : finset A} {x : A} (H : x ∈ -s) : x ∉ s := +theorem not_mem_of_mem_compl {s : finset A} {x : A} (H : x ∈ -s) : x ∉ s := not_mem_of_mem_diff H -theorem mem_complement_iff (s : finset A) (x : A) : x ∈ -s ↔ x ∉ s := -iff.intro not_mem_of_mem_complement mem_complement +theorem mem_compl_iff (s : finset A) (x : A) : x ∈ -s ↔ x ∉ s := +iff.intro not_mem_of_mem_compl mem_compl section open classical - theorem union_eq_comp_comp_inter_comp (s t : finset A) : s ∪ t = -(-s ∩ -t) := - ext (take x, by rewrite [mem_union_iff, mem_complement_iff, mem_inter_iff, *mem_complement_iff, + theorem union_eq_compl_compl_inter_compl (s t : finset A) : s ∪ t = -(-s ∩ -t) := + ext (take x, by rewrite [mem_union_iff, mem_compl_iff, mem_inter_iff, *mem_compl_iff, or_iff_not_and_not]) - theorem inter_eq_comp_comp_union_comp (s t : finset A) : s ∩ t = -(-s ∪ -t) := - ext (take x, by rewrite [mem_inter_iff, mem_complement_iff, mem_union_iff, *mem_complement_iff, + theorem inter_eq_compl_compl_union_compl (s t : finset A) : s ∩ t = -(-s ∪ -t) := + ext (take x, by rewrite [mem_inter_iff, mem_compl_iff, mem_union_iff, *mem_compl_iff, and_iff_not_or_not]) end diff --git a/library/data/hf.lean b/library/data/hf.lean index 13334fe487..d75eb373b3 100644 --- a/library/data/hf.lean +++ b/library/data/hf.lean @@ -433,8 +433,8 @@ theorem image_insert (f : hf → hf) (s : hf) (a : hf) : image f (insert a s) = begin unfold [image, insert], rewrite [*to_finset_of_finset, finset.image_insert] end open function -lemma image_compose {f : hf → hf} {g : hf → hf} {s : hf} : image (f∘g) s = image f (image g s) := -begin unfold image, rewrite [*to_finset_of_finset, finset.image_compose] end +lemma image_comp {f : hf → hf} {g : hf → hf} {s : hf} : image (f∘g) s = image f (image g s) := +begin unfold image, rewrite [*to_finset_of_finset, finset.image_comp] end lemma image_subset {a b : hf} (f : hf → hf) : a ⊆ b → image f a ⊆ image f b := begin unfold [subset, image], intro h, rewrite *to_finset_of_finset, apply finset.image_subset f h end @@ -455,7 +455,7 @@ theorem powerset_insert {a : hf} {s : hf} : a ∉ s → 𝒫 (insert a s) = 𝒫 begin unfold [mem, powerset, insert, union, image], rewrite [*to_finset_of_finset], intro h, have (λ (x : finset hf), of_finset (finset.insert a x)) = (λ (x : finset hf), of_finset (finset.insert a (to_finset (of_finset x)))), from funext (λ x, by rewrite to_finset_of_finset), - rewrite [finset.powerset_insert h, finset.image_union, -*finset.image_compose,↑compose,this] + rewrite [finset.powerset_insert h, finset.image_union, -*finset.image_comp, ↑compose, this] end theorem mem_powerset_iff_subset (s : hf) : ∀ x : hf, x ∈ 𝒫 s ↔ x ⊆ s := diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean index 761516cbae..23ad7f770b 100644 --- a/library/data/set/basic.lean +++ b/library/data/set/basic.lean @@ -440,19 +440,19 @@ theorem forall_not_of_sep_empty {s : set X} {P : X → Prop} (H : {x ∈ s | P x /- complement -/ -definition complement (s : set X) : set X := {x | x ∉ s} -prefix `-` := complement +definition compl (s : set X) : set X := {x | x ∉ s} +prefix `-` := compl -theorem mem_comp {s : set X} {x : X} (H : x ∉ s) : x ∈ -s := H +theorem mem_compl {s : set X} {x : X} (H : x ∉ s) : x ∈ -s := H -theorem not_mem_of_mem_comp {s : set X} {x : X} (H : x ∈ -s) : x ∉ s := H +theorem not_mem_of_mem_compl {s : set X} {x : X} (H : x ∈ -s) : x ∉ s := H -theorem mem_comp_iff (s : set X) (x : X) : x ∈ -s ↔ x ∉ s := !iff.refl +theorem mem_compl_iff (s : set X) (x : X) : x ∈ -s ↔ x ∉ s := !iff.refl -theorem inter_comp_self (s : set X) : s ∩ -s = ∅ := +theorem inter_compl_self (s : set X) : s ∩ -s = ∅ := ext (take x, !and_not_self_iff) -theorem comp_inter_self (s : set X) : -s ∩ s = ∅ := +theorem compl_inter_self (s : set X) : -s ∩ s = ∅ := ext (take x, !not_and_self_iff) /- some classical identities -/ @@ -460,36 +460,36 @@ ext (take x, !not_and_self_iff) section open classical - theorem comp_empty : -(∅ : set X) = univ := + theorem compl_empty : -(∅ : set X) = univ := ext (take x, iff.intro (assume H, trivial) (assume H, not_false)) - theorem comp_union (s t : set X) : -(s ∪ t) = -s ∩ -t := + theorem compl_union (s t : set X) : -(s ∪ t) = -s ∩ -t := ext (take x, !not_or_iff_not_and_not) - theorem comp_comp (s : set X) : -(-s) = s := + theorem compl_compl (s : set X) : -(-s) = s := ext (take x, !not_not_iff) - theorem comp_inter (s t : set X) : -(s ∩ t) = -s ∪ -t := + theorem compl_inter (s t : set X) : -(s ∩ t) = -s ∪ -t := ext (take x, !not_and_iff_not_or_not) - theorem comp_univ : -(univ : set X) = ∅ := - by rewrite [-comp_empty, comp_comp] + theorem compl_univ : -(univ : set X) = ∅ := + by rewrite [-compl_empty, compl_compl] - theorem union_eq_comp_comp_inter_comp (s t : set X) : s ∪ t = -(-s ∩ -t) := + theorem union_eq_compl_compl_inter_compl (s t : set X) : s ∪ t = -(-s ∩ -t) := ext (take x, !or_iff_not_and_not) - theorem inter_eq_comp_comp_union_comp (s t : set X) : s ∩ t = -(-s ∪ -t) := + theorem inter_eq_compl_compl_union_compl (s t : set X) : s ∩ t = -(-s ∪ -t) := ext (take x, !and_iff_not_or_not) - theorem union_comp_self (s : set X) : s ∪ -s = univ := + theorem union_compl_self (s : set X) : s ∪ -s = univ := ext (take x, !or_not_self_iff) - theorem comp_union_self (s : set X) : -s ∪ s = univ := + theorem compl_union_self (s : set X) : -s ∪ s = univ := ext (take x, !not_or_self_iff) - theorem complement_compose_complement : - #function complement ∘ complement = @id (set X) := - funext (λ s, comp_comp s) + theorem compl_comp_compl : + #function compl ∘ compl = @id (set X) := + funext (λ s, compl_compl s) end /- set difference -/ @@ -522,7 +522,7 @@ ext (take x, iff.intro theorem diff_subset (s t : set X) : s \ t ⊆ s := inter_subset_left s _ -theorem comp_eq_univ_diff (s : set X) : -s = univ \ s := +theorem compl_eq_univ_diff (s : set X) : -s = univ \ s := ext (take x, iff.intro (assume H, and.intro trivial H) (assume H, and.right H)) /- powerset -/ @@ -569,7 +569,7 @@ exists.intro x (and.intro H1 H2) theorem mem_image_of_mem (f : X → Y) {x : X} {a : set X} (H : x ∈ a) : f x ∈ image f a := mem_image H rfl -lemma image_compose (f : Y → Z) (g : X → Y) (a : set X) : (f ∘ g) ' a = f ' (g ' a) := +lemma image_comp (f : Y → Z) (g : X → Y) (a : set X) : (f ∘ g) ' a = f ' (g ' a) := ext (take z, iff.intro (assume Hz : z ∈ (f ∘ g) ' a, @@ -609,15 +609,15 @@ eq_empty_of_forall_not_mem obtain x [(H : x ∈ empty) H'], from this, H) -theorem mem_image_complement (t : set X) (S : set (set X)) : - t ∈ complement ' S ↔ -t ∈ S := +theorem mem_image_compl (t : set X) (S : set (set X)) : + t ∈ compl ' S ↔ -t ∈ S := iff.intro - (suppose t ∈ complement ' S, + (suppose t ∈ compl ' S, obtain t' [(Ht' : t' ∈ S) (Ht : -t' = t)], from this, - show -t ∈ S, by rewrite [-Ht, comp_comp]; exact Ht') + show -t ∈ S, by rewrite [-Ht, compl_compl]; exact Ht') (suppose -t ∈ S, - have -(-t) ∈ complement 'S, from mem_image_of_mem complement this, - show t ∈ complement 'S, from comp_comp t ▸ this) + have -(-t) ∈ compl 'S, from mem_image_of_mem compl this, + show t ∈ compl 'S, from compl_compl t ▸ this) theorem image_id (s : set X) : id ' s = s := ext (take x, iff.intro @@ -626,9 +626,9 @@ ext (take x, iff.intro show x ∈ s, by rewrite [-x'eq]; apply Hx') (suppose x ∈ s, mem_image_of_mem id this)) -theorem complement_complement_image (S : set (set X)) : - complement ' (complement ' S) = S := -by rewrite [-image_compose, complement_compose_complement, image_id] +theorem compl_compl_image (S : set (set X)) : + compl ' (compl ' S) = S := +by rewrite [-image_comp, compl_comp_compl, image_id] 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 := @@ -791,32 +791,32 @@ theorem sInter_insert (s : set X) (T : set (set X)) : ⋂₀ (insert s T) = s ∩ ⋂₀ T := by rewrite [insert_eq, sInter_union, sInter_singleton] -theorem comp_sUnion (S : set (set X)) : - - ⋃₀ S = ⋂₀ (complement ' S) := +theorem compl_sUnion (S : set (set X)) : + - ⋃₀ S = ⋂₀ (compl ' S) := ext (take x, iff.intro (assume H : x ∈ -(⋃₀ S), - take t, suppose t ∈ complement ' S, + take t, suppose t ∈ compl ' S, obtain t' [(Ht' : t' ∈ S) (Ht : -t' = t)], from this, have x ∈ -t', from suppose x ∈ t', H (mem_sUnion this Ht'), show x ∈ t, using this, by rewrite -Ht; apply this) - (assume H : x ∈ ⋂₀ (complement ' S), + (assume H : x ∈ ⋂₀ (compl ' S), suppose x ∈ ⋃₀ S, obtain t [(tS : t ∈ S) (xt : x ∈ t)], from this, - have -t ∈ complement ' S, from mem_image_of_mem complement tS, + have -t ∈ compl ' S, from mem_image_of_mem compl tS, have x ∈ -t, from H this, show false, proof this xt qed)) -theorem sUnion_eq_comp_sInter_comp (S : set (set X)) : - ⋃₀ S = - ⋂₀ (complement ' S) := -by rewrite [-comp_comp, comp_sUnion] +theorem sUnion_eq_compl_sInter_compl (S : set (set X)) : + ⋃₀ S = - ⋂₀ (compl ' S) := +by rewrite [-compl_compl, compl_sUnion] -theorem comp_sInter (S : set (set X)) : - - ⋂₀ S = ⋃₀ (complement ' S) := -by rewrite [sUnion_eq_comp_sInter_comp, complement_complement_image] +theorem compl_sInter (S : set (set X)) : + - ⋂₀ S = ⋃₀ (compl ' S) := +by rewrite [sUnion_eq_compl_sInter_compl, compl_compl_image] -theorem sInter_eq_comp_sUnion_comp (S : set (set X)) : - ⋂₀ S = -(⋃₀ (complement ' S)) := -by rewrite [-comp_comp, comp_sInter] +theorem sInter_eq_comp_sUnion_compl (S : set (set X)) : + ⋂₀ S = -(⋃₀ (compl ' S)) := +by rewrite [-compl_compl, compl_sInter] theorem inter_sUnion_nonempty_of_inter_nonempty {s t : set X} {S : set (set X)} (Hs : t ∈ S) (Hne : s ∩ t ≠ ∅) : s ∩ ⋃₀ S ≠ ∅ := @@ -863,17 +863,17 @@ ext (take x, iff.intro have s i ∈ s ' univ, from mem_image_of_mem s trivial, show x ∈ s i, from H this)) -theorem comp_Union {X I : Type} (s : I → set X) : - (⋃ i, s i) = (⋂ i, - s i) := -by rewrite [Union_eq_sUnion_image, comp_sUnion, -image_compose, -Inter_eq_sInter_image] +theorem compl_Union {X I : Type} (s : I → set X) : - (⋃ i, s i) = (⋂ i, - s i) := +by rewrite [Union_eq_sUnion_image, compl_sUnion, -image_comp, -Inter_eq_sInter_image] -theorem comp_Inter {X I : Type} (s : I → set X) : -(⋂ i, s i) = (⋃ i, - s i) := -by rewrite [Inter_eq_sInter_image, comp_sInter, -image_compose, -Union_eq_sUnion_image] +theorem compl_Inter {X I : Type} (s : I → set X) : -(⋂ i, s i) = (⋃ i, - s i) := +by rewrite [Inter_eq_sInter_image, compl_sInter, -image_comp, -Union_eq_sUnion_image] theorem Union_eq_comp_Inter_comp {X I : Type} (s : I → set X) : (⋃ i, s i) = - (⋂ i, - s i) := -by rewrite [-comp_comp, comp_Union] +by rewrite [-compl_compl, compl_Union] theorem Inter_eq_comp_Union_comp {X I : Type} (s : I → set X) : (⋂ i, s i) = - (⋃ i, -s i) := -by rewrite [-comp_comp, comp_Inter] +by rewrite [-compl_compl, compl_Inter] lemma inter_distrib_Union_left {X I : Type} (s : I → set X) (a : set X) : a ∩ (⋃ i, s i) = ⋃ i, a ∩ s i := diff --git a/library/theories/analysis/metric_space.lean b/library/theories/analysis/metric_space.lean index 7c42303b83..3b5be5b4c9 100644 --- a/library/theories/analysis/metric_space.lean +++ b/library/theories/analysis/metric_space.lean @@ -456,19 +456,19 @@ theorem mem_open_ball (x : V) {ε : ℝ} (H : ε > 0) : x ∈ open_ball x ε := definition closed_ball (x : V) (ε : ℝ) := {y ∈ univ | dist x y ≤ ε} -theorem closed_ball_eq_comp (x : V) (ε : ℝ) : closed_ball x ε = -{y ∈ univ | dist x y > ε} := +theorem closed_ball_eq_compl (x : V) (ε : ℝ) : closed_ball x ε = -{y ∈ univ | dist x y > ε} := begin apply ext, intro y, apply iff.intro, intro Hx, - apply mem_comp, + apply mem_compl, intro Hxmem, cases Hxmem with _ Hgt, cases Hx with _ Hle, apply not_le_of_gt Hgt Hle, intro Hx, - note Hx' := not_mem_of_mem_comp Hx, + note Hx' := not_mem_of_mem_compl Hx, split, apply mem_univ, apply le_of_not_gt, @@ -497,9 +497,9 @@ theorem open_ball_open (x : V) (ε : ℝ) : Open (open_ball x ε) := theorem closed_ball_closed (x : V) {ε : ℝ} (H : ε > 0) : closed (closed_ball x ε) := begin - apply iff.mpr !closed_iff_Open_comp, - rewrite closed_ball_eq_comp, - rewrite comp_comp, + apply iff.mpr !closed_iff_Open_compl, + rewrite closed_ball_eq_compl, + rewrite compl_compl, apply Open_of_forall_exists_Open_nbhd, intro y Hy, cases Hy with _ Hxy, diff --git a/library/theories/analysis/real_limit.lean b/library/theories/analysis/real_limit.lean index 323e0c3279..28fb9800d9 100644 --- a/library/theories/analysis/real_limit.lean +++ b/library/theories/analysis/real_limit.lean @@ -503,7 +503,7 @@ have H₂ : ∀ x, x ∈ X ' univ → b ≤ x, from show b ≤ x, by rewrite -Hi₂; apply Hb i), have H₃ : {x : ℝ | -x ∈ X ' univ} = {x : ℝ | x ∈ (λ n, -X n) ' univ}, from calc {x : ℝ | -x ∈ X ' univ} = (λ y, -y) ' (X ' univ) : by rewrite image_neg_eq - ... = {x : ℝ | x ∈ (λ n, -X n) ' univ} : image_compose, + ... = {x : ℝ | x ∈ (λ n, -X n) ' univ} : image_comp, have H₄ : ∀ i, - X i ≤ - b, from take i, neg_le_neg (Hb i), begin+ -- need krewrite here diff --git a/library/theories/group_theory/finsubg.lean b/library/theories/group_theory/finsubg.lean index 04b9810699..51d1d74c3f 100644 --- a/library/theories/group_theory/finsubg.lean +++ b/library/theories/group_theory/finsubg.lean @@ -85,7 +85,7 @@ funext take c, calc a*(c*b) = (a*c)*b : mul.assoc lemma fin_lrcoset_comm {a b : A} : fin_lcoset (fin_rcoset H b) a = fin_rcoset (fin_lcoset H a) b := -by esimp [fin_lcoset, fin_rcoset]; rewrite [-*image_compose, lmul_rmul] +by esimp [fin_lcoset, fin_rcoset]; rewrite [-*image_comp, lmul_rmul] lemma inv_mem_fin_inv {a : A} : a ∈ H → a⁻¹ ∈ fin_inv H := assume Pin, mem_image Pin rfl @@ -135,7 +135,7 @@ lemma finsubg_inv_lcoset_eq_rcoset {a : A} : fin_inv (fin_lcoset H a) = fin_rcoset H a⁻¹ := begin esimp [fin_inv, fin_lcoset, fin_rcoset], - rewrite [-image_compose], + rewrite [-image_comp], apply ext, intro b, rewrite [*mem_image_iff, ↑compose, ↑lmul_by, ↑rmul_by], apply iff.intro, diff --git a/library/theories/group_theory/subgroup.lean b/library/theories/group_theory/subgroup.lean index c4cc018a48..86875f5fe0 100644 --- a/library/theories/group_theory/subgroup.lean +++ b/library/theories/group_theory/subgroup.lean @@ -28,10 +28,10 @@ lemma rmul_compose : ∀ (a b : A), (rmul a) ∘ (rmul b) = rmul (b*a) := funext (assume x, by rewrite [↑function.compose, ↑rmul, mul.assoc]) lemma lcompose a b (S : set A) : l a (l b S) = l (a*b) S := - calc (lmul a) ' ((lmul b) ' S) = ((lmul a) ∘ (lmul b)) ' S : image_compose + calc (lmul a) ' ((lmul b) ' S) = ((lmul a) ∘ (lmul b)) ' S : image_comp ... = lmul (a*b) ' S : lmul_compose lemma rcompose a b (S : set A) : r a (r b S) = r (b*a) S := - calc (rmul a) ' ((rmul b) ' S) = ((rmul a) ∘ (rmul b)) ' S : image_compose + calc (rmul a) ' ((rmul b) ' S) = ((rmul a) ∘ (rmul b)) ' S : image_comp ... = rmul (b*a) ' S : rmul_compose lemma l_sub a (S H : set A) : S ⊆ H → (l a S) ⊆ (l a H) := image_subset (lmul a) definition l_same S (a b : A) := l a S = l b S diff --git a/library/theories/measure_theory/sigma_algebra.lean b/library/theories/measure_theory/sigma_algebra.lean index ab5e617518..1c23d8cb84 100644 --- a/library/theories/measure_theory/sigma_algebra.lean +++ b/library/theories/measure_theory/sigma_algebra.lean @@ -26,14 +26,14 @@ definition measurable (t : set X) : Prop := t ∈ sets X theorem measurable_univ : measurable (@univ X) := univ_mem_sets X -theorem measurable_comp {s : set X} (H : measurable s) : measurable (-s) := +theorem measurable_compl {s : set X} (H : measurable s) : measurable (-s) := comp_mem_sets H -theorem measurable_of_measurable_comp {s : set X} (H : measurable (-s)) : measurable s := -!comp_comp ▸ measurable_comp H +theorem measurable_of_measurable_compl {s : set X} (H : measurable (-s)) : measurable s := +!compl_compl ▸ measurable_compl H theorem measurable_empty : measurable (∅ : set X) := -comp_univ ▸ measurable_comp measurable_univ +compl_univ ▸ measurable_compl measurable_univ theorem measurable_cUnion {s : ℕ → set X} (H : ∀ i, measurable (s i)) : measurable (⋃ i, s i) := @@ -41,8 +41,8 @@ cUnion_mem_sets H theorem measurable_cInter {s : ℕ → set X} (H : ∀ i, measurable (s i)) : measurable (⋂ i, s i) := -have ∀ i, measurable (-(s i)), from take i, measurable_comp (H i), -have measurable (-(⋃ i, -(s i))), from measurable_comp (measurable_cUnion this), +have ∀ i, measurable (-(s i)), from take i, measurable_compl (H i), +have measurable (-(⋃ i, -(s i))), from measurable_compl (measurable_cUnion this), show measurable (⋂ i, s i), using this, by rewrite Inter_eq_comp_Union_comp; apply this theorem measurable_union {s t : set X} (Hs : measurable s) (Ht : measurable t) : @@ -57,7 +57,7 @@ show measurable (s ∩ t), using this, by rewrite -Inter_bin_ext; exact measurab theorem measurable_diff {s t : set X} (Hs : measurable s) (Ht : measurable t) : measurable (s \ t) := -measurable_inter Hs (measurable_comp Ht) +measurable_inter Hs (measurable_compl Ht) theorem measurable_insert {x : X} {s : set X} (Hx : measurable '{x}) (Hs : measurable s) : measurable (insert x s) := @@ -100,7 +100,7 @@ begin induction Hs with s sG s Hs ssX s Hs sisX, {exact H sG}, {exact measurable_univ}, - {exact measurable_comp ssX}, + {exact measurable_compl ssX}, exact measurable_cUnion sisX end @@ -135,8 +135,8 @@ protected definition inf (M N : sigma_algebra X) : sigma_algebra X := sets := @sets X M ∩ @sets X N, univ_mem_sets := abstract and.intro (@measurable_univ X M) (@measurable_univ X N) end, comp_mem_sets := abstract take s, assume Hs, and.intro - (@measurable_comp X M s (and.elim_left Hs)) - (@measurable_comp X N s (and.elim_right Hs)) end, + (@measurable_compl X M s (and.elim_left Hs)) + (@measurable_compl X N s (and.elim_right Hs)) end, cUnion_mem_sets := abstract take s, assume Hs, and.intro (@measurable_cUnion X M s (λ i, and.elim_left (Hs i))) (@measurable_cUnion X N s (λ i, and.elim_right (Hs i))) end⦄ @@ -156,7 +156,7 @@ protected definition Inf (MS : set (sigma_algebra X)) : sigma_algebra X := sets := ⋂ M ∈ MS, @sets _ M, univ_mem_sets := abstract take M, assume HM, @measurable_univ X M end, comp_mem_sets := abstract take s, assume Hs, take M, assume HM, - measurable_comp (Hs M HM) end, + measurable_compl (Hs M HM) end, cUnion_mem_sets := abstract take s, assume Hs, take M, assume HM, measurable_cUnion (λ i, Hs i M HM) end ⦄ @@ -242,7 +242,7 @@ section theorem borel_of_closed {s : set X} (H : closed s) : borel s := have borel (-s), from borel_of_open H, - @measurable_of_measurable_comp _ (borel_algebra X) _ this + @measurable_of_measurable_compl _ (borel_algebra X) _ this end end measure_theory diff --git a/library/theories/topology/basic.lean b/library/theories/topology/basic.lean index 5e29c7346d..989339622a 100644 --- a/library/theories/topology/basic.lean +++ b/library/theories/topology/basic.lean @@ -63,46 +63,46 @@ end definition closed [reducible] (s : set X) : Prop := Open (-s) -theorem closed_iff_Open_comp (s : set X) : closed s ↔ Open (-s) := !iff.refl +theorem closed_iff_Open_compl (s : set X) : closed s ↔ Open (-s) := !iff.refl -theorem Open_iff_closed_comp (s : set X) : Open s ↔ closed (-s) := -by rewrite [closed_iff_Open_comp, comp_comp] +theorem Open_iff_closed_compl (s : set X) : Open s ↔ closed (-s) := +by rewrite [closed_iff_Open_compl, compl_compl] -theorem closed_comp {s : set X} (H : Open s) : closed (-s) := -by rewrite [-Open_iff_closed_comp]; apply H +theorem closed_compl {s : set X} (H : Open s) : closed (-s) := +by rewrite [-Open_iff_closed_compl]; apply H theorem closed_empty : closed (∅ : set X) := -by rewrite [↑closed, comp_empty]; exact Open_univ +by rewrite [↑closed, compl_empty]; exact Open_univ theorem closed_univ : closed (univ : set X) := -by rewrite [↑closed, comp_univ]; exact Open_empty +by rewrite [↑closed, compl_univ]; exact Open_empty theorem closed_sInter {S : set (set X)} (H : ∀₀ t ∈ S, closed t) : closed (⋂₀ S) := begin - rewrite [↑closed, comp_sInter], + rewrite [↑closed, compl_sInter], apply Open_sUnion, intro t, - rewrite [mem_image_complement, Open_iff_closed_comp], + rewrite [mem_image_compl, Open_iff_closed_compl], apply H end theorem closed_Inter {I : Type} {s : I → set X} (H : ∀ i, closed (s i : set X)) : closed (⋂ i, s i) := -by rewrite [↑closed, comp_Inter]; apply Open_Union; apply H +by rewrite [↑closed, compl_Inter]; apply Open_Union; apply H theorem closed_inter {s t : set X} (Hs : closed s) (Ht : closed t) : closed (s ∩ t) := -by rewrite [↑closed, comp_inter]; apply Open_union; apply Hs; apply Ht +by rewrite [↑closed, compl_inter]; apply Open_union; apply Hs; apply Ht theorem closed_union {s t : set X} (Hs : closed s) (Ht : closed t) : closed (s ∪ t) := -by rewrite [↑closed, comp_union]; apply Open_inter; apply Hs; apply Ht +by rewrite [↑closed, compl_union]; apply Open_inter; apply Hs; apply Ht theorem closed_sUnion_of_finite {s : set (set X)} [fins : finite s] (H : ∀₀ t ∈ s, closed t) : closed (⋂₀ s) := begin - rewrite [↑closed, comp_sInter], + rewrite [↑closed, compl_sInter], apply Open_sUnion, intro t, - rewrite [mem_image_complement, Open_iff_closed_comp], + rewrite [mem_image_compl, Open_iff_closed_compl], apply H end @@ -110,7 +110,7 @@ theorem open_diff {s t : set X} (Hs : Open s) (Ht : closed t) : Open (s \ t) := Open_inter Hs Ht theorem closed_diff {s t : set X} (Hs : closed s) (Ht : Open t) : closed (s \ t) := -closed_inter Hs (closed_comp Ht) +closed_inter Hs (closed_compl Ht) section open classical