English
Let s be a set of topologies on α. The topology induced by g from the infimum over s equals the infimum of the induced topologies of the elements of s: induced_g(sInf s) = sInf (induced_g'' s).
Русский
Пусть s — множество топологий на α. Индуцированная по g топология от sInf s равна sInf(induced_g'' s).
LaTeX
$$$\operatorname{induced}_g(\mathrm{sInf}\, s) = \mathrm{sInf}(\mathrm{image}(\operatorname{induced}_g)\, s)$$$
Lean4
@[simp]
theorem induced_sInf {s : Set (TopologicalSpace α)} :
TopologicalSpace.induced g (sInf s) = sInf (TopologicalSpace.induced g '' s) := by
rw [sInf_eq_iInf', sInf_image', induced_iInf]
