isClosed_sum_iff — Mathlib

English

For s ⊆ X ⊕ Y, s is closed iff its preimages under the left and right injections are closed.

Русский

Для множества s ⊆ X ⊕ Y выполняется: s замкнуто ⇔ inl^{-1}(s) замкнуто в X и inr^{-1}(s) замкнуто в Y.

LaTeX

$$$IsClosed(s) \\iff IsClosed(\\mathrm{inl}^{-1}(s)) \\land IsClosed(\\mathrm{inr}^{-1}(s)).$$$

Lean4

theorem isClosed_sum_iff {s : Set (X ⊕ Y)} : IsClosed s ↔ IsClosed (inl ⁻¹' s) ∧ IsClosed (inr ⁻¹' s) := by
  simp only [← isOpen_compl_iff, isOpen_sum_iff, preimage_compl]

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