ext — Mathlib

English

StieltjesFunction.ext asserts equality of two Stieltjes functions from equality of their values pointwise.

Русский

StieltjesFunction.ext утверждает равенство двух функций по значению на каждой точке.

LaTeX

$$$$\\forall f,g: StieltjesFunction, (\\forall x, f(x)=g(x)) \\Rightarrow f=g.$$$$

Lean4

@[ext]
theorem ext {f g : StieltjesFunction} (h : ∀ x, f x = g x) : f = g := by
  exact (StieltjesFunction.mk.injEq ..).mpr (funext h)

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