congr_fun — Mathlib

English

If f and g are continuous homomorphisms between omega-complete ordered types and f = g, then they evaluate equally at every point.

Русский

Если f и g — непрерывные гомоморфизмы между ω-порядками и f = g, тогда их значения совпадают в каждой точке.

LaTeX

$$$\\forall {\\alpha, \\beta}, [\\OmegaCompletePartialOrder\\ \\alpha], [\\OmegaCompletePartialOrder\\ \\beta], {f,g : \\OmegaCompletePartialOrder.ContinuousHom\\ \\alpha\\ \\beta},\\ Eq\\ f\\ g \\Rightarrow\\ ∀ x:\\alpha,\\ Eq\\ (f\\,x) (g\\,x)$$$

Lean4

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

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