isClosed_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem isClosed_iff [TopologicalSpace X] {s : Set (ULift.{v} X)} : IsClosed s ↔ IsClosed (ULift.up ⁻¹' s) := by
  rw [← isOpen_compl_iff, ← isOpen_compl_iff, isOpen_iff, preimage_compl]

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