trans

Mathlib.RingTheory.Valuation.Basic

URI: https://scilib.ai/kg/mathlib#AddValuation.IsEquiv.trans

English

Equivalence is transitive: if v1 IsEquiv v2 and v2 IsEquiv v3, then v1 IsEquiv v3.

Русский

Эквивалентность транзитивна: если v1 IsEquiv v2 и v2 IsEquiv v3, то v1 IsEquiv v3.

LaTeX

$$$$ v_1.IsEquiv v_2 \\rightarrow v_2.IsEquiv v_3 \\rightarrow v_1.IsEquiv v_3. $$$$

Lean4

@[trans]
theorem trans (h₁₂ : v₁.IsEquiv v₂) (h₂₃ : v₂.IsEquiv v₃) : v₁.IsEquiv v₃ :=
  Valuation.IsEquiv.trans h₁₂ h₂₃

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

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

Разделы

Аффилиация

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