lift_of — Mathlib

English

The equality of two lifts is determined by equality on each summand, i.e., equality of the corresponding components fi on i determines the lift equality.

Русский

Равенство двух lift определяется равенством их соответствующих компонент по каждому i.

LaTeX

$$$ \\text{equality of lifts } \\iff \\forall i, fi = gi. $$$

Lean4

@[simp]
theorem lift_of {N} [Monoid N] (fi : ∀ i, M i →* N) {i} (m : M i) : lift fi (of m) = fi i m :=
  DFunLike.congr_fun (lift_comp_of ..) m

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