isOpen_iff — Mathlib

English

For any X, a set s ⊆ ULift X is open iff its preimage under ULift.up is open in X.

Русский

Для множества s ⊆ ULift X множество открыто тогда и только тогда, когда его предварение под ULift.up открыто в X.

LaTeX

$$$\mathrm{IsOpen}(s) \iff \mathrm{IsOpen}(\mathrm{ULift.up}^{-1}(s)).$$$

Lean4

theorem isOpen_iff [TopologicalSpace X] {s : Set (ULift.{v} X)} : IsOpen s ↔ IsOpen (ULift.up ⁻¹' s) := by
  rw [ULift.topologicalSpace, ← Equiv.ulift_apply, ← Equiv.ulift.coinduced_symm, ← isOpen_coinduced]

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