isBasis_closure

Mathlib.Combinatorics.Matroid.Closure

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

← MathLib Explorer

English

If I is independent, then I is a basis for its closure: I is a basis of cl(I).

Русский

Если I независим, то I является базисом своего замыкания: I является базисом cl(I).

LaTeX

$$$M.Indep I \\Rightarrow M.IsBasis I (\\operatorname{cl}(I))$$$

Lean4

theorem isBasis_closure (hI : M.Indep I) : M.IsBasis I (M.closure I) := by rw [hI.closure_eq_setOf_isBasis_insert];
  exact hI.isBasis_setOf_insert_isBasis

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

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

Разделы

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

Аффилиация

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