Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-01 07:02 226ea0fd

View on Github →

feat(topology/subset_properties): upgrade is_(pre)irreducible.closure to iff (#17254)

Estimated changes

Modified src/topology/basic.lean

added theorem closure_inter_open_nonempty_iff

Modified src/topology/subset_properties.lean

deleted theorem is_irreducible.closure

added theorem is_irreducible_iff_closure

deleted theorem is_preirreducible.closure

added theorem is_preirreducible_iff_closure