Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-23 08:22 02022cd6

View on Github →

feat(topology/subset_properties): an infinite type with cofinite topology is irreducible (#16499)

Estimated changes

Modified src/data/set/basic.lean

Modified src/topology/separation.lean

modified theorem is_irreducible_iff_singleton

modified theorem is_preirreducible_iff_subsingleton

added theorem not_preirreducible_nontrivial_t2

Modified src/topology/sober.lean

Modified src/topology/subset_properties.lean