closure_diff_singleton_ssubset

Mathlib.Combinatorics.Matroid.Closure

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

← MathLib Explorer

English

If e ∈ I, then M.closure(I \\ {e}) ⊂ M.closure(I).

Русский

Если e ∈ I, то closure(I \\ {e}) ⊊ closure(I).

LaTeX

$$$ \\text{If } hI : M.Indep I \\text{ and } e \\in I, \\; M.\\mathrm{closure}(I \\setminus \\{e\\}) \\subset M.\\mathrm{closure}(I) $$$

Lean4

theorem closure_diff_singleton_ssubset (hI : M.Indep I) (he : e ∈ I) : M.closure (I \ { e }) ⊂ M.closure I :=
  hI.closure_ssubset_closure <| by simpa

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

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

Разделы

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

Аффилиация

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