coe_mk' — Mathlib

English

Extensionality for affine isometry equivalences: equality is determined pointwise.

Русский

Расщепление для аффинно-изометрических эквивалентностей: равенство определяется по значению на точках.

LaTeX

$$$$ \forall e,e' : P \simeq^{\mathrm{AI}} P, \ \bigl( \forall x, e(x) = e'(x) \bigr) \Rightarrow e = e'. $$$$

Lean4

@[simp]
theorem coe_mk' (e : P₁ → P₂) (e' : V₁ ≃ₗᵢ[𝕜] V₂) (p h) : ⇑(mk' e e' p h) = e :=
  rfl

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