liftEquiv_comp_apply — Mathlib

English

The liftEquiv operation respects composition: liftEquiv M g p (liftEquiv M i p j) = liftEquiv M (g ∘ i) p j.

Русский

Операция liftEquiv сохраняет композицию: liftEquiv M g p (liftEquiv M i p j) = liftEquiv M (g ∘ i) p j.

LaTeX

$$$ \operatorname{liftEquiv}(M,g,p)\big(\operatorname{liftEquiv}(M,i,p)(\,j\,)\big) = \operatorname{liftEquiv}(M, g \circ i, p)\, j $$$

Lean4

@[simp]
theorem liftEquiv_comp_apply : liftEquiv M g p (liftEquiv M i p j) = liftEquiv M (g.comp i) p j :=
  lift_lift i j g p

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