English
Let X be a topological space. The topology t on X is the infimum of the induced topologies coming from maps X → Opens(X) via the indicator of membership in open sets. This characterizes t as the coarsest topology making all evaluation maps x ↦ (x ∈ U) continuous.
Русский
Пусть X — топологическое пространство. Топология t на X есть инфимума над индукциями топологий, порождаемых отображениями X → Opens(X) с координатами x ↦ (x ∈ U). Эта топология является наименьшей, для которой все соответствующие отображения непрерывны.
LaTeX
$$$t = \bigwedge_{U \in \mathrm{Opens}(X)} \mathrm{induced}(x \mapsto \mathbf{1}_{U}(x)).$$$
Lean4
theorem eq_induced_by_maps_to_sierpinski (X : Type*) [t : TopologicalSpace X] :
t = ⨅ u : Opens X, sierpinskiSpace.induced (· ∈ u) :=
by
apply le_antisymm
· rw [le_iInf_iff]
exact fun u => Continuous.le_induced (isOpen_iff_continuous_mem.mp u.2)
· intro u h
rw [← generateFrom_iUnion_isOpen]
apply isOpen_generateFrom_of_mem
simp only [Set.mem_iUnion, Set.mem_setOf_eq, isOpen_induced_iff]
exact ⟨⟨u, h⟩, { True }, isOpen_singleton_true, by simp [Set.preimage]⟩
