induced_iInf — Mathlib

English

For a family t_i of topologies on α, the induced topology of the infimum over i equals the infimum of the induced topologies: ind_g( inf_i t_i ) = inf_i ind_g(t_i).

Русский

Для семейства топологий t_i на α выполняется: индуцированная по g топология от inf_i t_i равна inf_i индуцированной по g топологии t_i.

LaTeX

$$$\operatorname{induced}_g(\inf_i t_i) = \inf_i \operatorname{induced}_g(t_i)$$$

Lean4

@[simp]
theorem induced_iInf {ι : Sort w} {t : ι → TopologicalSpace α} : (⨅ i, t i).induced g = ⨅ i, (t i).induced g :=
  (gc_coinduced_induced g).u_iInf

Похожие утверждения