insert_dep

Mathlib.Combinatorics.Matroid.Basic

URI: https://scilib.ai/kg/mathlib#Matroid.IsBasis.insert_dep

← MathLib Explorer

English

If I is a basis X and e ∈ X \ I, then I ∪ {e} is dependent.

Русский

Если I — база X и e ∈ X \ I, то I ∪ {e} зависимо.

LaTeX

$$$ M.IsBasis I X \land e \in X \setminus I \Rightarrow M.Dep (I \cup \{e\}) $$$

Lean4

theorem insert_dep (hI : M.IsBasis I X) (he : e ∈ X \ I) : M.Dep (insert e I) :=
  hI.dep_of_ssubset (ssubset_insert he.2) (insert_subset he.1 hI.subset)

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

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

Разделы

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

Аффилиация

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