Documentation

Linglib.Core.Order.Minimals

Minimal elements under a preorder given as a term #

This file defines the set of minimal elements of a set under a preorder that is passed as a term rather than found by instance resolution. Mathlib's Minimal reads the order from the LE instance of the type, which does not fit a setting where many preorders on one type are in play and the preorder is itself data, as with the lattice of preorders on a type. The definition here unfolds to Minimal for the membership predicate, so the lemmas of Mathlib.Order.Minimal apply after letI := p.

Main declarations #

source
def Preorder.minimals {α : Type u_1} (p : Preorder α) (s : Set α) :
Set α

The minimal elements of s under the preorder p.

Equations
  • p.minimals s = {a : α | Minimal (fun (x : α) => x ∈ s) a}
Instances For
    source
    theorem Preorder.mem_minimals_iff {α : Type u_1} {p : Preorder α} {s : Set α} {a : α} :
    a ∈ p.minimals s ↔ a ∈ s ∧ ∀ ⦃b : α⦄, b ∈ s → b ≤ a → a ≤ b
    source
    theorem Preorder.minimals_subset {α : Type u_1} (p : Preorder α) (s : Set α) :
    p.minimals s ⊆ s
    source
    @[simp]
    theorem Preorder.minimals_empty {α : Type u_1} (p : Preorder α) :
    p.minimals ∅ = ∅
    source
    theorem Preorder.minimals_union_subset {α : Type u_1} {p : Preorder α} {s t : Set α} :
    p.minimals (s ∪ t) ⊆ p.minimals s ∪ p.minimals t

    A minimal element of a union is a minimal element of one of its parts.

    source
    theorem Preorder.mem_minimals_of_subset {α : Type u_1} {p : Preorder α} {s t : Set α} {a : α} (h : s ⊆ t) (ha : a ∈ p.minimals t) (has : a ∈ s) :
    a ∈ p.minimals s

    An element minimal in a set is minimal in any subset that contains it.

    source
    theorem Preorder.minimals_congr {α : Type u_1} {p : Preorder α} {s : Set α} {q : Preorder α} (h : ∀ a ∈ s, ∀ b ∈ s, a ≤ b ↔ a ≤ b) :
    p.minimals s = q.minimals s

    Two preorders that agree on a set have the same minimal elements of it.

    source
    theorem Preorder.minimals_eq_of_lt_iff {α : Type u_1} {p : Preorder α} {s : Set α} {q : Preorder α} (h : ∀ (a b : α), a < b ↔ a < b) :
    p.minimals s = q.minimals s

    The minimal elements of a set depend only on the strict order.

    source
    @[simp]
    theorem Preorder.minimals_top {α : Type u_1} (s : Set α) :
    ⊤.minimals s = s

    Under the preorder that relates every two elements, every element of a set is minimal.

    source
    theorem Preorder.exists_le_mem_minimals {α : Type u_1} {p : Preorder α} {s : Set α} {a : α} (hp : WellFounded LT.lt) (ha : a ∈ s) :
    ∃ b ∈ p.minimals s, b ≤ a

    Under a well-founded strict order every element of a set lies above a minimal element of the set.

    source
    theorem Preorder.mem_minimals_iff_forall_le {α : Type u_1} {p : Preorder α} {s : Set α} {a : α} (hp : Std.Total LE.le) :
    a ∈ p.minimals s ↔ a ∈ s ∧ ∀ b ∈ s, a ≤ b

    Under a total preorder the minimal elements of a set are its least elements.

    source
    theorem Preorder.mem_minimals_pair {α : Type u_1} {p : Preorder α} {a : α} (hp : Std.Total LE.le) {b : α} :
    a ∈ p.minimals {a, b} ↔ a ≤ b

    Under a total preorder an element is minimal in a pair exactly when it is below the other element.

    source
    theorem Preorder.minimals_nonempty {α : Type u_1} {s : Set α} [Finite α] (p : Preorder α) (hs : s.Nonempty) :
    (p.minimals s).Nonempty

    On a finite type every nonempty set has a minimal element.

    source
    theorem Preorder.minimals_nonempty_of_finite {α : Type u_1} {s : Set α} (p : Preorder α) (hfin : s.Finite) (hs : s.Nonempty) :
    (p.minimals s).Nonempty

    Every nonempty finite set has a minimal element.

    source
    @[instance_reducible]
    instance Preorder.instDecidableMemSetMinimalsOfFintypeOfDecidableRelLeOfDecidablePred {α : Type u_1} [Fintype α] (p : Preorder α) [DecidableRel LE.le] (s : Set α) [DecidablePred fun (x : α) => x ∈ s] (a : α) :
    Decidable (a ∈ p.minimals s)
    Equations
    source
    @[instance_reducible]
    instance Preorder.instDecidableMinimalOfFintypeOfDecidableLEOfDecidablePred_linglib {β : Type u_2} [Preorder β] [Fintype β] [DecidableLE β] {P : β → Prop} [DecidablePred P] (b : β) :
    Decidable (Minimal P b)
    Equations

    Preorders pulled back along a map #

    source
    @[simp]
    theorem Preorder.lift_le_iff {α : Type u_1} {β : Type u_2} (f : α → β) [Preorder β] {a b : α} :
    a ≤ b ↔ f a ≤ f b
    source
    @[simp]
    theorem Preorder.lift_lt_iff {α : Type u_1} {β : Type u_2} (f : α → β) [Preorder β] {a b : α} :
    a < b ↔ f a < f b
    source
    @[instance_reducible]
    instance Preorder.instDecidableRelLeOfDecidableLE_linglib {α : Type u_1} {β : Type u_2} (f : α → β) [Preorder β] [DecidableLE β] :
    DecidableRel LE.le
    Equations
    source
    @[instance_reducible]
    instance Preorder.instDecidableRelLtOfDecidableLT_linglib {α : Type u_1} {β : Type u_2} (f : α → β) [Preorder β] [DecidableLT β] :
    DecidableRel LT.lt
    Equations
    source
    theorem Preorder.total_lift {α : Type u_1} {β : Type u_2} (f : α → β) [LinearOrder β] :
    Std.Total LE.le

    The pullback of a linear order is total.

    source
    theorem Preorder.mem_minimals_lift {α : Type u_1} {s : Set α} {a : α} {β : Type u_2} (f : α → β) [LinearOrder β] :
    a ∈ (lift f).minimals s ↔ a ∈ s ∧ ∀ b ∈ s, f a ≤ f b

    The minimal elements under the pullback of a linear order are the elements of least value.

    source
    theorem Preorder.minimals_ofCriteria_eq {α : Type u_1} {s : Set α} {C : Type u_2} {sat : α → C → Prop} {criteria : Set C} (hex : ∃ a ∈ s, ∀ c ∈ criteria, sat a c) :
    (ofCriteria sat criteria).minimals s = {a : α | a ∈ s ∧ ∀ c ∈ criteria, sat a c}

    Under a criteria-derived preorder, when some element of the set satisfies every criterion, the minimal elements are exactly those that do.