ZeroLEOne

📁 Source: Mathlib/Algebra/Order/ZeroLEOne.lean

Statistics

Metric	Count
Definitions ZeroLEOneClass	1
Theorems instZeroLEOneClass, instZeroLEOneClass, instZeroLEOneClass, instZeroLEOneClass, instZeroLEOneClass, factZeroLeOne, factZeroLtOne, zero_le_one, one_pos, zero_le_one, zero_le_one', zero_lt_one, zero_lt_one'	13
Total	14

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instZeroLEOneClass 📖	mathematical	—	ZeroLEOneClass	—	—

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instZeroLEOneClass 📖	mathematical	—	ZeroLEOneClass	—	—

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instZeroLEOneClass 📖	mathematical	ZeroLEOneClass	instZero instOne hasLe	—	zero_le_one

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instZeroLEOneClass 📖	mathematical	—	ZeroLEOneClass instZero instOne instLE_mathlib	—	zero_le_one

Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instZeroLEOneClass 📖	mathematical	—	ZeroLEOneClass	—	—

ZeroLEOneClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
factZeroLeOne 📖	mathematical	—	Fact	—	zero_le_one
factZeroLtOne 📖	mathematical	—	Fact Preorder.toLT PartialOrder.toPreorder	—	zero_lt_one
zero_le_one 📖	—	—	—	—	—

(root)

Definitions

Name	Category	Theorems
ZeroLEOneClass 📖	CompData	24 math math: ZNum.zeroLEOneClass, WithBot.zeroLEOneClass, Surreal.instZeroLEOneClass, CanonicallyOrderedAdd.toZeroLEOneClass, OrderType.instZeroLEOneClass, ConditionallyCompleteLinearOrderedField.toZeroLEOneClass, IsOrderedRing.toZeroLEOneClass, Prod.instZeroLEOneClass, Real.instZeroLEOneClass, Nat.instZeroLEOneClass, Rat.instZeroLEOneClass, Ordinal.instZeroLEOneClass, WithTop.zeroLEOneClass, RCLike.toZeroLEOneClass, PartENat.instZeroLEOneClass, Zsqrtd.instZeroLEOneClassCastInt, instZeroLEOneClass, Nimber.instZeroLEOneClass, SetTheory.PGame.instZeroLEOneClass, Int.instZeroLEOneClass, instZeroLEOneClassEReal, IsStrictOrderedRing.toZeroLEOneClass, LinearOrderedCommMonoidWithZero.toZeroLeOneClass, Set.Icc.instZeroLEOneClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
one_pos 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder	—	zero_lt_one
zero_le_one 📖	—	—	—	—	ZeroLEOneClass.zero_le_one
zero_le_one' 📖	—	—	—	—	zero_le_one
zero_lt_one 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder	—	LE.le.lt_of_ne zero_le_one
zero_lt_one' 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder	—	zero_lt_one

---

← Back to Index