loopyOn_finite

Mathlib.Combinatorics.Matroid.Constructions

URI: https://scilib.ai/kg/mathlib#Matroid.Finite.loopyOn_finite

English

If E is finite, then loopyOn E is a finite matroid.

Русский

Если E — конечное, то loopyOn(E) — конечный матроид.

LaTeX

$$$ E.\\mathrm{Finite} \\Rightarrow \\mathrm{Matroid.Finite}(\\mathrm{loopyOn}(E))$$$

Lean4

theorem loopyOn_finite (hE : E.Finite) : Matroid.Finite (loopyOn E) :=
  ⟨hE⟩

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

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

Разделы

Аффилиация

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