Stable binary relations

def IsOrderPropRelWith {α : Type u_1} {β : Type u_2} (n : ℕ) (r : α → β → Prop) : Prop

Equations

• IsOrderPropRelWith n r = ∃ (a : Fin n → α), ∃ (b : Fin n → β), ∀ (i j : Fin n), i ≤ j ↔ r (a i) (b j)

def IsOrderPropRel {α : Type u_1} {β : Type u_2} (r : α → β → Prop) : Prop

Equations

• IsOrderPropRel r = ∃ (a : ℕ → α), ∃ (b : ℕ → β), ∀ (i j : ℕ), i ≤ j ↔ r (a i) (b j)

def IsStableRelWith {α : Type u_1} {β : Type u_2} (n : ℕ) (r : α → β → Prop) : Prop

Equations

• IsStableRelWith n r = ∀ (a : Fin n → α) (b : Fin n → β), ∃ (i : Fin n), ∃ (j : Fin n), ¬(i ≤ j ↔ r (a i) (b j))

def IsStableRel {α : Type u_1} {β : Type u_2} (r : α → β → Prop) : Prop

Equations

• IsStableRel r = ∀ (a : ℕ → α) (b : ℕ → β), ∃ (i : ℕ), ∃ (j : ℕ), ¬(i ≤ j ↔ r (a i) (b j))

def IsTreeBoundedRelWith {α : Type u_1} {β : Type u_2} (n : ℕ) (r : α → β → Prop) : Prop

Equations

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

@[simp]

theorem not_isStableRelWith {α : Type u_1} {β : Type u_2} {n : ℕ} {r : α → β → Prop} : ¬IsStableRelWith n r ↔ IsOrderPropRelWith n r

@[simp]

theorem not_isOrderPropRelWith {α : Type u_1} {β : Type u_2} {n : ℕ} {r : α → β → Prop} : ¬IsOrderPropRelWith n r ↔ IsStableRelWith n r

@[simp]

theorem not_isStableRel {α : Type u_1} {β : Type u_2} {r : α → β → Prop} : ¬IsStableRel r ↔ IsOrderPropRel r

@[simp]

theorem not_isOrderPropRel {α : Type u_1} {β : Type u_2} {r : α → β → Prop} : ¬IsOrderPropRel r ↔ IsStableRel r

theorem IsStableRelWith.isTreeBoundedRelWith {α : Type u_1} {β : Type u_2} {n : ℕ} {r : α → β → Prop} (hr : IsStableRelWith n r) : IsTreeBoundedRelWith (2 ^ n + 1) r

theorem IsTreeBoundedRelWith.isStableRelWith {α : Type u_1} {β : Type u_2} {n : ℕ} {r : α → β → Prop} (hr : IsTreeBoundedRelWith n r) : IsStableRelWith (2 ^ n) r