ZornAtoms

📁 Source: Mathlib/Order/ZornAtoms.lean

Statistics

Metric	Count
Definitions	0
Theorems of_isChain_bounded, of_isChain_bounded	2
Total	2

IsAtomic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isChain_bounded 📖	mathematical	Set Set.instMembership lowerBounds Preorder.toLE PartialOrder.toPreorder	IsAtomic	—	isCoatomic_dual_iff_isAtomic IsCoatomic.of_isChain_bounded IsChain.symm

IsCoatomic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isChain_bounded 📖	mathematical	Set Set.instMembership upperBounds Preorder.toLE PartialOrder.toPreorder	IsCoatomic	—	zorn_le_nonempty₀ LT.lt.ne le_trans Ne.lt_top Set.left_mem_Ico Maximal.prop LE.le.eq_or_lt le_top Maximal.eq_of_le LE.le.trans LT.lt.le

---

← Back to Index