ext

Mathlib.MeasureTheory.Function.SimpleFunc

URI: https://scilib.ai/kg/mathlib#MeasureTheory.SimpleFunc.ext

English

If two simple functions agree at every point, they are equal.

Русский

Если две простые функции совпадают в каждой точке, то они равны.

LaTeX

$$$\\forall f,g : α \\to_\\mathrm{ₛ} β, (\\forall a, f(a)=g(a)) \\Rightarrow f=g$$$

Lean4

@[ext]
theorem ext {f g : α →ₛ β} (H : ∀ a, f a = g a) : f = g :=
  DFunLike.ext _ _ H

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru