ext — Mathlib

English

If two bounded-order homomorphisms f and g from α to β agree at every element a ∈ α, then f and g are equal.

Русский

Если два отображения, сохраняющие порядок и границы, совпадают на каждом элементе множества α, то они совпадают как функции.

LaTeX

$$$\forall f,g:\mathrm{BoundedOrderHom}(\alpha,\beta),\; (\forall a\in \alpha,\ f(a)=g(a)) \implies f=g$.$$

Lean4

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

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