theorem
RightDirected.finite_bounded_above
{α : Type u_1}
[Preorder α]
[RightDirected α]
{a : Set α}
[Finite ↥a]
:
a.Nonempty → a.BoundedAbove
theorem
LeftDirected.finite_bounded_above
{α : Type u_1}
[Preorder α]
[h : LeftDirected α]
{a : Set α}
[Finite ↥a]
:
a.Nonempty → a.BoundedBelow
theorem
SupSemilattice.finite_hasLUB
{α : Type u_1}
[SupSemilattice α]
{a : Set α}
[Finite ↥a]
:
a.Nonempty → ∃ (x : α), IsLUB a x
theorem
SupSemilattice.finite_hasLUB'
{α : Type u_1}
[SupSemilattice α]
[HasLeast α]
{a : Set α}
[Finite ↥a]
:
∃ (x : α), IsLUB a x
theorem
InfSemilattice.finite_hasGLB
{α : Type u_1}
[InfSemilattice α]
{a : Set α}
[Finite ↥a]
:
a.Nonempty → ∃ (x : α), IsGLB a x
theorem
InfSemilattice.finite_hasGLB'
{α : Type u_1}
[InfSemilattice α]
[HasGreatest α]
{a : Set α}
[Finite ↥a]
:
∃ (x : α), IsGLB a x
theorem
TotalOrder.finite_has_greatest
{α : Type u_1}
[TotalOrder α]
{a : Set α}
[_hf : Finite ↥a]
:
a.Nonempty → ∃ (x : ↥a), Greatest x
theorem
TotalOrder.finite_has_least
{α : Type u_1}
[TotalOrder α]
{a : Set α}
[hf : Finite ↥a]
(hne : a.Nonempty)
:
∃ (x : ↥a), Least x
theorem
TotalOrder.finite_greatest
{α : Type u_1}
[ne : Nonempty α]
[TotalOrder α]
[Finite α]
:
∃ (x : α), Greatest x
theorem
TotalOrder.finite_least
{α : Type u_1}
[ne : Nonempty α]
[TotalOrder α]
[Finite α]
:
∃ (x : α), Least x
Equations
- instWellOrderOfTotalOrderOfFinite = WellOrder.mk ⋯
instance
partialOrder_finite_inductive
{α : Type u_1}
[PartialOrder α]
[Finite α]
[hne : Nonempty α]
:
Equations
- ⋯ = ⋯
theorem
PartialOrder.finite_has_maximal
{α : Type u_1}
[PartialOrder α]
[Finite α]
[Nonempty α]
:
∃ (x : α), Maximal x
theorem
PartialOrder.finite_has_minimal
{α : Type u_1}
[PartialOrder α]
[Finite α]
[Nonempty α]
:
∃ (x : α), Minimal x