exists_isBase_subset

Mathlib.Combinatorics.Matroid.Closure

URI: https://scilib.ai/kg/mathlib#Matroid.Spanning.exists_isBase_subset

English

If S is spanning, there exists a base B with B ⊆ S and B a base of M.

Русский

Если S является порождающим, существует база B, такая что B ⊆ S и B — база M.

LaTeX

$$$$ M.Spanning S \Rightarrow \exists B, M.IsBase B ∧ B \subseteq S. $$$$

Lean4

theorem exists_isBase_subset (hS : M.Spanning S) : ∃ B, M.IsBase B ∧ B ⊆ S := by
  rwa [spanning_iff_exists_isBase_subset] at hS

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

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

Разделы

Аффилиация

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