michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/data/{set,finset},library/*): use compl for set and finset complement

Browse source
This commit is contained in:
Jeremy Avigad 2016-02-16 13:56:01 -05:00 committed by Leonardo de Moura
parent 8f83c78bc9
commit 518a77587a
9 changed files with 103 additions and 103 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
library/data/finset/comb.lean
View file

@ -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

6
library/data/hf.lean
View file

@ -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 :=

102
library/data/set/basic.lean
View file

@ -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 :=

12
library/theories/analysis/metric_space.lean
View file

@ -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,

2
library/theories/analysis/real_limit.lean
View file

@ -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

4
library/theories/group_theory/finsubg.lean
View file

@ -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,

4
library/theories/group_theory/subgroup.lean
View file

@ -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

24
library/theories/measure_theory/sigma_algebra.lean
View file

@ -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

30
library/theories/topology/basic.lean
View file

@ -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