Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_preirreducible_iff_subsingleton

Modification history

2022-09-23 08:22
src/topology/separation.lean
feat(topology/subset_properties): an infinite type with cofinite topology is irreducible (#16499)
Modified is_preirreducible_iff_subsingletonView on Github →
2021-12-20 13:27
src/topology/separation.lean
feat(topology/sober): Specialization & generic points & sober spaces (#10914)
Added is_preirreducible_iff_subsingletonView on Github →