isOpen_sum_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem isOpen_sum_iff {s : Set (X ⊕ Y)} : IsOpen s ↔ IsOpen (inl ⁻¹' s) ∧ IsOpen (inr ⁻¹' s) :=
  Iff.rfl

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