English
The infimum of a family of completely regular topologies on a set X is completely regular.
Русский
На множестве X наименьшее пересечение топологий сохраняет полную регулярность.
LaTeX
$$$\\forall ι\\, (t : ι \\to TopologicalSpace X), (\\forall i, [CompletelyRegularSpace (X, t i)]) \\Rightarrow [CompletelyRegularSpace (X, \\inf_i t_i)]$$$
Lean4
theorem completelyRegularSpace_iInf {ι X : Type*} {t : ι → TopologicalSpace X}
(ht : ∀ i, @CompletelyRegularSpace X (t i)) : @CompletelyRegularSpace X (⨅ i, t i) :=
by
letI :=
(⨅ i, t i) -- register this as default topological space to reduce `@`s
rw [completelyRegularSpace_iff_isOpen]
intro x K hK hxK
simp_rw [← hK.mem_nhds_iff, nhds_iInf, mem_iInf, exists_finite_iff_finset, Finset.coe_sort_coe] at hxK; clear hK
obtain ⟨I', V, hV, rfl⟩ := hxK
simp only [mem_nhds_iff] at hV
choose U hUV hU hxU using hV
replace hU := fun (i : ↥I') => @CompletelyRegularSpace.completely_regular_isOpen _ (t i) (ht i) x (U i) (hU i) (hxU i)
clear hxU
choose fs hfs hxfs hfsU using hU
use I'.attach.sup fs
constructorm* _ ∧ _
· solve_by_elim [Continuous.finset_sup, continuous_iInf_dom]
· simpa [show (0 : ↥I) = ⊥ from rfl] using hxfs
· simp only [EqOn, Pi.one_apply, show (1 : ↥I) = ⊤ from rfl] at hfsU ⊢
conv => equals ∀ x i, x ∈ (V i)ᶜ → ∃ b, fs b x = ⊤ => simp [Finset.sup_eq_top_iff]
intro x i hxi
specialize hfsU i (by tauto_set)
exists i
