ext — Mathlib

English

Let f, g be StarAlgEquiv between A and B over R. If f and g agree on every element of A, then f = g.

Русский

Пусть f, g — ⋆-алгебраические эквиваленты A → B над R. Если они совпадают на каждом элементе A, то f = g.

LaTeX

$$$$ \forall f,g : A \simeq_{\star}^{R} B,\ (\forall a : A, f(a) = g(a)) \Rightarrow f = g. $$$$

Lean4

@[ext]
theorem ext {f g : A ≃⋆ₐ[R] B} (h : ∀ a, f a = g a) : f = g :=
  DFunLike.ext f g h

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