instSub

Mathlib.RingTheory.HahnSeries.Summable

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

Lean4

instance : Sub (SummableFamily Γ R α) where
  sub s
    s' :=
    { toFun := s - s'
      isPWO_iUnion_support' := by
        simp_rw [sub_eq_add_neg]
        exact (s + -s').isPWO_iUnion_support
      finite_co_support'
        g := by
        simp_rw [sub_eq_add_neg]
        exact (s + -s').finite_co_support' _ }

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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