lift_of — Mathlib

English

The quotient construction equals the canonical embedding of the corresponding generator.

Русский

Квартирование совпадает с каноническим вложением соответствующего порождающего элемента.

LaTeX

$$$\\operatorname{Quot.mk}(\\text{DirectLimit.Eqv} f).r(\\text{of}(i,x)) = \\text{of}(R,i,x)$$$

Lean4

@[simp]
theorem lift_of {i} (x) : lift R ι G f g Hg (of R ι G f i x) = g i x :=
  DirectSum.toModule_lof R _ _

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