mathlib

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