insert_isBasis_iff_mem_closure

Mathlib.Combinatorics.Matroid.Closure

URI: https://scilib.ai/kg/mathlib#Matroid.Indep.insert_isBasis_iff_mem_closure

← MathLib Explorer

English

Given that inserting e into I yields a basis, e lies in the closure of I.

Русский

Если вставка e в I даёт базис, то e ∈ cl(I).

LaTeX

$$$M.IsBasis I (\\operatorname{insert} e I) \\iff e \\in \\operatorname{cl}(I)$$$

Lean4

theorem insert_isBasis_iff_mem_closure (hI : M.Indep I) : M.IsBasis I (insert e I) ↔ e ∈ M.closure I := by
  rw [hI.closure_eq_setOf_isBasis_insert, mem_setOf]

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

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

Разделы

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

Аффилиация

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