P24 — Mathlib

English

If x1, x2, y are surreal games that are numeric, then the relation P24 holds for (x1, x2, y).

Русский

Если x1, x2 и y — числовые сюрреал-игры, то выполняется свойство P24(x1, x2, y).

LaTeX

$$$$ \forall x_1\,x_2\,y\; (x_1.Numeric \land x_2.Numeric \land y.Numeric) \Rightarrow P24(x_1,x_2,y). $$$$

Lean4

theorem P24 (hx₁ : x₁.Numeric) (hx₂ : x₂.Numeric) (hy : y.Numeric) : P24 x₁ x₂ y :=
  main _ <| Args.numeric_P24.mpr ⟨hx₁, hx₂, hy⟩

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