induced_restrict — Mathlib

English

For S ⊆ I, the induced topology on S.restrict Pi.topologicalSpace equals the infimum over i ∈ S of induced (eval i) (T i).

Русский

Для S ⊆ I индуцированная топология на S.restrict Pi.topologicalSpace равна инфимума по i ∈ S индуцированным (eval i) (T_i).

LaTeX

$$$\\operatorname{Induced}(S\\restriction\\Pi\\text{topologicalSpace}) = \\bigwedge_{i\\in S} \\operatorname{Induced}(\\mathrm{eval}\,i, T_i).$$$

Lean4

theorem induced_restrict (S : Set ι) : induced (S.restrict) Pi.topologicalSpace = ⨅ i ∈ S, induced (eval i) (T i) := by
  simp +unfoldPartialApp [← iInf_subtype'', ← induced_precomp' ((↑) : S → ι), restrict]

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