alexandrovDiscrete_iSup — Mathlib

English

Let t_i be a family of topologies on α such that each (α, t_i) is Alexandrov-discrete; then (α, ⨆ i, t_i) is Alexandrov-discrete.

Русский

Пусть дано семейство топологий t_i на числе α, причём каждая пара (α, t_i) Александрово-дискретна; тогда (α, ⨆ i, t_i) Александрово-дискретно.

LaTeX

$$AlexandrovDiscrete(α, ⨆ i, t_i)$$

Lean4

theorem alexandrovDiscrete_iSup {t : ι → TopologicalSpace α} (_ : ∀ i, @AlexandrovDiscrete α (t i)) :
    @AlexandrovDiscrete α (⨆ i, t i) :=
  @AlexandrovDiscrete.mk α (⨆ i, t i) fun _S hS ↦
    isOpen_iSup_iff.2 fun i ↦ @isOpen_sInter _ (t i) _ _ fun _s hs ↦ isOpen_iSup_iff.1 (hS _ hs) _

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