Similarity orderings

[Lew73b] [Sta68]

A SimilarityOrdering W is a centered family of preorders: for each center w₀, atCenter w₀ is the closeness Preorder ((atCenter w₀).le w₁ w₂ means w₁ is at least as close to w₀ as w₂). This replaces the former hand-rolled ternary relation closer with per-center reflexivity/transitivity fields — those are now just the Preorder axioms of atCenter w₀.

The closest worlds are mathlib's Minimal, and the Limit Assumption is Set.Finite.exists_minimal.

Key operations

• atCenter w₀ — the closeness preorder centered at w₀.
• closer w₀ w₁ w₂ — (atCenter w₀).le w₁ w₂, the ternary closeness relation.
• closestWorlds w₀ A — minimal elements of a Finset under closer w₀.
• isCentered — strong centering ([Lew73b]).
• ≤[sim, w₀] notation: w₁ ≤[sim, w₀] w₂ reads "w₁ is at least as similar to w₀ as w₂ is".

Structure

structure Core.Order.SimilarityOrdering (W : Type u_1) : Type u_1

A similarity ordering: a centered family of preorders. atCenter w₀ is the closeness preorder centered at w₀.

• atCenter : W → Preorder W

  The closeness preorder centered at each world.

• decClose (w₀ w₁ w₂ : W) : Decidable (w₁ ≤ w₂)

  Closeness is decidable at each center.

@[reducible]

def Core.Order.SimilarityOrdering.closer {W : Type u_1} (sim : SimilarityOrdering W) (w₀ w₁ w₂ : W) : Prop

closer w₀ w₁ w₂ means w₁ is at least as close to w₀ as w₂ is — the ≤ of the preorder centered at w₀.

Equations

• (w₁ ≤[sim,w₀] w₂) = (w₁ ≤ w₂)

@[implicit_reducible]

instance Core.Order.SimilarityOrdering.instDecidableCloser {W : Type u_1} (sim : SimilarityOrdering W) (w₀ w₁ w₂ : W) : Decidable (w₁ ≤[sim,w₀] w₂)

Equations

• sim.instDecidableCloser w₀ w₁ w₂ = sim.decClose w₀ w₁ w₂

theorem Core.Order.SimilarityOrdering.closer_refl {W : Type u_1} (sim : SimilarityOrdering W) (w₀ w : W) : w ≤[sim,w₀] w

Every world is at least as close to any center as itself.

theorem Core.Order.SimilarityOrdering.closer_trans {W : Type u_1} (sim : SimilarityOrdering W) (w₀ w₁ w₂ w₃ : W) : (w₁ ≤[sim,w₀] w₂) → (w₂ ≤[sim,w₀] w₃) → w₁ ≤[sim,w₀] w₃

Transitivity of closeness at a fixed center.

Constructors

def Core.Order.SimilarityOrdering.ofBool {W : Type u_1} (f : W → W → W → Bool) (hrefl : ∀ (w₀ w : W), f w₀ w w = true) (htrans : ∀ (w₀ w₁ w₂ w₃ : W), f w₀ w₁ w₂ = true → f w₀ w₂ w₃ = true → f w₀ w₁ w₃ = true) : SimilarityOrdering W

Construct a SimilarityOrdering from a Bool-valued function. Reflexivity and transitivity can typically be discharged by decide.

Equations

• One or more equations did not get rendered due to their size.

Centering

def Core.Order.SimilarityOrdering.isCentered {W : Type u_1} (sim : SimilarityOrdering W) : Prop

A strongly centered similarity ordering: every world is strictly closest to itself ([Lew73b]'s centering axiom).

Equations

• sim.isCentered = ∀ (w w' : W), w ≠ w' → (w ≤[sim,w] w') ∧ ¬w' ≤[sim,w] w

Closest worlds

def Core.Order.SimilarityOrdering.closestWorlds {W : Type u_1} [DecidableEq W] (sim : SimilarityOrdering W) (w₀ : W) (A : Finset W) : Finset W

The closest A-worlds to w₀: the minimal elements of A under the similarity preorder centered at w₀.

Equations

• sim.closestWorlds w₀ A = {w' ∈ A | ∀ w'' ∈ A, (w' ≤[sim,w₀] w'') ∨ ¬w'' ≤[sim,w₀] w'}

@[simp]

theorem Core.Order.SimilarityOrdering.closestWorlds_empty {W : Type u_1} [DecidableEq W] (sim : SimilarityOrdering W) (w₀ : W) : sim.closestWorlds w₀ ∅ = ∅

theorem Core.Order.SimilarityOrdering.closestWorlds_subset {W : Type u_1} [DecidableEq W] (sim : SimilarityOrdering W) (w₀ : W) (A : Finset W) : sim.closestWorlds w₀ A ⊆ A

theorem Core.Order.SimilarityOrdering.mem_closestWorlds {W : Type u_1} [DecidableEq W] (sim : SimilarityOrdering W) (w₀ : W) (A : Finset W) (w' : W) : w' ∈ sim.closestWorlds w₀ A ↔ w' ∈ A ∧ ∀ w'' ∈ A, (w' ≤[sim,w₀] w'') ∨ ¬w'' ≤[sim,w₀] w'

theorem Core.Order.SimilarityOrdering.mem_closestWorlds_of_subset {W : Type u_1} [DecidableEq W] (sim : SimilarityOrdering W) {w₀ w : W} {A B : Finset W} (hBA : B ⊆ A) (hw : w ∈ sim.closestWorlds w₀ A) (hwB : w ∈ B) : w ∈ sim.closestWorlds w₀ B

Closest-world membership is preserved when restricting to a subset.

theorem Core.Order.SimilarityOrdering.closestWorlds_nonempty {W : Type u_1} [DecidableEq W] (sim : SimilarityOrdering W) (w₀ : W) {A : Finset W} (hne : A.Nonempty) : (sim.closestWorlds w₀ A).Nonempty

Limit Assumption ([Lew73b]): every non-empty Finset has a closest world. Routes through Set.Finite.exists_minimal on the preorder centered at w₀.

Selection-function bridge primitives

def Core.Order.candidateSelections {W : Type u_1} (sim : SimilarityOrdering W) (domain : Set W) (w : W) (A : Set W) : Set W

Candidate selection set: the worlds in A ∩ domain that are minimal at w under the similarity ordering.

Equations

• Core.Order.candidateSelections sim domain w A = {w' : W | w' ∈ A ∩ domain ∧ ∀ w'' ∈ A ∩ domain, w' ≤[sim,w] w''}

def Core.Order.«term_≤[_,_]_» : Lean.TrailingParserDescr

Comparative-closeness notation ([Lew73b]): w₁ ≤[sim, w₀] w₂ reads "w₁ is at least as similar to w₀ as w₂ is".

Equations

• One or more equations did not get rendered due to their size.