Mathlib v3 is deprecated. Go to Mathlib v4

Theorem not_preirreducible_nontrivial_t2

Modification history

2022-09-23 08:22

src/topology/separation.lean

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

Added not_preirreducible_nontrivial_t2 View on Github →