ext — Mathlib

English

Two continuous multiplicative isomorphisms are equal if they agree on every element.

Русский

Две непрерывные мультипликативные эквивалентности равны, если на каждом элементе они совпадают.

LaTeX

$$$\forall f,g:\,M\simeq_{\text{mult}}N,\ \big(\forall x\in M,\ f(x)=g(x)\big)\Rightarrow f=g$$$

Lean4

/-- Two continuous multiplicative isomorphisms agree if they are defined by the
same underlying function. -/
@[to_additive (attr := ext) /-- Two continuous additive isomorphisms agree if they are defined by
    the same underlying function. -/
    ]
theorem ext {f g : M ≃ₜ* N} (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext f g h

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