Finite

📁 Source: Mathlib/Order/Preorder/Finite.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_le_maximal, exists_le_minimal, exists_le_maximal, exists_le_minimal, exists_maximal, exists_maximalFor, exists_minimal, exists_minimalFor, exists_le_maximal, exists_le_minimal, exists_lt_map_eq_of_forall_mem, exists_maximal, exists_maximalFor, exists_maximalFor', exists_minimal, exists_minimalFor, exists_minimalFor', exists_lt_map_eq_of_mapsTo, finite_isBot, finite_isTop, infinite_of_forall_exists_gt, infinite_of_forall_exists_lt	22
Total	22

Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_le_maximal 📖	mathematical	—	Preorder.toLE Maximal	—	Set.Finite.exists_le_maximal Set.toFinite Subtype.finite
exists_le_minimal 📖	mathematical	—	Preorder.toLE Minimal	—	Set.Finite.exists_le_minimal Set.toFinite Subtype.finite

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_le_maximal 📖	mathematical	Finset instMembership	Preorder.toLE Maximal	—	exists_maximal instIsTransLe mem_filter le_rfl LE.le.trans
exists_le_minimal 📖	mathematical	Finset instMembership	Preorder.toLE Minimal	—	exists_le_maximal
exists_maximal 📖	mathematical	Nonempty	Maximal Finset instMembership	—	exists_maximalFor
exists_maximalFor 📖	mathematical	Nonempty	MaximalFor Finset instMembership	—	Nonempty.cons_induction mem_cons_self trans mem_cons_of_mem instIsEmptyFalse
exists_minimal 📖	mathematical	Nonempty	Minimal Finset instMembership	—	exists_minimalFor
exists_minimalFor 📖	mathematical	Nonempty	MinimalFor Finset instMembership	—	exists_maximalFor OrderDual.instIsTransLE

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_isBot 📖	mathematical	—	Finite setOf IsBot Preorder.toLE PartialOrder.toPreorder	—	Subsingleton.finite subsingleton_isBot
finite_isTop 📖	mathematical	—	Finite setOf IsTop Preorder.toLE PartialOrder.toPreorder	—	Subsingleton.finite subsingleton_isTop
infinite_of_forall_exists_gt 📖	mathematical	Set instMembership Preorder.toLT	Infinite	—	infinite_of_injective_forall_mem instInfiniteNat StrictMono.injective strictMono_nat_of_lt_succ
infinite_of_forall_exists_lt 📖	mathematical	Set instMembership Preorder.toLT	Infinite	—	infinite_of_forall_exists_gt OrderDual.instNonempty

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_le_maximal 📖	mathematical	Set Set.instMembership	Preorder.toLE Maximal	—	CanLift.prf Set.instCanLiftFinsetCoeFinite Finset.exists_le_maximal
exists_le_minimal 📖	mathematical	Set Set.instMembership	Preorder.toLE Minimal	—	CanLift.prf Set.instCanLiftFinsetCoeFinite Finset.exists_le_minimal
exists_lt_map_eq_of_forall_mem 📖	mathematical	Set Set.instMembership	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Set.Infinite.exists_lt_map_eq_of_mapsTo Set.infinite_univ Set.mapsTo_univ_iff
exists_maximal 📖	mathematical	Set.Nonempty	Maximal Set Set.instMembership	—	exists_maximalFor
exists_maximalFor 📖	mathematical	Set.Nonempty	MaximalFor Set Set.instMembership	—	CanLift.prf Set.instCanLiftFinsetCoeFinite Finset.exists_maximalFor
exists_maximalFor' 📖	mathematical	Set.Nonempty	MaximalFor Set Set.instMembership	—	exists_maximalFor Set.Nonempty.image Set.mem_image_of_mem
exists_minimal 📖	mathematical	Set.Nonempty	Minimal Set Set.instMembership	—	exists_minimalFor
exists_minimalFor 📖	mathematical	Set.Nonempty	MinimalFor Set Set.instMembership	—	exists_maximalFor OrderDual.instIsTransLE
exists_minimalFor' 📖	mathematical	Set.Nonempty	MinimalFor Set Set.instMembership	—	exists_maximalFor' OrderDual.instIsTransLE

Set.Infinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_lt_map_eq_of_mapsTo 📖	mathematical	Set.Infinite Set.MapsTo	Set Set.instMembership Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	exists_ne_map_eq_of_mapsTo Ne.lt_or_gt

---

← Back to Index