TeichmullerTukey

📁 Source: Mathlib/Order/TeichmullerTukey.lean

Statistics

Metric	Count
Definitions IsOfFiniteCharacter	1
Theorems exists_maximal	1
Total	2

Order

Definitions

Name	Category	Theorems
IsOfFiniteCharacter 📖	MathDef	—

Order.IsOfFiniteCharacter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_maximal 📖	mathematical	Order.IsOfFiniteCharacter Set Set.instMembership	Set.instHasSubset Maximal Set.instLE	—	zorn_subset_nonempty DirectedOn.exists_mem_subset_of_finite_of_subset_sUnion IsChain.directedOn Set.instReflSubset Set.subset_sUnion_of_mem

---

← Back to Index