ext

Mathlib.Probability.Kernel.Defs

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.Kernel.ext

English

Two kernels κ and η are equal if they coincide at every base point a: α, i.e., κ a = η a for all a.

Русский

Два ядра κ и η равны, если они совпадают при каждом элементе a: α, то есть κ a = η a для всех a.

LaTeX

$$$\\\\kappa = \\\\eta \\\\iff \\\\forall a, \\\\kappa a = \\\\eta a$$$

Lean4

@[ext]
theorem ext (h : ∀ a, κ a = η a) : κ = η :=
  DFunLike.ext _ _ h

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

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

Разделы

Аффилиация

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