isOpen_iff' — Mathlib

English

Another form of the same openness criterion: IsOpen s is equivalent to s = ∅ or the complement is finite.

Русский

Ещё одно выражение критерия открытости: IsOpen s эквивалентно s = ∅ или sᶜ конечен.

LaTeX

$$$$ IsOpen(s) \\iff s = \\emptyset \\lor s^c \\ Finite $$$$

Lean4

theorem isOpen_iff' {s : Set (CofiniteTopology X)} : IsOpen s ↔ s = ∅ ∨ sᶜ.Finite := by
  simp only [isOpen_iff, nonempty_iff_ne_empty, or_iff_not_imp_left]

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