equiv_trans — Mathlib

English

If b ≡ b' e and b' ≡ b'' e', then b ≡ b'' (e ∘ e').

Русский

Если базисы связаны через эквивалентности и отображения, то композиция также соответствует композиции базисов.

LaTeX

$$$(b.\\equiv b' e).\\text{trans} (b'.\\equiv b'' e') = b.\\equiv b'' (e \\circ e').$$$

Lean4

@[simp]
theorem equiv_trans {ι'' : Type*} (b'' : Basis ι'' R M'') (e : ι ≃ ι') (e' : ι' ≃ ι'') :
    (b.equiv b' e).trans (b'.equiv b'' e') = b.equiv b'' (e.trans e') :=
  b.ext' fun i => by simp

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