Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-11-28 16:50
b79cbba3
View on Github →
feat(Order): maximal chains are preserved under order isomorphisms (
#19471
) From LeanCamCombi
Estimated changes
Modified
Mathlib/Order/Chain.lean
added
theorem
Flag.coe_map
added
theorem
Flag.coe_ofIsMaxChain
added
def
Flag.map
added
theorem
Flag.mem_iff_forall_le_or_ge
added
def
Flag.ofIsMaxChain
added
theorem
Flag.symm_map
added
theorem
IsChain.empty
added
theorem
IsChain.pair
added
theorem
IsChain.singleton
added
theorem
IsMaxChain.image
deleted
theorem
isChain_empty