isOpen_sup — Mathlib

English

Let t1 and t2 be topologies on α and s ⊆ α. Then s is open in the supremum topology t1 ⊔ t2 if and only if s is open in t1 and in t2.

Русский

Пусть t1 и t2 — топологии на α, и S ⊆ α. Тогда S открыто в верхней сумме топологий t1 ⊔ t2 тогда и только тогда, когда S открыто в t1 и в t2.

LaTeX

$$$$ IsOpen_{t_1 \lor t_2}(s) \iff IsOpen_{t_1}(s) \land IsOpen_{t_2}(s). $$$$

Lean4

theorem isOpen_sup {t₁ t₂ : TopologicalSpace α} {s : Set α} : IsOpen[t₁ ⊔ t₂] s ↔ IsOpen[t₁] s ∧ IsOpen[t₂] s :=
  Iff.rfl

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