refl — Mathlib

English

The identity relation on games holds reflexively: every game is identical to itself.

Русский

Отношение тождества на играх сохраняет рефлексивность: каждая игра идентична самой себе.

LaTeX

$$$\forall x:\mathrm{PGame},\ x\equiv x.$$$

Lean4

@[refl, simp]
protected theorem refl (x) : x ≡ x :=
  PGame.recOn x fun _ _ _ _ IHL IHR ↦ ⟨Relator.BiTotal.refl IHL, Relator.BiTotal.refl IHR⟩

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