English
For a subset s of the cofinite space CofiniteTopology X, s is open exactly when either s is nonempty and its complement is finite, or equivalently s is nonempty implies sᶜ is finite.
Русский
Для подмножества s пространства CofiniteTopology X открытость эквивалентна тому, что либо s непусто и его комплемент конечен, либо эквивалентно тому, что непустость s влечёт конечность комплемента.
LaTeX
$$$$ IsOpen(s) \\iff s.Nonempty \\to s^c \\\\ Finite $$$$
Lean4
instance : TopologicalSpace (CofiniteTopology X)
where
IsOpen s := s.Nonempty → Set.Finite sᶜ
isOpen_univ := by simp
isOpen_inter s
t := by
rintro hs ht ⟨x, hxs, hxt⟩
rw [compl_inter]
exact (hs ⟨x, hxs⟩).union (ht ⟨x, hxt⟩)
isOpen_sUnion := by
rintro s h ⟨x, t, hts, hzt⟩
rw [compl_sUnion]
exact Finite.sInter (mem_image_of_mem _ hts) (h t hts ⟨x, hzt⟩)
