isOpen_iff

Mathlib.Topology.Constructions

URI: https://scilib.ai/kg/mathlib#CofiniteTopology.isOpen_iff

English

For a subset s of CofiniteTopology X, IsOpen s is equivalent to s = ∅ or the complement of s is finite.

Русский

Для подмножества s CofiniteTopology X: 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.Nonempty → sᶜ.Finite :=
  Iff.rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru