isClopen_range_sigmaMk — Mathlib

English

For a family of types X_i with i in some index set, the range of Sigma.mk is clopen.

Русский

Для семейства типов X_i индексированного i суммируемого типа Sigma.mk их диапазон является клиopen.

LaTeX

$$$$ \operatorname{IsClopen}\left(\operatorname{range}\left(\Sigma\,\mathrm{mk}\, i\right)\right) $$$$

Lean4

theorem isClopen_range_sigmaMk {X : ι → Type*} [∀ i, TopologicalSpace (X i)] {i : ι} :
    IsClopen (Set.range (@Sigma.mk ι X i)) :=
  ⟨IsClosedEmbedding.sigmaMk.isClosed_range, IsOpenEmbedding.sigmaMk.isOpen_range⟩

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