trans

Mathlib.SetTheory.ZFC.PSet

URI: https://scilib.ai/kg/mathlib#PSet.Equiv.trans

English

If x ≃ y and y ≃ z, then x ≃ z.

Русский

Если x эквивалентно y и y эквивалентно z, то x эквивалентно z.

LaTeX

$$Equiv x y → Equiv y z → Equiv x z$$

Lean4

@[trans]
protected theorem trans {x y z} (h1 : Equiv x y) (h2 : Equiv y z) : Equiv x z :=
  h1.euc h2.symm

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

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

Разделы

Аффилиация

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