congr_right

Mathlib.SetTheory.PGame.Basic

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.Identical.congr_right

English

If x ≡ y, then z ≡ x iff z ≡ y.

Русский

Если x идентичен y, то z идентичен x тогда и только тогда z идентичен y.

LaTeX

$$$ \forall {x y z : PGame}, x \equiv y \rightarrow (z \equiv x \iff z \equiv y)$$$

Lean4

theorem congr_right {x y z} (h : x ≡ y) : z ≡ x ↔ z ≡ y :=
  ⟨fun hz ↦ hz.trans h, fun hz ↦ hz.trans h.symm⟩

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

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

Разделы

Аффилиация

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