equiv

Mathlib.SetTheory.PGame.Order

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.Relabelling.equiv

English

If x and y are related by relabelling, then x is equivalent to y.

Русский

Если x и y связаны ребаллиннгом, то они эквивалентны.

LaTeX

$$$x \equiv_r y \Rightarrow x \approx y$$$

Lean4

/-- A relabelling lets us prove equivalence of games. -/
theorem equiv {x y : PGame} (r : x ≡r y) : x ≈ y :=
  ⟨r.le, r.ge⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru