congr_left

Mathlib.SetTheory.PGame.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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