sum'

Mathlib.Combinatorics.Matroid.Sum

URI: https://scilib.ai/kg/mathlib#Matroid.Finitary.sum'

English

If every M_i is Finitary, then the sum' of the family is Finitary.

Русский

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

LaTeX

$$$$ (\forall i, (M i).Finitary) \Rightarrow (\operatorname{sum}' M).Finitary. $$$$

Lean4

theorem sum' (h : ∀ i, (M i).Finitary) : (Matroid.sum' M).Finitary :=
  by
  have := Finitary.sigma h
  rw [Matroid.sum']
  infer_instance

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

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

Разделы

Аффилиация

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