rel_trans'

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

URI: https://scilib.ai/kg/mathlib#ValuativeRel.rel_trans'

English

The transitivity of the valuative relation: from y ≤ᵥ z and x ≤ᵥ y, we get x ≤ᵥ z.

Русский

Транзитивность отношения: если y ≤ᵥ z и x ≤ᵥ y, то x ≤ᵥ z.

LaTeX

$$$ (h1 : y ≤\!_v z) (h2 : x ≤\!_v y) : x ≤\!_v z $$$

Lean4

theorem rel_trans' {x y z : R} (h1 : y ≤ᵥ z) (h2 : x ≤ᵥ y) : x ≤ᵥ z :=
  h2.trans h1

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

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

Разделы

Аффилиация

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