freeOn_indep_iff

Mathlib.Combinatorics.Matroid.Constructions

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

English

(freeOn(E)).Indep I iff I ⊆ E.

Русский

Матроид freeOn(E) независим относительно I тогда и только тогда, когда I ⊆ E.

LaTeX

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

Lean4

@[simp]
theorem freeOn_indep_iff : (freeOn E).Indep I ↔ I ⊆ E := by simp [indep_iff]

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

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

Разделы

Аффилиация

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