congr_fun — Mathlib

English

If two continuous maps f and g coincide as elements of C(X, Y) (i.e., f = g), then they have the same values at every point: f(x) = g(x) for all x ∈ X.

Русский

Если два непрерывных отображения f и g совпадают как элементы C(X, Y) (то есть f = g), то их значения совпадают при каждом x ∈ X: f(x) = g(x).

LaTeX

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

Lean4

/-- Deprecated. Use `DFunLike.congr_fun` instead. -/
protected theorem congr_fun {f g : C(X, Y)} (H : f = g) (x : X) : f x = g x :=
  H ▸ rfl

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