isClosed_iff_coe_preimage — Mathlib

English

Under an open cover, s is open exactly when all the restricted preimages are open.

Русский

При открытом покрытии s открыто тогда и только тогда, когда все ограниченные прообразы открыты.

LaTeX

$$$IsOpen s \\iff \\forall i, IsOpen ((\\uparrow)^{-1}' s : Set (U i))$$$

Lean4

theorem isClosed_iff_coe_preimage {s : Set β} : IsClosed s ↔ ∀ i, IsClosed ((↑) ⁻¹' s : Set (U i)) := by
  simpa using hU.isOpen_iff_coe_preimage (s := sᶜ)

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