Northcott

📁 Source: Mathlib/NumberTheory/Height/Northcott.lean

Statistics

Metric	Count
Definitions Northcott	1
Theorems exists_min_image, finite_le, northcott_iff, northcott_iff_tendsto	4
Total	5

Northcott

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_min_image 📖	mathematical	Set.Nonempty	Set Set.instMembership Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Set.exists_min_image Set.Finite.inter_of_left finite_le le_rfl
finite_le 📖	mathematical	—	Set.Finite setOf	—	—

(root)

Definitions

Name	Category	Theorems
Northcott 📖	CompData	2 math math: northcott_iff_tendsto, northcott_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
northcott_iff 📖	mathematical	—	Northcott Set.Finite setOf	—	—
northcott_iff_tendsto 📖	mathematical	—	Northcott Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.Tendsto Filter.cofinite Filter.atTop	—	Set.Finite.subset le_of_lt NoMaxOrder.exists_gt lt_of_le_of_lt

---

← Back to Index