coe_comp_rangeRestrict — Mathlib

English

The composition of the inclusion from f.range to N with the restriction map equals f; i.e. (↑) ∘ (f.rangeRestrict) = f.

Русский

Композиция включения из образа в N с ограничивающей картой равна f.

LaTeX

$$$ (\uparrow) : f.range \to N \circ (f.rangeRestrict) = f$$$

Lean4

@[to_additive]
theorem coe_comp_rangeRestrict (f : G →* N) : ((↑) : f.range → N) ∘ (⇑f.rangeRestrict : G → f.range) = f :=
  rfl

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