Commit 2026-02-13 13:12 8894c125

View on Github →

chore(Order/RelClasses): resolve TODO (#34386) Resolves TODO in Mathlib/Order/RelClasses by removing Eq.subset and renaming Eq.subset' to Eq.subset.

Estimated changes

Modified Mathlib/Combinatorics/Matroid/Basic.lean

Modified Mathlib/Data/Finset/Card.lean

Modified Mathlib/Data/Set/Basic.lean

deleted theorem Eq.subset

Modified Mathlib/Data/Set/Card.lean

Modified Mathlib/Order/RelClasses.lean

Modified Mathlib/Topology/IsLocalHomeomorph.lean