Linear

📁 Source: Mathlib/Order/Extension/Linear.lean

Statistics

Metric	Count
Definitions LinearExtension, instInhabitedLinearExtension, instLinearOrderLinearExtensionOfPartialOrder, toLinearExtension	4
Theorems extend_partialOrder	1
Total	5

(root)

Definitions

Name	Category	Theorems
LinearExtension 📖	CompOp	—
instInhabitedLinearExtension 📖	CompOp	—
instLinearOrderLinearExtensionOfPartialOrder 📖	CompOp	—
toLinearExtension 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extend_partialOrder 📖	mathematical	—	IsLinearOrder Pi.hasLe Prop.le	—	refl IsPreorder.toRefl IsPartialOrder.toIsPreorder IsChain.total instReflLe trans IsPreorder.toIsTrans antisymm IsPartialOrder.toAntisymm le_sSup zorn_le_nonempty₀ Maximal.eq_of_le Maximal.prop

---

← Back to Index