Commit 2024-12-20 05:03 e9808488

View on Github →

chore: rename {to,of}_With{Upper,Lower}{Set,}_symm_eq (#19996)

Estimated changes

Modified Mathlib/Topology/Order/LowerUpperTopology.lean

added theorem Topology.WithLower.ofLower_symm

deleted theorem Topology.WithLower.of_WithLower_symm_eq

added theorem Topology.WithLower.toLower_symm

deleted theorem Topology.WithLower.to_WithLower_symm_eq

added theorem Topology.WithUpper.ofUpper_symm

deleted theorem Topology.WithUpper.of_WithUpper_symm_eq

added theorem Topology.WithUpper.toUpper_symm

deleted theorem Topology.WithUpper.to_WithUpper_symm_eq

Modified Mathlib/Topology/Order/UpperLowerSetTopology.lean

added theorem Topology.WithLowerSet.ofLowerSet_symm

deleted theorem Topology.WithLowerSet.of_WithLowerSet_symm_eq

added theorem Topology.WithLowerSet.toLowerSet_symm

deleted theorem Topology.WithLowerSet.to_WithLowerSet_symm_eq

added theorem Topology.WithUpperSet.ofUpperSet_symm

deleted theorem Topology.WithUpperSet.of_WithUpperSet_symm_eq

added theorem Topology.WithUpperSet.toUpperSet_symm

deleted theorem Topology.WithUpperSet.to_WithUpperSet_symm_eq