trans — Mathlib

English

If Q1 is equivalent to Q2 and Q2 is equivalent to Q3, then Q1 is equivalent to Q3.

Русский

Если Q1 эквивантна Q2, а Q2 эквивантна Q3, то и Q1 эквивалентна Q3.

LaTeX

$$$Q_1 \;\text{is equivalent to } Q_2\; \Rightarrow\; Q_2 \;\text{is equivalent to } Q_3\; \Rightarrow\; Q_1 \;\text{is equivalent to } Q_3$$$

Lean4

@[trans]
theorem trans (h : Q₁.Equivalent Q₂) (h' : Q₂.Equivalent Q₃) : Q₁.Equivalent Q₃ :=
  h'.elim <| h.elim fun f g => ⟨f.trans g⟩

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