ext

Mathlib.RingTheory.HahnSeries.Summable

URI: https://scilib.ai/kg/mathlib#HahnSeries.SummableFamily.ext

English

Two summable families are equal if they agree componentwise.

Русский

Две суммируемые семейства равны, если их соответствующие компоненты равны.

LaTeX

$$$\\forall s,t:\\, \\text{SummableFamily},\\ (\\forall a, s(a)=t(a))\\Rightarrow s=t$$$

Lean4

@[ext]
theorem ext {s t : SummableFamily Γ R α} (h : ∀ a : α, s a = t a) : s = t :=
  DFunLike.ext s t h

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

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

Разделы

Аффилиация

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