Commit 2025-08-22 21:50 8c7376e0

View on Github →

chore(Topology): deprecate unitInterval.mem_iff_one_sub_mem (duplicate) (#28428)

Estimated changes

Modified Mathlib/Analysis/Normed/Unbundled/SmoothingSeminorm.lean

Modified Mathlib/Topology/UnitInterval.lean

deleted theorem unitInterval.mem_iff_one_sub_mem

modified def unitInterval.symm