trans — Mathlib

English

Let v1, v2, v3 be valuations. If v1 is equivalent to v2 and v2 is equivalent to v3, then v1 is equivalent to v3.

Русский

Пусть v1, v2, v3 — оценки. Если v1 эквивалентна v2 и v2 эквивалентна v3, то и v1 эквивалентна v3.

LaTeX

$$$ (v_1 \approx v_2) \rightarrow (v_2 \approx v_3) \rightarrow (v_1 \approx v_3) $$$

Lean4

@[trans]
theorem trans (h₁₂ : v₁.IsEquiv v₂) (h₂₃ : v₂.IsEquiv v₃) : v₁.IsEquiv v₃ := fun _ _ => Iff.trans (h₁₂ _ _) (h₂₃ _ _)

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