coe_mk — Mathlib

English

Let f: P → Q be an affine map and h a continuity datum. The continuous affine map determined by f with this continuity data acts on each p ∈ P by f(p); in particular the underlying function of ⟨f, h⟩ is f.

Русский

Пусть f: P → Q — аффинная карта и дано значение непрерывности h. Непрерывная аффинная карта, полученная из f и h, действует на каждую точку p ∈ P как f(p); следовательно, функция, лежащая в основе ⟨f, h⟩, равна f.

LaTeX

$$$\big(\langle f,h \rangle : P \to Q\big) = f$$$

Lean4

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

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