freeOn_indep

Mathlib.Combinatorics.Matroid.Constructions

URI: https://scilib.ai/kg/mathlib#Matroid.freeOn_indep

English

If I ⊆ E then (freeOn E).Indep I.

Русский

Если I ⊆ E, то I независимо в freeOn(E).

LaTeX

$$$ \\text{If } I \\subseteq E, \\; (\\text{freeOn}(E)).Indep I $$$

Lean4

theorem freeOn_indep (hIE : I ⊆ E) : (freeOn E).Indep I :=
  freeOn_indep_iff.2 hIE

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

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

Разделы

Аффилиация

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