Documentation Verification Report

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_subsingleton_isCofinal`, `exists_lt_map_eq_of_mapsTo`, `finite_isBot`, `finite_isTop`, `infinite_of_forall_exists_gt`, `infinite_of_forall_exists_lt`	23
Total	23

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` `SetLike.instMembership` `instSetLike`	`Preorder.toLE` `Maximal` `Finset` `SetLike.instMembership` `instSetLike`	—	`exists_maximal` `instIsTransLe` `mem_filter` `le_rfl` `LE.le.trans`
`exists_le_minimal` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike`	`Preorder.toLE` `Minimal` `Finset` `SetLike.instMembership` `instSetLike`	—	`exists_le_maximal`
`exists_maximal` 📖	mathematical	`Nonempty`	`Maximal` `Finset` `SetLike.instMembership` `instSetLike`	—	`exists_maximalFor`
`exists_maximalFor` 📖	mathematical	`Nonempty`	`MaximalFor` `Finset` `SetLike.instMembership` `instSetLike`	—	`Nonempty.cons_induction` `mem_cons_self` `trans` `mem_cons_of_mem` `instIsEmptyFalse`
`exists_minimal` 📖	mathematical	`Nonempty`	`Minimal` `Finset` `SetLike.instMembership` `instSetLike`	—	`exists_minimalFor`
`exists_minimalFor` 📖	mathematical	`Nonempty`	`MinimalFor` `Finset` `SetLike.instMembership` `instSetLike`	—	`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` `Set` `Set.instMembership`	—	`CanLift.prf` `Set.instCanLiftFinsetCoeFinite` `Finset.exists_le_maximal`
`exists_le_minimal` 📖	mathematical	`Set` `Set.instMembership`	`Preorder.toLE` `Minimal` `Set` `Set.instMembership`	—	`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`
`exists_subsingleton_isCofinal` 📖	mathematical	`IsCofinal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set` `Set.Subsingleton` `IsCofinal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Set.eq_empty_or_nonempty` `exists_maximal` `instIsTransLe` `LE.le.trans` `Maximal.le`

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