instIrreducibleSpaceCofiniteTopologyOfInfinite

English

An infinite type with the cofinite topology is irreducible.

Русский

Бесконечный множество с кофайнтовой топологией неразложимо.

LaTeX

$$$[\text{Infinite } X] \Rightarrow \mathrm{IrreducibleSpace}(\mathrm{CofiniteTopology}(X))$$$

Lean4

/-- An infinite type with cofinite topology is an irreducible topological space. -/
instance (priority := 100) {X} [Infinite X] : IrreducibleSpace (CofiniteTopology X)
    where
  isPreirreducible_univ u
    v := by
    haveI : Infinite (CofiniteTopology X) := ‹_›
    simp only [CofiniteTopology.isOpen_iff, univ_inter]
    intro hu hv hu' hv'
    simpa only [compl_union, compl_compl] using ((hu hu').union (hv hv')).infinite_compl.nonempty
  toNonempty := (inferInstance : Nonempty X)

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