induced_restrict_sUnion — Mathlib

English

For S, the induced topology on S.restrict Pi.topologicalSpace equals the infimum of Induced at eval i for i ∈ S.

Русский

Для S индуцированная топология на S.restrict совпадает с инфимин по eval i для i ∈ S.

LaTeX

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

Lean4

theorem induced_restrict_sUnion (𝔖 : Set (Set ι)) :
    induced (⋃₀ 𝔖).restrict (Pi.topologicalSpace (Y := fun i : (⋃₀ 𝔖) ↦ A i)) =
      ⨅ S ∈ 𝔖, induced S.restrict Pi.topologicalSpace :=
  by simp_rw [Pi.induced_restrict, iInf_sUnion]

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