isBasis_restrict_of_subset

Mathlib.Combinatorics.Matroid.Minor.Restrict

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

← MathLib Explorer

English

If I is a basis of M on X and X ⊆ Y, then (M|Y).IsBasis I X.

Русский

Если I является базисом M на X и X ⊆ Y, то (M|Y).IsBasis I X.

LaTeX

$$$ (M \\restriction Y).IsBasis I X $$$

Lean4

theorem isBasis_restrict_of_subset (hI : M.IsBasis I X) (hXY : X ⊆ Y) : (M ↾ Y).IsBasis I X := by
  rwa [← isBase_restrict_iff, M.restrict_restrict_eq hXY, isBase_restrict_iff]

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

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

Разделы

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

Аффилиация

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