The criteria-derived preorder

This file defines the preorder that a family of criteria induces on a type. Given a relation sat : α → C → Prop and a set of criteria, Preorder.ofCriteria sat criteria ranks a below b when a satisfies every criterion of the set that b satisfies. It is the pullback of ⊇ along the map sending an element to the set of criteria it satisfies (ofCriteria_le_iff_subset).

Main declarations

• Preorder.ofCriteria: the criteria-derived preorder.
• Preorder.ofCriteria_empty: no criteria give the total order.
• Preorder.satisfied: the criteria that an element satisfies.

@[reducible]

def Preorder.ofCriteria {α : Type u_1} {C : Type u_2} (sat : α → C → Prop) (criteria : Set C) : Preorder α

The criteria-derived preorder ranks a below b when a satisfies every criterion in criteria that b satisfies.

Equations

• Preorder.ofCriteria sat criteria = { le := fun (a b : α) => ∀ c ∈ criteria, sat b c → sat a c, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

theorem Preorder.ofCriteria_le_iff {α : Type u_1} {C : Type u_2} (sat : α → C → Prop) (criteria : Set C) (a b : α) : a ≤ b ↔ ∀ c ∈ criteria, sat b c → sat a c

The criteria-derived order unfolds to its definition. The lemma is not tagged simp, so unfolding is opt-in.

theorem Preorder.ofCriteria_lt_iff {α : Type u_1} {C : Type u_2} (sat : α → C → Prop) (criteria : Set C) (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a

The strict criteria-derived order unfolds to the order and the failure of its converse.

theorem Preorder.ofCriteria_le_iff_subset {α : Type u_1} {C : Type u_2} (sat : α → C → Prop) (criteria : Set C) (a b : α) : a ≤ b ↔ {c : C | c ∈ criteria ∧ sat b c} ⊆ {c : C | c ∈ criteria ∧ sat a c}

The criteria-derived order is the pullback of ⊇ along the map sending a to the set of criteria it satisfies, with target (Set C)ᵒᵈ.

@[simp]

theorem Preorder.ofCriteria_empty {α : Type u_1} {C : Type u_2} (sat : α → C → Prop) : ofCriteria sat ∅ = ⊤

No criteria give the order relating every two elements.

The satisfied criteria as a valuation

def Preorder.satisfied {α : Type u_1} {C : Type u_2} (sat : α → C → Prop) (criteria : Set C) (a : α) : Set C

The criteria that a satisfies. The criteria-derived order is the pullback of ⊇ along this map (satisfied_subset_iff), so the minimal elements of the order are the MaximalFor elements of the map: the best elements are those satisfying a maximal set of criteria, with no order instance on the type.

Equations

• Preorder.satisfied sat criteria a = {c : C | c ∈ criteria ∧ sat a c}

@[simp]

theorem Preorder.mem_satisfied {α : Type u_1} {C : Type u_2} {sat : α → C → Prop} {criteria : Set C} {a : α} {c : C} : c ∈ satisfied sat criteria a ↔ c ∈ criteria ∧ sat a c

@[simp]

theorem Preorder.mem_satisfied_univ {α : Type u_1} {C : Type u_2} {sat : α → C → Prop} {a : α} {c : C} : c ∈ satisfied sat Set.univ a ↔ sat a c

theorem Preorder.satisfied_subset_iff {α : Type u_1} {C : Type u_2} (sat : α → C → Prop) (criteria : Set C) (a b : α) : satisfied sat criteria a ⊆ satisfied sat criteria b ↔ b ≤ a

@[instance_reducible]

instance Preorder.instDecidableLeSetSatisfiedOfPredMemListOfDecidableEq {α : Type u_1} {C : Type u_2} (sat : α → C → Prop) (l : List C) [DecidableEq C] [(a : α) → (c : C) → Decidable (sat a c)] (a b : α) : Decidable (satisfied sat {c : C | c ∈ l} a ⊆ satisfied sat {c : C | c ∈ l} b)

Equations

• Preorder.instDecidableLeSetSatisfiedOfPredMemListOfDecidableEq sat l a b = decidable_of_iff (∀ c ∈ l, sat a c → sat b c) ⋯