Theorems · Theorem · order theory

Acc.prod_gameAdd

∀ {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} {a : α} {b : β},
  Acc rα a → Acc rβ b → Acc (Prod.GameAdd rα rβ) (a, b)

If a is accessible under rα and b is accessible under rβ, then (a, b) is accessible under Prod.GameAdd rα rβ. Notice that Prod.lexAccessible requires the stronger condition ∀ b, Acc rβ b.

Defined in

Mathlib.Order.GameAdd

Cited by

3 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms