Commit 2025-10-09 13:01 b7b295a9

View on Github →

chore (Topology/UniformSpace/Ultra): deprecate IsTransitiveRel.mem_filter_prod_comm (#30319)

Estimated changes

Modified Mathlib/Topology/UniformSpace/Ultra/Basic.lean

deleted theorem IsTransitiveRel.mem_filter_prod_comm

Modified Mathlib/Topology/UniformSpace/Ultra/Completion.lean