Skip to content

Commit

Permalink
more lemmas
Browse files Browse the repository at this point in the history
  • Loading branch information
@YaelDillies
YaelDillies committed Jan 3, 2025
1 parent ddf26b3 commit 4e337c3
Showing 1 changed file with 91 additions and 14 deletions.
105 changes: 91 additions & 14 deletions Mathlib/Topology/Constructible.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,9 @@ lemma IsRetrocompact.union (hs : IsRetrocompact s) (ht : IsRetrocompact t) :
IsRetrocompact (s ∪ t : Set X) :=
fun _U hUcomp hUopen ↦ union_inter_distrib_right .. ▸ (hs hUcomp hUopen).union (ht hUcomp hUopen)

private lemma supClosed_isRetrocompact : SupClosed {s : Set X | IsRetrocompact s} :=
fun _s hs _t ht ↦ hs.union ht

lemma IsRetrocompact.finsetSup {ι : Type*} {s : Finset ι} {t : ι → Set X}
(ht : ∀ i ∈ s, IsRetrocompact (t i)) : IsRetrocompact (s.sup t) := by
induction' s using Finset.cons_induction with i s ih hi
Expand All @@ -63,22 +66,50 @@ lemma IsRetrocompact.finsetSup' {ι : Type*} {s : Finset ι} {hs} {t : ι → Se
(ht : ∀ i ∈ s, IsRetrocompact (t i)) : IsRetrocompact (s.sup' hs t) := by
rw [Finset.sup'_eq_sup]; exact .finsetSup ht

lemma IsRetrocompact.inter [T2Space X] (hs : IsRetrocompact s) (ht : IsRetrocompact t) :
lemma IsRetrocompact.iUnion [Finite ι] {f : ι → Set X} (hf : ∀ i, IsRetrocompact (f i)) :
IsRetrocompact (⋃ i, f i) := supClosed_isRetrocompact.iSup_mem .empty hf

lemma IsRetrocompact.sUnion {S : Set (Set X)} (hS : S.Finite) (hS' : ∀ s ∈ S, IsRetrocompact s) :
IsRetrocompact (⋃₀ S) := supClosed_isRetrocompact.sSup_mem hS .empty hS'

lemma IsRetrocompact.biUnion {ι : Type*} {f : ι → Set X} {t : Set ι} (ht : t.Finite)
(hf : ∀ i ∈ t, IsRetrocompact (f i)) : IsRetrocompact (⋃ i ∈ t, f i) :=
supClosed_isRetrocompact.biSup_mem ht .empty hf

section T2Space
variable [T2Space X]

lemma IsRetrocompact.inter (hs : IsRetrocompact s) (ht : IsRetrocompact t) :
IsRetrocompact (s ∩ t : Set X) :=
fun _U hUcomp hUopen ↦ inter_inter_distrib_right .. ▸ (hs hUcomp hUopen).inter (ht hUcomp hUopen)

lemma IsRetrocompact.finsetInf [T2Space X] {ι : Type*} {s : Finset ι} {t : ι → Set X}
private lemma infClosed_isRetrocompact : InfClosed {s : Set X | IsRetrocompact s} :=
fun _s hs _t ht ↦ hs.inter ht

lemma IsRetrocompact.finsetInf {ι : Type*} {s : Finset ι} {t : ι → Set X}
(ht : ∀ i ∈ s, IsRetrocompact (t i)) : IsRetrocompact (s.inf t) := by
induction' s using Finset.cons_induction with i s ih hi
· simp
· rw [Finset.inf_cons]
exact (ht _ <| by simp).inter <| hi <| Finset.forall_of_forall_cons ht

set_option linter.docPrime false in
lemma IsRetrocompact.finsetInf' [T2Space X] {ι : Type*} {s : Finset ι} {hs} {t : ι → Set X}
lemma IsRetrocompact.finsetInf' {ι : Type*} {s : Finset ι} {hs} {t : ι → Set X}
(ht : ∀ i ∈ s, IsRetrocompact (t i)) : IsRetrocompact (s.inf' hs t) := by
rw [Finset.inf'_eq_inf]; exact .finsetInf ht

lemma IsRetrocompact.iInter [Finite ι] {f : ι → Set X} (hf : ∀ i, IsRetrocompact (f i)) :
IsRetrocompact (⋂ i, f i) := infClosed_isRetrocompact.iInf_mem .univ hf

lemma IsRetrocompact.sInter {S : Set (Set X)} (hS : S.Finite) (hS' : ∀ s ∈ S, IsRetrocompact s) :
IsRetrocompact (⋂₀ S) := infClosed_isRetrocompact.sInf_mem hS .univ hS'

lemma IsRetrocompact.biInter {ι : Type*} {f : ι → Set X} {t : Set ι} (ht : t.Finite)
(hf : ∀ i ∈ t, IsRetrocompact (f i)) : IsRetrocompact (⋂ i ∈ t, f i) :=
infClosed_isRetrocompact.biInf_mem ht .univ hf

end T2Space

lemma IsRetrocompact.inter_isOpen (hs : IsRetrocompact s) (ht : IsRetrocompact t)
(htopen : IsOpen t) : IsRetrocompact (s ∩ t : Set X) :=
fun _U hUcomp hUopen ↦ inter_assoc .. ▸ hs (ht hUcomp hUopen) (htopen.inter hUopen)
Expand Down Expand Up @@ -257,11 +288,14 @@ lemma isConstructible_preimage_of_isOpenEmbedding {s : Set Y} (hf : IsOpenEmbedd

section CompactSpace
variable [CompactSpace X] {P : ∀ s : Set X, IsConstructible s → Prop} {B : Set (Set X)}
{b : ι → Set X}

lemma _root_.IsRetrocompact.isCompact (hs : IsRetrocompact s) : IsCompact s := by
simpa using hs CompactSpace.isCompact_univ

lemma _root_.TopologicalSpace.IsTopologicalBasis.IsRetrocompact_iff_isCompact
/-- Variant of `TopologicalSpace.IsTopologicalBasis.isRetrocompact_iff_isCompact` for a
non-indexed topological basis. -/
lemma _root_.TopologicalSpace.IsTopologicalBasis.isRetrocompact_iff_isCompact'
(basis : IsTopologicalBasis B) (compact_inter : ∀ U ∈ B, ∀ V ∈ B, IsCompact (U ∩ V))
(hU : IsOpen U) : IsRetrocompact U ↔ IsCompact U := by
refine ⟨IsRetrocompact.isCompact, fun hU' {V} hV' hV ↦ ?_⟩
Expand All @@ -273,22 +307,65 @@ lemma _root_.TopologicalSpace.IsTopologicalBasis.IsRetrocompact_iff_isCompact
and_imp, forall_exists_index, Prod.forall]
exact fun u v hu _ hv _ ↦ compact_inter _ hu _ hv

lemma _root_.TopologicalSpace.IsTopologicalBasis.IsRetrocompact (basis : IsTopologicalBasis B)
lemma _root_.TopologicalSpace.IsTopologicalBasis.isRetrocompact_iff_isCompact
(basis : IsTopologicalBasis (range b)) (compact_inter : ∀ i j, IsCompact (b i ∩ b j))
(hU : IsOpen U) : IsRetrocompact U ↔ IsCompact U :=
basis.isRetrocompact_iff_isCompact' (by simpa using compact_inter) hU

/-- Variant of `TopologicalSpace.IsTopologicalBasis.isRetrocompact` for a non-indexed topological
basis. -/
lemma _root_.TopologicalSpace.IsTopologicalBasis.isRetrocompact' (basis : IsTopologicalBasis B)
(compact_inter : ∀ U ∈ B, ∀ V ∈ B, IsCompact (U ∩ V)) (hU : U ∈ B) : IsRetrocompact U :=
(basis.IsRetrocompact_iff_isCompact compact_inter <| basis.isOpen hU).2 <| by
(basis.isRetrocompact_iff_isCompact' compact_inter <| basis.isOpen hU).2 <| by
simpa using compact_inter _ hU _ hU

lemma _root_.TopologicalSpace.IsTopologicalBasis.isConstructible (basis : IsTopologicalBasis B)
lemma _root_.TopologicalSpace.IsTopologicalBasis.isRetrocompact
(basis : IsTopologicalBasis (range b)) (compact_inter : ∀ i j, IsCompact (b i ∩ b j)) (i : ι) :
IsRetrocompact (b i) :=
(basis.isRetrocompact_iff_isCompact compact_inter <| basis.isOpen <| mem_range_self _).2 <| by
simpa using compact_inter i i

/-- Variant of `TopologicalSpace.IsTopologicalBasis.isConstructible` for a non-indexed topological
basis. -/
lemma _root_.TopologicalSpace.IsTopologicalBasis.isConstructible' (basis : IsTopologicalBasis B)
(compact_inter : ∀ U ∈ B, ∀ V ∈ B, IsCompact (U ∩ V)) (hU : U ∈ B) : IsConstructible U :=
(basis.IsRetrocompact compact_inter hU).isConstructible <| basis.isOpen hU
(basis.isRetrocompact' compact_inter hU).isConstructible <| basis.isOpen hU

lemma _root_.TopologicalSpace.IsTopologicalBasis.isConstructible
(basis : IsTopologicalBasis (range b)) (compact_inter : ∀ i j, IsCompact (b i ∩ b j)) (i : ι) :
IsConstructible (b i) :=
(basis.isRetrocompact compact_inter _).isConstructible <| basis.isOpen <| mem_range_self _

proof_wanted IsConstructible.induction_of_isTopologicalBasis (basis : IsTopologicalBasis B)
(compact_inter : ∀ U ∈ B, ∀ V ∈ B, IsCompact (U ∩ V))
(sdiff : ∀ U (hU : U ∈ B) 𝒱 (h𝒱B : 𝒱 ⊆ B) (h𝒱 : 𝒱.Finite), P (U \ ⋃ V ∈ 𝒱, V)
((basis.isConstructible compact_inter hU).sdiff <| .biUnion h𝒱 fun V hV ↦
basis.isConstructible compact_inter <| h𝒱B hV))
@[elab_as_elim]
lemma IsConstructible.induction_of_isTopologicalBasis {ι : Type*} [Nonempty ι] (b : ι → Set X)
(basis : IsTopologicalBasis (range b)) (compact_inter : ∀ i j, IsCompact (b i ∩ b j))
(sdiff : ∀ i s (hs : Set.Finite s), P (b i \ ⋃ j ∈ s, b j)
((basis.isConstructible compact_inter _).sdiff <| .biUnion hs fun _ _ ↦
basis.isConstructible compact_inter _))
(union : ∀ s hs t ht, P s hs → P t ht → P (s ∪ t) (hs.union ht))
(s : Set X) (hs : IsConstructible s) : P s hs
(s : Set X) (hs : IsConstructible s) : P s hs := by
induction hs using BooleanSubalgebra.closure_sdiff_sup_induction with
| sup => exact fun s hs t ht ↦ ⟨hs.1.union ht.1, hs.2.union ht.2⟩
| inf => exact fun s hs t ht ↦ ⟨hs.1.inter ht.1, hs.2.inter_isOpen ht.2 ht.1⟩
| bot_mem => exact ⟨isOpen_empty, .empty⟩
| top_mem => exact ⟨isOpen_univ, .univ⟩
| sdiff U hU V hV =>
have := isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis _ basis
fun i ↦ by simpa using compact_inter i i
obtain ⟨s, hs, rfl⟩ := (this _).1 ⟨hU.2.isCompact, hU.1⟩
obtain ⟨t, ht, rfl⟩ := (this _).1 ⟨hV.2.isCompact, hV.1⟩
simp_rw [iUnion_diff]
induction s, hs using Set.Finite.dinduction_on with
| H0 => simpa using sdiff (Classical.arbitrary _) {Classical.arbitrary _}
| @H1 i s hi hs ih =>
simp_rw [biUnion_insert]
exact union _ _ _
(.biUnion hs fun i _ ↦ (basis.isConstructible compact_inter _).sdiff <|
.biUnion ht fun j _ ↦ basis.isConstructible compact_inter _)
(sdiff _ _ ht)
(ih ⟨isOpen_biUnion fun _ _ ↦ basis.isOpen ⟨_, rfl⟩, .biUnion hs
fun i _ ↦ basis.isRetrocompact compact_inter _⟩)
| sup' s _ t _ hs' ht' => exact union _ _ _ _ hs' ht'

end CompactSpace

Expand Down

0 comments on commit 4e337c3

Please sign in to comment.