Lifting a relation from points to sets

Two lifts of a relation r on α to Set α: the ∀∃ domination lift (dominationLift r A B: every b ∈ B is r-dominated by some a ∈ A — for a preorder this is the Smyth, or upper-powerdomain, preorder) and the injective matching lift (matchingLift: the dominators can be chosen distinct — the Gale order when r is a linear order). Two closure properties of set relations, RightUnion and DeterminedBySingletons, and the fact that the domination lift has both.

def RightUnion {α : Type u_1} (r : Set α → Set α → Prop) : Prop

Right-union: r A B → r A C → r A (B ∪ C).

Equations

• RightUnion r = ∀ (A B C : Set α), r A B → r A C → r A (B ∪ C)

def DeterminedBySingletons {α : Type u_1} (r : Set α → Set α → Prop) : Prop

Determination by singletons: r A {b} → ∃ a ∈ A, r {a} {b}.

Equations

• DeterminedBySingletons r = ∀ (A : Set α) (b : α), r A {b} → ∃ (a : α), a ∈ A ∧ r {a} {b}

def dominationLift {α : Type u_1} (r : α → α → Prop) (A B : Set α) : Prop

The domination lift: every b ∈ B is r-dominated by some a ∈ A.

Equations

• dominationLift r A B = ∀ (b : α), b ∈ B → ∃ (a : α), a ∈ A ∧ r a b

def matchingLift {α : Type u_1} (r : α → α → Prop) (A B : Set α) : Prop

The matching lift: some injection f : B ↪ A dominates pointwise.

Equations

• matchingLift r A B = ∃ (f : α → α), (∀ (b : α), b ∈ B → f b ∈ A ∧ r (f b) b) ∧ ∀ (b₁ b₂ : α), b₁ ∈ B → b₂ ∈ B → f b₁ = f b₂ → b₁ = b₂

theorem dominationLift_rightUnion {α : Type u_1} {r : α → α → Prop} : RightUnion (dominationLift r)

The domination lift is right-union closed.

theorem dominationLift_determinedBySingletons {α : Type u_1} {r : α → α → Prop} : DeterminedBySingletons (dominationLift r)

The domination lift is determined by singletons.