Commit 2024-11-28 16:50 b79cbba3

View on Github →

feat(Order): maximal chains are preserved under order isomorphisms (#19471) From LeanCamCombi

Estimated changes

added theorem Flag.coe_map
added theorem Flag.coe_ofIsMaxChain
added def Flag.map
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