Commit 2025-11-04 17:16 70d200fd

View on Github →

feat(Data/Setoid/Basic): add theorems about lifting a function to its kernel (#28818) Currently ker_lift_injective and quotientKerEquivOfRightInverse lift f to ker f in their definition. This PR makes this function available as Setoid.kerLift f and adds a few more theorems about it.

Estimated changes

Modified Counterexamples/AharoniKorman.lean

Modified Mathlib/Data/Setoid/Basic.lean

added def Setoid.kerLift

added theorem Setoid.kerLift_injective

added theorem Setoid.kerLift_mk

modified theorem Setoid.ker_eq_lift_of_injective

deleted theorem Setoid.ker_lift_injective

added theorem Setoid.lift_injective_iff_ker_eq_of_le

added theorem Setoid.range_kerLift_eq_range

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean

Modified Mathlib/Topology/Separation/Hausdorff.lean