isOpen_iff — Mathlib

English

A set is open iff it contains 0 in its complement or contains a ray Iio(γ) with γ ≠ 0.

Русский

Множество открыто тогда, когда оно содержит 0 в дополнении или содержит луч Iio(γ) с γ ≠ 0.

LaTeX

$$$\text{IsOpen}(s) \iff \bigl(0 \notin s\bigr) \lor \exists γ ≠ 0, Iio(γ) \subseteq s$$$

Lean4

theorem isOpen_iff {s : Set Γ₀} : IsOpen s ↔ (0 : Γ₀) ∉ s ∨ ∃ γ, γ ≠ 0 ∧ Iio γ ⊆ s :=
  by
  rw [isOpen_iff_mem_nhds, ← and_forall_ne (0 : Γ₀)]
  simp +contextual [nhds_of_ne_zero, imp_iff_not_or, hasBasis_nhds_zero.mem_iff]

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