restrict_isBase

Mathlib.Combinatorics.Matroid.Minor.Restrict

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

English

If I is a basis of M on X, then the restriction (M|X) has I as a base: (M|X).IsBase I.

Русский

Если I является базисом M на X, то ограничение (M|X) имеет I в качестве базиса: (M|X).IsBase I.

LaTeX

$$$ (M|X).IsBase I $$$

Lean4

theorem restrict_isBase (h : M.IsBasis I X) : (M ↾ X).IsBase I :=
  (isBase_restrict_iff h.subset_ground).2 h

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

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

Разделы

Аффилиация

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