coe_fn_mk — Mathlib

English

If f is a principal-segment embedding, then the function represented by PrincipalSeg.mk f t o is exactly f; i.e., its graph is f.

Русский

Если f — встраивание в виде главного сегмента, то функция, задаваемая PrincipalSeg.mk f t o, равна f.

LaTeX

$$$(\\mathrm{PrincipalSeg.mk}\\ f\\ t\\ o : \\alpha \\to \\beta) = f$; equivalently, $(\\mathrm{PrincipalSeg.mk}\\ f\\ t\\ o)(a) = f(a)$ for all $a$.$$

Lean4

@[simp]
theorem coe_fn_mk (f : r ↪r s) (t o) : (@PrincipalSeg.mk _ _ r s f t o : α → β) = f :=
  rfl

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