Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-28 19:31 b7655704

View on Github →

chore(topology): rename interior_eq_of_open (#3614) This allows to use dot notation and is more consistent with its closed twin is_closed.closure_eq

Estimated changes

Modified src/analysis/normed_space/basic.lean

Modified src/geometry/manifold/charted_space.lean

Modified src/geometry/manifold/local_invariant_properties.lean

Modified src/topology/algebra/ordered.lean

Modified src/topology/basic.lean

deleted theorem interior_eq_of_open

added theorem is_open.interior_eq

Modified src/topology/continuous_on.lean

Modified src/topology/local_homeomorph.lean

Modified src/topology/opens.lean

Modified src/topology/subset_properties.lean