Commit 2023-01-02 21:24 a2d98732

View on Github →

feat: port Order.ZornAtoms (#1293)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/ZornAtoms.lean

added theorem IsAtomic.of_isChain_bounded

added theorem IsCoatomic.of_isChain_bounded