congr_fun — Mathlib

English

If f and g are dilations and f = g, then for every x, f(x) = g(x). More generally, equal dilations coincide pointwise.

Русский

Если дилатации f и g равны, то для каждого x выполняется f(x) = g(x). В общем случае равные дилатации совпадают по значению на каждой точке.

LaTeX

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

Lean4

protected theorem congr_fun {f g : α →ᵈ β} (h : f = g) (x : α) : f x = g x :=
  DFunLike.congr_fun h x

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