isBasis_inter_ground

Mathlib.Combinatorics.Matroid.Basic

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

English

If I is a Basis' I X, then I is a Basis I (X ∩ E).

Русский

Если I является Basis' I X, то I является Basis I (X ∩ E).

LaTeX

$$$ M.IsBasis' I X \Rightarrow M.IsBasis I (X \cap M.E) $$$

Lean4

theorem isBasis_inter_ground (hIX : M.IsBasis' I X) : M.IsBasis I (X ∩ M.E) :=
  isBasis'_iff_isBasis_inter_ground.mp hIX

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

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

Разделы

Аффилиация

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