isClosed_iff — Mathlib

English

A subset s of CofiniteTopology X is closed exactly when s is the whole space or s is finite.

Русский

Подмножество s CofiniteTopology X замкнуто тогда и только тогда, когда оно есть целое пространство или конечное.

LaTeX

$$$$ IsClosed(s) \\iff s = \\text{univ} \\lor s.Finite $$$$

Lean4

theorem isClosed_iff {s : Set (CofiniteTopology X)} : IsClosed s ↔ s = univ ∨ s.Finite := by
  simp only [← isOpen_compl_iff, isOpen_iff', compl_compl, compl_empty_iff]

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