Commit 2025-11-03 16:36 f2cc6169

View on Github →

feat(Order): the Bourbaki–Witt theorem (#29652) We prove the Bourbaki-Witt theorem, one of Wiedijk's 1000+ theorems

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/BourbakiWitt.lean

added structure ChainCompletePartialOrder.IsAdmissible

added theorem ChainCompletePartialOrder.IsExtremePt.bot_eq_of_le_or_map_le

added theorem ChainCompletePartialOrder.IsExtremePt.bot_isChain

added theorem ChainCompletePartialOrder.IsExtremePt.mem_bot_iff_isExtremePt

added theorem ChainCompletePartialOrder.IsExtremePt.setOf_isExtremePt_eq_bot

added theorem ChainCompletePartialOrder.IsExtremePt.setOf_isExtremePt_isAdmissible

added structure ChainCompletePartialOrder.IsExtremePt

added theorem ChainCompletePartialOrder.bot_isAdmissible

added theorem ChainCompletePartialOrder.ici_isAdmissible

added theorem ChainCompletePartialOrder.map_mem_bot

added theorem ChainCompletePartialOrder.nonempty_fixedPoints_of_inflationary

added theorem ChainCompletePartialOrder.subset_bot_iff

added structure NonemptyChain

Modified docs/1000.yaml