forall_relations — Mathlib

English

A property P of relations of any arity holds for all n if and only if it holds for the 2-ary relation le.

Русский

Свойство P, зависящее от отношения произвольной арности, равно истинному для всех n тогда, когда оно истинно для 2-арности le.

LaTeX

$$$ (\\forall {n} (R), P n R) \\iff P 2 . le $$$

Lean4

@[simp]
theorem forall_relations {P : ∀ (n) (_ : Language.order.Relations n), Prop} : (∀ {n} (R), P n R) ↔ P 2 .le :=
  ⟨fun h => h _, fun h n R =>
    match n, R with
    | 2, .le => h⟩

Похожие утверждения