isOpen_iSup_iff — Mathlib

English

For a family t : ι → TopologicalSpace α and a set s ⊆ α, s is open in the supremum topology ⨆ i, t i iff s is open in every t i.

Русский

Для семейства t : ι → TopologicalSpace α и множества s ⊆ α, s открыто в верхней топологии ⨆ i, t i тогда и только тогда, когда s открыто во всех t i.

LaTeX

$$$\\mathrm{IsOpen}[\\bigvee_i t_i]\,s \\iff \\forall i, \\mathrm{IsOpen}[t_i]\,s$$$

Lean4

theorem isOpen_iSup_iff {s : Set α} : IsOpen[⨆ i, t i] s ↔ ∀ i, IsOpen[t i] s :=
  show s ∈ {s | IsOpen[iSup t] s} ↔ s ∈ {x : Set α | ∀ i : ι, IsOpen[t i] x} by simp [setOf_isOpen_iSup]

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