ext — Mathlib

English

Two dilations are equal if and only if they agree on every input: if ∀x, f(x) = g(x) then f = g.

Русский

Две дилатации равны тогда и только тогда, когда они совпадают на каждом входе: если ∀x, f(x) = g(x), то f = g.

LaTeX

$$\forall f,g : α \toᵈ β, (\forall x, f(x) = g(x)) \Rightarrow f = g$$

Lean4

@[ext]
theorem ext {f g : α →ᵈ β} (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext f g h

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