ext — Mathlib

English

Two affine maps are equal precisely when they have the same action on all points.

Русский

Два аффинных отображения равны тогда и только тогда, когда они совпадают на каждом элементе области определения.

LaTeX

$$$\forall p, f(p) = g(p) \Rightarrow f = g$$$

Lean4

/-- Two affine maps are equal if they coerce to the same function. -/
@[ext]
theorem ext {f g : P1 →ᵃ[k] P2} (h : ∀ p, f p = g p) : f = g :=
  DFunLike.ext _ _ h

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