doc-next-gen

Mathlib.Data.Fintype.Order

Module docstring

{"# Order structures on finite types

This file provides order instances on fintypes.

Computable instances

On a Fintype, we can construct * an OrderBot from SemilatticeInf. * an OrderTop from SemilatticeSup. * a BoundedOrder from Lattice.

Those are marked as def to avoid defeqness issues.

Completion instances

Those instances are noncomputable because the definitions of sSup and sInf use Set.toFinset and set membership is undecidable in general.

On a Fintype, we can promote: * a Lattice to a CompleteLattice. * a DistribLattice to a CompleteDistribLattice. * a LinearOrder to a CompleteLinearOrder. * a BooleanAlgebra to a CompleteAtomicBooleanAlgebra.

Those are marked as def to avoid typeclass loops.

Concrete instances

We provide a few instances for concrete types: * Fin.completeLinearOrder * Bool.completeLinearOrder * Bool.completeBooleanAlgebra ","### Properties for PartialOrders ","### Concrete instances ","### Directed Orders "}

Fintype.toOrderBot abbrev
[SemilatticeInf α] : OrderBot α
Full source 
/-- Constructs the `⊥` of a finite nonempty `SemilatticeInf`. -/
abbrev toOrderBot [SemilatticeInf α] : OrderBot α where
  bot := univ.inf' univ_nonempty id
  bot_le a := inf'_le _ <| mem_univ a
Existence of Bottom Element in Finite Meet-Semilattices
Informal description
For any finite nonempty meet-semilattice $\alpha$, there exists a least element $\bot \in \alpha$ such that $\bot \leq a$ for all $a \in \alpha$.
Fintype.toOrderTop abbrev
[SemilatticeSup α] : OrderTop α
Full source 
/-- Constructs the `⊤` of a finite nonempty `SemilatticeSup` -/
abbrev toOrderTop [SemilatticeSup α] : OrderTop α where
  top := univ.sup' univ_nonempty id
  le_top a := le_sup' id <| mem_univ a
Existence of Top Element in Finite Join-Semilattices
Informal description
For any finite nonempty type $\alpha$ equipped with a join-semilattice structure (i.e., a partial order with binary supremum operation $\sqcup$), there exists a greatest element $\top \in \alpha$ such that $a \leq \top$ for all $a \in \alpha$.
Fintype.toBoundedOrder abbrev
[Lattice α] : BoundedOrder α
Full source 
/-- Constructs the `⊤` and `⊥` of a finite nonempty `Lattice`. -/
abbrev toBoundedOrder [Lattice α] : BoundedOrder α :=
  { toOrderBot α, toOrderTop α with }
Existence of Top and Bottom Elements in Finite Lattices
Informal description
For any finite nonempty type $\alpha$ equipped with a lattice structure, there exists both a greatest element $\top$ and a least element $\bot$ in $\alpha$, making it a bounded order.
Fintype.toCompleteLattice abbrev
[Lattice α] [BoundedOrder α] : CompleteLattice α
Full source 
/-- A finite bounded lattice is complete. -/
noncomputable abbrev toCompleteLattice [Lattice α] [BoundedOrder α] : CompleteLattice α where
  __ := ‹Lattice α›
  __ := ‹BoundedOrder α›
  sSup := fun s => s.toFinset.sup id
  sInf := fun s => s.toFinset.inf id
  le_sSup := fun _ _ ha => Finset.le_sup (f := id) (Set.mem_toFinset.mpr ha)
  sSup_le := fun _ _ ha => Finset.sup_le fun _ hb => ha _ <| Set.mem_toFinset.mp hb
  sInf_le := fun _ _ ha => Finset.inf_le (Set.mem_toFinset.mpr ha)
  le_sInf := fun _ _ ha => Finset.le_inf fun _ hb => ha _ <| Set.mem_toFinset.mp hb
Finite Bounded Lattices are Complete
Informal description
For any finite type $\alpha$ equipped with a lattice structure and a bounded order (i.e., having both a greatest element $\top$ and a least element $\bot$), the lattice is complete. This means that every subset of $\alpha$ has both a supremum (least upper bound) and an infimum (greatest lower bound).
Fintype.toCompleteDistribLatticeMinimalAxioms abbrev
[DistribLattice α] [BoundedOrder α] : CompleteDistribLattice.MinimalAxioms α
Full source 
/-- A finite bounded distributive lattice is completely distributive. -/
noncomputable abbrev toCompleteDistribLatticeMinimalAxioms [DistribLattice α] [BoundedOrder α] :
    CompleteDistribLattice.MinimalAxioms α where
  __ := toCompleteLattice α
  iInf_sup_le_sup_sInf := fun a s => by
    convert (Finset.inf_sup_distrib_left s.toFinset id a).ge using 1
    rw [Finset.inf_eq_iInf]
    simp_rw [Set.mem_toFinset]
    rfl
  inf_sSup_le_iSup_inf := fun a s => by
    convert (Finset.sup_inf_distrib_left s.toFinset id a).le using 1
    rw [Finset.sup_eq_iSup]
    simp_rw [Set.mem_toFinset]
    rfl
Finite Bounded Distributive Lattices Satisfy Complete Distributivity Axioms
Informal description
For any finite type $\alpha$ equipped with a bounded distributive lattice structure (i.e., a lattice with both greatest and least elements where meet and join distribute over each other), the minimal axioms for a complete distributive lattice are satisfied. This means that finite meets distribute over arbitrary joins and finite joins distribute over arbitrary meets in $\alpha$.
Fintype.toCompleteDistribLattice abbrev
[DistribLattice α] [BoundedOrder α] : CompleteDistribLattice α
Full source 
/-- A finite bounded distributive lattice is completely distributive. -/
noncomputable abbrev toCompleteDistribLattice [DistribLattice α] [BoundedOrder α] :
    CompleteDistribLattice α := .ofMinimalAxioms (toCompleteDistribLatticeMinimalAxioms _)
Finite Bounded Distributive Lattices are Complete Distributive Lattices
Informal description
For any finite type $\alpha$ equipped with a bounded distributive lattice structure (i.e., a lattice with both greatest and least elements where meet and join distribute over each other), $\alpha$ forms a complete distributive lattice. This means that every subset of $\alpha$ has both a supremum (least upper bound) and an infimum (greatest lower bound), and the lattice satisfies the complete distributivity laws: 1. Finite meets distribute over arbitrary joins: $a \sqcap \left( \bigsqcup_{i \in I} f_i \right) = \bigsqcup_{i \in I} (a \sqcap f_i)$ 2. Finite joins distribute over arbitrary meets: $a \sqcup \left( \bigsqcap_{i \in I} f_i \right) = \bigsqcap_{i \in I} (a \sqcup f_i)$
Fintype.toCompleteLinearOrder abbrev
[LinearOrder α] [BoundedOrder α] : CompleteLinearOrder α
Full source 
/-- A finite bounded linear order is complete.

If the `α` is already a `BiheytingAlgebra`, then prefer to construct this instance manually using
`Fintype.toCompleteLattice` instead, to avoid creating a diamond with
`LinearOrder.toBiheytingAlgebra`. -/
noncomputable abbrev toCompleteLinearOrder
    [LinearOrder α] [BoundedOrder α] : CompleteLinearOrder α :=
  { toCompleteLattice α, ‹LinearOrder α›, LinearOrder.toBiheytingAlgebra with }
Finite Bounded Linear Orders are Complete
Informal description
For any finite type $\alpha$ equipped with a linear order and a bounded order (i.e., having both a greatest element $\top$ and a least element $\bot$), the linear order is complete. This means that every subset of $\alpha$ has both a supremum (least upper bound) and an infimum (greatest lower bound), and the order is total.
Fintype.toCompleteBooleanAlgebra abbrev
[BooleanAlgebra α] : CompleteBooleanAlgebra α
Full source 
/-- A finite boolean algebra is complete. -/
noncomputable abbrev toCompleteBooleanAlgebra [BooleanAlgebra α] : CompleteBooleanAlgebra α where
  __ := ‹BooleanAlgebra α›
  __ := Fintype.toCompleteDistribLattice α
  inf_sSup_le_iSup_inf _ _ := inf_sSup_eq.le
  iInf_sup_le_sup_sInf _ _ := sup_sInf_eq.ge
Finite Boolean Algebras are Complete
Informal description
For any finite type $\alpha$ equipped with a Boolean algebra structure, $\alpha$ forms a complete Boolean algebra. This means that every subset of $\alpha$ has both a supremum (least upper bound) and an infimum (greatest lower bound), and the algebra satisfies the complete distributivity laws: 1. Finite meets distribute over arbitrary joins: $a \sqcap \left( \bigsqcup_{i \in I} f_i \right) = \bigsqcup_{i \in I} (a \sqcap f_i)$ 2. Finite joins distribute over arbitrary meets: $a \sqcup \left( \bigsqcap_{i \in I} f_i \right) = \bigsqcap_{i \in I} (a \sqcup f_i)$
Fintype.toCompleteAtomicBooleanAlgebra abbrev
[BooleanAlgebra α] : CompleteAtomicBooleanAlgebra α
Full source 
/-- A finite boolean algebra is complete and atomic. -/
noncomputable abbrev toCompleteAtomicBooleanAlgebra [BooleanAlgebra α] :
    CompleteAtomicBooleanAlgebra α :=
  (toCompleteBooleanAlgebra α).toCompleteAtomicBooleanAlgebra
Finite Boolean Algebras are Complete and Atomic
Informal description
For any finite type $\alpha$ equipped with a Boolean algebra structure, $\alpha$ forms a complete atomic Boolean algebra. This means that every subset of $\alpha$ has both a supremum (least upper bound) and an infimum (greatest lower bound), the algebra satisfies the complete distributivity laws, and every element is the supremum of the atoms below it.
Fintype.toCompleteLatticeOfNonempty abbrev
[Lattice α] : CompleteLattice α
Full source 
/-- A nonempty finite lattice is complete. If the lattice is already a `BoundedOrder`, then use
`Fintype.toCompleteLattice` instead, as this gives definitional equality for `⊥` and `⊤`. -/
noncomputable abbrev toCompleteLatticeOfNonempty [Lattice α] : CompleteLattice α :=
  @toCompleteLattice _ _ _ <| @toBoundedOrder α _ ⟨Classical.arbitrary α⟩ _
Nonempty Finite Lattices are Complete
Informal description
Every nonempty finite lattice is a complete lattice. That is, for any nonempty finite type $\alpha$ equipped with a lattice structure, every subset of $\alpha$ has both a supremum (least upper bound) and an infimum (greatest lower bound).
Fintype.toCompleteLinearOrderOfNonempty abbrev
[LinearOrder α] : CompleteLinearOrder α
Full source 
/-- A nonempty finite linear order is complete. If the linear order is already a `BoundedOrder`,
then use `Fintype.toCompleteLinearOrder` instead, as this gives definitional equality for `⊥` and
`⊤`. -/
noncomputable abbrev toCompleteLinearOrderOfNonempty [LinearOrder α] : CompleteLinearOrder α := by
  let _ := toBoundedOrder α
  exact { toCompleteLatticeOfNonempty α, ‹LinearOrder α›, LinearOrder.toBiheytingAlgebra with }
Nonempty Finite Linear Orders are Complete
Informal description
Every nonempty finite type $\alpha$ equipped with a linear order structure is a complete linear order. That is, every subset of $\alpha$ has both a supremum (least upper bound) and an infimum (greatest lower bound), and the order is total.
Finite.exists_minimal_le theorem
[Finite α] (h : p a) : ∃ b, b ≤ a ∧ Minimal p b
Full source 
lemma Finite.exists_minimal_le [Finite α] (h : p a) : ∃ b, b ≤ a ∧ Minimal p b := by
  obtain ⟨b, ⟨hba, hb⟩, hbmin⟩ :=
    Set.Finite.exists_minimal_wrt id {x | x ≤ a ∧ p x} (Set.toFinite _) ⟨a, rfl.le, h⟩
  exact ⟨b, hba, hb, fun x hx hxb ↦ (hbmin x ⟨hxb.trans hba, hx⟩ hxb).le⟩
Existence of Minimal Elements Below a Given Element in Finite Preorders
Informal description
Let $\alpha$ be a finite type with a preorder, and let $p : \alpha \to \mathrm{Prop}$ be a predicate. For any element $a \in \alpha$ satisfying $p(a)$, there exists an element $b \in \alpha$ such that $b \leq a$ and $b$ is minimal with respect to $p$ (i.e., $p(b)$ holds and for any $c$ satisfying $p(c)$, if $c \leq b$ then $b \leq c$).
Finite.exists_le_maximal theorem
[Finite α] (h : p a) : ∃ b, a ≤ b ∧ Maximal p b
Full source 
lemma Finite.exists_le_maximal [Finite α] (h : p a) : ∃ b, a ≤ b ∧ Maximal p b :=
  Finite.exists_minimal_le (α := αᵒᵈ) h
Existence of Maximal Elements Above a Given Element in Finite Preorders
Informal description
Let $\alpha$ be a finite type with a preorder, and let $p : \alpha \to \mathrm{Prop}$ be a predicate. For any element $a \in \alpha$ satisfying $p(a)$, there exists an element $b \in \alpha$ such that $a \leq b$ and $b$ is maximal with respect to $p$ (i.e., $p(b)$ holds and for any $c$ satisfying $p(c)$, if $b \leq c$ then $c \leq b$).
Finset.exists_minimal_le theorem
(s : Finset α) (h : a ∈ s) : ∃ b, b ≤ a ∧ Minimal (· ∈ s) b
Full source 
lemma Finset.exists_minimal_le (s : Finset α) (h : a ∈ s) : ∃ b, b ≤ a ∧ Minimal (· ∈ s) b := by
  obtain ⟨⟨b, _⟩, lb, minb⟩ := @Finite.exists_minimal_le s _ ⟨a, h⟩ (·.1 ∈ s) _ h
  use b, lb; rwa [minimal_subtype, inf_idem] at minb
Existence of Minimal Elements Below Any Element in a Finite Set
Informal description
For any finite set $s$ of elements in a partially ordered type $\alpha$ and any element $a \in s$, there exists an element $b \in s$ such that $b \leq a$ and $b$ is minimal in $s$ (i.e., for any $c \in s$, if $c \leq b$ then $b \leq c$).
Finset.exists_le_maximal theorem
(s : Finset α) (h : a ∈ s) : ∃ b, a ≤ b ∧ Maximal (· ∈ s) b
Full source 
lemma Finset.exists_le_maximal (s : Finset α) (h : a ∈ s) : ∃ b, a ≤ b ∧ Maximal (· ∈ s) b :=
  s.exists_minimal_le (α := αᵒᵈ) h
Existence of Maximal Elements Above Any Element in a Finite Set
Informal description
For any finite set $s$ in a partially ordered type $\alpha$ and any element $a \in s$, there exists an element $b \in s$ such that $a \leq b$ and $b$ is maximal in $s$ (i.e., for any $c \in s$, if $b \leq c$ then $c \leq b$).
Set.Finite.exists_minimal_le theorem
{s : Set α} (hs : s.Finite) (h : a ∈ s) : ∃ b, b ≤ a ∧ Minimal (· ∈ s) b
Full source 
lemma Set.Finite.exists_minimal_le {s : Set α} (hs : s.Finite) (h : a ∈ s) :
    ∃ b, b ≤ a ∧ Minimal (· ∈ s) b := by
  obtain ⟨b, lb, minb⟩ := hs.toFinset.exists_minimal_le (hs.mem_toFinset.mpr h)
  use b, lb; simpa using minb
Existence of Minimal Elements Below Any Element in a Finite Set
Informal description
For any finite set $s$ in a partially ordered type $\alpha$ and any element $a \in s$, there exists an element $b \in s$ such that $b \leq a$ and $b$ is minimal in $s$ (i.e., for any $c \in s$, if $c \leq b$ then $b \leq c$).
Set.Finite.exists_le_maximal theorem
{s : Set α} (hs : s.Finite) (h : a ∈ s) : ∃ b, a ≤ b ∧ Maximal (· ∈ s) b
Full source 
lemma Set.Finite.exists_le_maximal {s : Set α} (hs : s.Finite) (h : a ∈ s) :
    ∃ b, a ≤ b ∧ Maximal (· ∈ s) b :=
  hs.exists_minimal_le (α := αᵒᵈ) h
Existence of Maximal Elements Above Any Element in a Finite Partially Ordered Set
Informal description
For any finite set $s$ in a partially ordered type $\alpha$ and any element $a \in s$, there exists an element $b \in s$ such that $a \leq b$ and $b$ is maximal in $s$ (i.e., for any $c \in s$, if $b \leq c$ then $c \leq b$).
Fin.completeLinearOrder instance
{n : ℕ} [NeZero n] : CompleteLinearOrder (Fin n)
Full source 
noncomputable instance Fin.completeLinearOrder {n : ℕ} [NeZero n] : CompleteLinearOrder (Fin n) :=
  Fintype.toCompleteLinearOrder _
Complete Linear Order on Finite Ordinals $\mathrm{Fin}(n)$
Informal description
For any nonzero natural number $n$, the finite type $\mathrm{Fin}(n)$ of natural numbers less than $n$ is equipped with a complete linear order structure. This means that every subset of $\mathrm{Fin}(n)$ has both a supremum (least upper bound) and an infimum (greatest lower bound), and the order is total.
Bool.completeBooleanAlgebra instance
: CompleteBooleanAlgebra Bool
Full source 
noncomputable instance Bool.completeBooleanAlgebra : CompleteBooleanAlgebra Bool :=
  Fintype.toCompleteBooleanAlgebra _
Complete Boolean Algebra Structure on Boolean Values
Informal description
The Boolean type `Bool` (with values `true` and `false`) forms a complete Boolean algebra, where: - The meet operation $\sqcap$ is logical AND, - The join operation $\sqcup$ is logical OR, - The complement operation $(\cdot)^\complement$ is logical NOT, - The top element $\top$ is `true`, - The bottom element $\bot$ is `false`, - Every subset has both a supremum and an infimum.
Bool.completeLinearOrder instance
: CompleteLinearOrder Bool
Full source 
noncomputable instance Bool.completeLinearOrder : CompleteLinearOrder Bool where
  __ := Fintype.toCompleteLattice _
  __ : BiheytingAlgebra Bool := inferInstance
  __ : LinearOrder Bool := inferInstance
Complete Linear Order on Booleans
Informal description
The boolean type `Bool` (with values `true` and `false`) is equipped with a complete linear order structure, where every subset has both a supremum and an infimum, and the order is total with `false < true`.
Bool.completeAtomicBooleanAlgebra instance
: CompleteAtomicBooleanAlgebra Bool
Full source 
noncomputable instance Bool.completeAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra Bool :=
  Fintype.toCompleteAtomicBooleanAlgebra _
Complete Atomic Boolean Algebra Structure on Boolean Values
Informal description
The Boolean type $\text{Bool}$ (with values $\text{true}$ and $\text{false}$) forms a complete atomic Boolean algebra, where: - The meet operation $\sqcap$ is logical AND, - The join operation $\sqcup$ is logical OR, - The complement operation $(\cdot)^\complement$ is logical NOT, - The top element $\top$ is $\text{true}$, - The bottom element $\bot$ is $\text{false}$, - Every subset has both a supremum and an infimum, and every element is the supremum of the atoms below it.
Directed.finite_set_le theorem
(D : Directed r f) {s : Set γ} (hs : s.Finite) : ∃ z, ∀ i ∈ s, r (f i) (f z)
Full source 
theorem Directed.finite_set_le (D : Directed r f) {s : Set γ} (hs : s.Finite) :
    ∃ z, ∀ i ∈ s, r (f i) (f z) := by
  convert D.finset_le hs.toFinset using 3; rw [Set.Finite.mem_toFinset]
Existence of Upper Bound for Directed Family on Finite Set
Informal description
Let $\alpha$ be a type with a transitive relation $r$, and let $f : \gamma \to \alpha$ be a directed family of elements with respect to $r$. For any finite subset $s \subseteq \gamma$, there exists an element $z \in \gamma$ such that for every $i \in s$, the relation $r(f(i), f(z))$ holds.
Directed.finite_le theorem
(D : Directed r f) (g : β → γ) : ∃ z, ∀ i, r (f (g i)) (f z)
Full source 
theorem Directed.finite_le (D : Directed r f) (g : β → γ) : ∃ z, ∀ i, r (f (g i)) (f z) := by
  classical
    obtain ⟨z, hz⟩ := D.finite_set_le (Set.finite_range g)
    exact ⟨z, fun i => hz (g i) ⟨i, rfl⟩⟩
Existence of Upper Bound for Directed Family under Finite Mapping
Informal description
Let $\alpha$ be a type with a transitive relation $r$, and let $f : \gamma \to \alpha$ be a directed family of elements with respect to $r$. For any function $g : \beta \to \gamma$ where $\beta$ is finite, there exists an element $z \in \gamma$ such that for every $i \in \beta$, the relation $r(f(g(i)), f(z))$ holds.
Finite.exists_le theorem
[IsDirected α (· ≤ ·)] (f : β → α) : ∃ M, ∀ i, f i ≤ M
Full source 
theorem Finite.exists_le [IsDirected α (· ≤ ·)] (f : β → α) : ∃ M, ∀ i, f i ≤ M :=
  directed_id.finite_le _
Existence of Upper Bound for Finite Families in Directed Preorders
Informal description
For any finite type $\beta$ and a function $f : \beta \to \alpha$ where $\alpha$ is a preorder with a directed $\leq$ relation, there exists an element $M \in \alpha$ such that $f(i) \leq M$ for all $i \in \beta$.
Finite.exists_ge theorem
[IsDirected α (· ≥ ·)] (f : β → α) : ∃ M, ∀ i, M ≤ f i
Full source 
theorem Finite.exists_ge [IsDirected α (· ≥ ·)] (f : β → α) : ∃ M, ∀ i, M ≤ f i :=
  directed_id.finite_le (r := (· ≥ ·)) _
Existence of Common Lower Bound for Finite Families in Directed Preorders
Informal description
Let $\alpha$ be a type with a directed relation $\geq$ (i.e., any two elements have a common lower bound), and let $f : \beta \to \alpha$ be a function where $\beta$ is a finite type. Then there exists an element $M \in \alpha$ such that $M \leq f(i)$ for all $i \in \beta$.
Set.Finite.exists_le theorem
[IsDirected α (· ≤ ·)] {s : Set α} (hs : s.Finite) : ∃ M, ∀ i ∈ s, i ≤ M
Full source 
theorem Set.Finite.exists_le [IsDirected α (· ≤ ·)] {s : Set α} (hs : s.Finite) :
    ∃ M, ∀ i ∈ s, i ≤ M :=
  directed_id.finite_set_le hs
Existence of Upper Bound for Finite Sets in Directed Preorders
Informal description
For any finite subset $s$ of a preordered type $\alpha$ where the relation $\leq$ is directed, there exists an upper bound $M \in \alpha$ such that $i \leq M$ for all $i \in s$.
Set.Finite.exists_ge theorem
[IsDirected α (· ≥ ·)] {s : Set α} (hs : s.Finite) : ∃ M, ∀ i ∈ s, M ≤ i
Full source 
theorem Set.Finite.exists_ge [IsDirected α (· ≥ ·)] {s : Set α} (hs : s.Finite) :
    ∃ M, ∀ i ∈ s, M ≤ i :=
  directed_id.finite_set_le (r := (· ≥ ·)) hs
Existence of Common Lower Bound for Finite Sets in Directed Preorders
Informal description
For any finite subset $s$ of a type $\alpha$ with a directed relation $\geq$ (i.e., every pair of elements has a common lower bound), there exists an element $M \in \alpha$ such that $M \leq i$ for all $i \in s$.
Finite.bddAbove_range theorem
[IsDirected α (· ≤ ·)] (f : β → α) : BddAbove (Set.range f)
Full source 
@[simp]
theorem Finite.bddAbove_range [IsDirected α (· ≤ ·)] (f : β → α) : BddAbove (Set.range f) := by
  obtain ⟨M, hM⟩ := Finite.exists_le f
  refine ⟨M, fun a ha => ?_⟩
  obtain ⟨b, rfl⟩ := ha
  exact hM b
Range of a Function from a Finite Type is Bounded Above in a Directed Preorder
Informal description
For any finite type $\beta$ and a function $f \colon \beta \to \alpha$ where $\alpha$ is a preorder with a directed $\leq$ relation, the range of $f$ is bounded above in $\alpha$.
Finite.bddBelow_range theorem
[IsDirected α (· ≥ ·)] (f : β → α) : BddBelow (Set.range f)
Full source 
@[simp]
theorem Finite.bddBelow_range [IsDirected α (· ≥ ·)] (f : β → α) : BddBelow (Set.range f) := by
  obtain ⟨M, hM⟩ := Finite.exists_ge f
  refine ⟨M, fun a ha => ?_⟩
  obtain ⟨b, rfl⟩ := ha
  exact hM b
Finite Range is Bounded Below in Directed Preorders
Informal description
Let $\alpha$ be a type with a directed relation $\geq$ (i.e., any two elements have a common lower bound), and let $f : \beta \to \alpha$ be a function where $\beta$ is a finite type. Then the range of $f$ is bounded below in $\alpha$.