liftEquiv_trans — Mathlib

English

The transitivity of liftEquiv gives a liftEquiv of the composite: (liftEquiv M i p).trans (liftEquiv M g p) = liftEquiv M (g ∘ i) p.

Русский

Транзитивность liftEquiv: композиция подъёмов даёт подъём по композиции: (liftEquiv M i p).trans (liftEquiv M g p) = liftEquiv M (g ∘ i) p.

LaTeX

$$$ (\operatorname{liftEquiv}\, M\, i\, p).\mathrm{trans}\,(\operatorname{liftEquiv}\, M\, g\, p) = \operatorname{liftEquiv}(M, g \circ i, p) $$$

Lean4

@[simp]
theorem liftEquiv_trans : (liftEquiv M i p).trans (liftEquiv M g p) = liftEquiv M (g.comp i) p :=
  Equiv.ext (liftEquiv_comp_apply i · g p)

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