sup — Mathlib

English

The disjoint union of two sequential spaces is sequential.

Русский

Разделение по прямому произведению двух последовательных пространств остаётся последовательным.

LaTeX

$$$\text{SequentialSpace}(X) \land \text{SequentialSpace}(Y) \Rightarrow \text{SequentialSpace}(X \oplus Y)$$$

Lean4

protected theorem sup {X} {t₁ t₂ : TopologicalSpace X} (h₁ : @SequentialSpace X t₁) (h₂ : @SequentialSpace X t₂) :
    @SequentialSpace X (t₁ ⊔ t₂) := by
  rw [sup_eq_iSup]
  exact .iSup <| Bool.forall_bool.2 ⟨h₂, h₁⟩

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