sup — Mathlib

English

Suprema of delta-generated topologies are delta-generated.

Русский

Супремумы топологий, дельта-генерируемых на одном множестве, являются дельта-генерируемыми.

LaTeX

$$$$\text{DeltaGeneratedSpace}(X, t_1 \sqcup t_2)$$ given $\DeltaGeneratedSpace(X, t_1)$ and $\DeltaGeneratedSpace(X, t_2).$$$$

Lean4

/-- Suprema of delta-generated topologies are delta-generated. -/
protected theorem sup {X : Type*} {t₁ t₂ : TopologicalSpace X} (h₁ : @DeltaGeneratedSpace X t₁)
    (h₂ : @DeltaGeneratedSpace X t₂) : @DeltaGeneratedSpace X (t₁ ⊔ t₂) :=
  by
  rw [sup_eq_iSup]
  exact .iSup <| Bool.forall_bool.2 ⟨h₂, h₁⟩

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