Commit 2025-09-29 10:30 1cde8411

View on Github →

feat: Equiv.with{Top,Bot}Congr (#29968) Extracted from #27918

Estimated changes

Modified Mathlib/Order/Hom/WithTopBot.lean

Modified Mathlib/Order/Interval/Basic.lean

Modified Mathlib/Order/WithBot.lean

added def Equiv.withBotCongr

added theorem Equiv.withBotCongr_refl

added theorem Equiv.withBotCongr_symm

added theorem Equiv.withBotCongr_trans

added def Equiv.withTopCongr

added theorem Equiv.withTopCongr_refl

added theorem Equiv.withTopCongr_symm

added theorem Equiv.withTopCongr_trans

Modified Mathlib/Topology/Compactification/OnePoint/Basic.lean