trans

Mathlib.Topology.Inseparable

URI: https://scilib.ai/kg/mathlib#Inseparable.trans

English

If x ~ᵢ y and y ~ᵢ z, then x ~ᵢ z.

Русский

Если x ~ᵢ y и y ~ᵢ z, то x ~ᵢ z.

LaTeX

$$$(x \\sim_i y) \\land (y \\sim_i z) \\Rightarrow (x \\sim_i z).$$$

Lean4

@[trans]
nonrec theorem trans (h₁ : x ~ᵢ y) (h₂ : y ~ᵢ z) : x ~ᵢ z :=
  h₁.trans h₂

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

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

Разделы

Аффилиация

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