indep_restrict_of_subset

Mathlib.Combinatorics.Matroid.Minor.Restrict

URI: https://scilib.ai/kg/mathlib#Matroid.Indep.indep_restrict_of_subset

English

If N is a minor of M and I is independent in N, then I is independent in M.

Русский

Если N является минором M и I независимо в N, тогда I независимо в M.

LaTeX

$$(N ≤m M) ∧ N.Indep I ⇒ M.Indep I$$

Lean4

theorem indep_restrict_of_subset (h : M.Indep I) (hIR : I ⊆ R) : (M ↾ R).Indep I :=
  restrict_indep_iff.mpr ⟨h, hIR⟩

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

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

Разделы

Аффилиация

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