loops_subset

Mathlib.Combinatorics.Matroid.Loop

URI: https://scilib.ai/kg/mathlib#Matroid.IsFlat.loops_subset

English

If F is flat, then every loop lies in F; i.e., M.loops ⊆ F.

Русский

Если F плоское множество, то каждый цикл петли принадлежит F; то есть M.loops ⊆ F.

LaTeX

$$$ M.IsFlat F \Rightarrow M.loops \subseteq F $$$

Lean4

theorem loops_subset (hF : M.IsFlat F) : M.loops ⊆ F := fun _ he ↦ IsLoop.mem_of_isFlat he hF

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

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

Разделы

Аффилиация

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