sup — Mathlib

English

If two Alexandrov-discrete topologies t1 and t2 are placed on the same set, their supremum topology t1 ⊔ t2 is Alexandrov-discrete.

Русский

Если на одном множестве заданы две Александрово-дискретные топологии t1 и t2, то их верхнее объединение (суупремум) t1 ⊔ t2 также Александрово-дискретно.

LaTeX

$$AlexandrovDiscrete(α, t1 ⊔ t2)$$

Lean4

theorem sup {t₁ t₂ : TopologicalSpace α} (_ : @AlexandrovDiscrete α t₁) (_ : @AlexandrovDiscrete α t₂) :
    @AlexandrovDiscrete α (t₁ ⊔ t₂) :=
  @AlexandrovDiscrete.mk α (t₁ ⊔ t₂) fun _S hS ↦
    ⟨@isOpen_sInter _ t₁ _ _ fun _s hs ↦ (hS _ hs).1, isOpen_sInter fun _s hs ↦ (hS _ hs).2⟩

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