instIsEquivEquiv — Mathlib

English

There is an IsEquiv instance for PGame and the equivalence relation ≈ on pre-games; in particular, ≈ is an equivalence relation.

Русский

Существует отношение эквивалентности на предиграх; ≈ является эквивалентностью.

LaTeX

$$$\text{IsEquiv}(PGame, PGame.Equiv)$$$

Lean4

instance : IsEquiv _ PGame.Equiv where
  refl _ := ⟨le_rfl, le_rfl⟩
  trans := fun _ _ _ ⟨xy, yx⟩ ⟨yz, zy⟩ => ⟨xy.trans yz, zy.trans yx⟩
  symm _ _ := And.symm

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