trans — Mathlib

English

If s1 is equivalent to s2 and s2 is equivalent to s3, then s1 is equivalent to s3.

Русский

Если s1 эквивалентна s2 и s2 эквивалентна s3, тогда s1 эквивалентна s3.

LaTeX

$$$\\forall s_1\\ s_2\\ s_3,\\; s_1.Equivalent s_2 \\rightarrow s_2.Equivalent s_3 \\rightarrow s_1.Equivalent s_3.$$$

Lean4

@[trans]
theorem trans {s₁ s₂ s₃ : CompositionSeries X} (h₁ : Equivalent s₁ s₂) (h₂ : Equivalent s₂ s₃) : Equivalent s₁ s₃ :=
  ⟨h₁.choose.trans h₂.choose, fun i => iso_trans (h₁.choose_spec i) (h₂.choose_spec (h₁.choose i))⟩

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