LeastGreatest

📁 Source: Mathlib/Data/Int/LeastGreatest.lean

Statistics

Metric	Count
Definitions greatestOfBdd, leastOfBdd	2
Theorems coe_greatestOfBdd_eq, coe_leastOfBdd_eq, exists_greatest_of_bdd, exists_least_of_bdd, isGreatest_coe_greatestOfBdd, isLeast_coe_leastOfBdd	6
Total	8

Int

Definitions

Name	Category	Theorems
greatestOfBdd 📖	CompOp	4 math math: coe_greatestOfBdd_eq, csSup_eq_greatestOfBdd, isGreatest_coe_greatestOfBdd, csSup_eq_greatest_of_bdd
leastOfBdd 📖	CompOp	4 math math: coe_leastOfBdd_eq, csInf_eq_least_of_bdd, csInf_eq_leastOfBdd, isLeast_coe_leastOfBdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_greatestOfBdd_eq 📖	mathematical	—	greatestOfBdd	—	le_antisymm
coe_leastOfBdd_eq 📖	mathematical	—	leastOfBdd	—	le_antisymm
exists_greatest_of_bdd 📖	—	—	—	—	—
exists_least_of_bdd 📖	—	—	—	—	—
isGreatest_coe_greatestOfBdd 📖	mathematical	—	IsGreatest setOf greatestOfBdd	—	—
isLeast_coe_leastOfBdd 📖	mathematical	—	IsLeast setOf leastOfBdd	—	—

---

← Back to Index