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

∫ Утверждение Mathlib

mem_ground

Mathlib.Combinatorics.Matroid.Loop

URI: https://scilib.ai/kg/mathlib#Matroid.IsLoop.mem_ground

← MathLib Explorer

English

If e is a loop in M, then e belongs to the ground E of M.

Русский

Если элемент e является петлей в M, то e принадлежит опорному множеству E матроида.

LaTeX

$$$M.IsLoop(e) \\Rightarrow e \\in M.E$$$

Lean4

@[aesop unsafe 20% (rule_sets := [Matroid])]
theorem mem_ground (he : M.IsLoop e) : e ∈ M.E :=
  closure_subset_ground M ∅ he

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

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

Разделы

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

Аффилиация

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

© 2026 SciLib Lab · ФИЦ ИУ РАН. Все права защищены. Контакты: info@scilibai.ru