mk_coe — Mathlib

English

The continuous affine map built from an affine map f and a continuity datum h has as its affine-map component exactly f; i.e., the affine part of ⟨f,h⟩ is f.

Русский

Непрерывная аффинная карта, собранная из аффинной карты f и данных о непрерывности h, имеет в качестве аффинной части ровно f.

LaTeX

$$$\operatorname{toAffineMap}(\langle f,h\rangle) = f$$$

Lean4

@[simp]
theorem mk_coe (f : P →ᴬ[R] Q) (h) : (⟨(f : P →ᵃ[R] Q), h⟩ : P →ᴬ[R] Q) = f :=
  by
  ext
  rfl

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