English
If a topology is generated from half-infinite intervals (Ioi and Iio) with endpoints in a set c, then the finite intersections of these intervals form a topological basis.
Русский
Если топология генерируется из полуотрезков (Ioi и Iio) с концами в множествах c, то конечные пересечения таких интервалов образуют базис топологии.
LaTeX
$$$IsTopologicalBasis\\bigl\\{(\\bigcap_{a\\in f} Ioi(a)) \\cap (\\bigcap_{a\\in g} Iio(a)\\ \\vert \\ f,g\\subseteq c, f,g\\text{ finite)}\\bigr\\}$$$
Lean4
/-- If a topology is generated by half-open intervals with endpoints in a set `c`, then the sets
formed by intersecting finitely many of these intervals form a topological basis. -/
theorem isTopologicalBasis_biInter_Ioi_Iio_of_generateFrom (c : Set α)
(h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}) :
IsTopologicalBasis
{s | ∃ (f g : Set α), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ (⋂ a ∈ g, Iio a)} :=
by
refine IsTopologicalBasis.of_isOpen_of_subset ?_ (isTopologicalBasis_of_subbasis h) ?_
· rintro u ⟨f, g, hfc, hgc, hf_fin, hg_fin, rfl⟩
apply IsOpen.inter
· apply hf_fin.isOpen_biInter (fun i hi ↦ ?_)
rw [h]
exact isOpen_generateFrom_of_mem ⟨i, hfc hi, Or.inl rfl⟩
· apply hg_fin.isOpen_biInter (fun i hi ↦ ?_)
rw [h]
exact isOpen_generateFrom_of_mem ⟨i, hgc hi, Or.inr rfl⟩
simp only [exists_and_left, image_subset_iff, preimage_setOf_eq, setOf_subset_setOf, and_imp]
intro k k_fin hk
let kl := {s ∈ k | ∃ a ∈ c, s = Ioi a}
let kr := {s ∈ k | ∃ a ∈ c, s = Iio a}
have k_eq : k = kl ∪ kr := by
have : ∀ s ∈ k, ∃ a ∈ c, s = Ioi a ∨ s = Iio a := hk
ext
simp only [mem_union, mem_setOf_eq, kl, kr]
grind
have : Finite kl := k_fin.subset (by simp [k_eq])
have : Finite kr := k_fin.subset (by simp [k_eq])
have Al : ∀ s : kl, ∃ a ∈ c, s = Ioi a := fun s ↦ s.2.2
choose al alc hal using Al
have Ar : ∀ s : kr, ∃ a ∈ c, s = Iio a := fun s ↦ s.2.2
choose ar arc har using Ar
refine
⟨range al, by simp [range_subset_iff, alc], range ar, by simp [range_subset_iff, arc], finite_range _,
finite_range _, ?_⟩
rw [k_eq, sInter_eq_biInter, biInter_union, biInter_range, biInter_range, biInter_eq_iInter, biInter_eq_iInter]
simp [hal, har]
