isOpen_def — Mathlib

English

For every set s ⊆ WithUpper α, IsOpen s iff IsOpen[upper α] (toUpper ⁻¹' s).

Русский

Для любого множества s ⊆ WithUpper α верно: открыто ли s тогда и только тогда, когда toUpper⁻¹(s) открыто в верхней топологии α.

LaTeX

$$$\\forall s : Set(WithUpper α),\\ IsOpen s \\iff IsOpen[upper α] (toUpper^{-1} s)$$$

Lean4

theorem isOpen_def {s : Set (WithUpper α)} : IsOpen s ↔ (upper α).IsOpen (toUpper ⁻¹' s) :=
  Iff.rfl

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