not_isBasis_of_ssubset

Mathlib.Combinatorics.Matroid.Basic

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

← MathLib Explorer

English

If J is a strict subset of I and I is a basis of X, then J cannot be a basis of X.

Русский

Если J строгий подмножество I и I — база X, тогда J не может быть базой X.

LaTeX

$$$ M.IsBasis I X \land J \subsetneq I \Rightarrow \neg M.IsBasis J X $$$

Lean4

theorem not_isBasis_of_ssubset (hI : M.IsBasis I X) (hJI : J ⊂ I) : ¬M.IsBasis J X := fun h ↦
  hJI.ne (h.eq_of_subset_indep hI.indep hJI.subset hI.subset)

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

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

Разделы

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

Аффилиация

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