freeOn_restrict

Mathlib.Combinatorics.Matroid.Constructions

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

English

If R is a subset of E, then restricting the matroid freeOn E to R yields the freeOn R: (freeOn E)|R = freeOn R when R ⊆ E.

Русский

Если R ⊆ E, то ограничение матроидa freeOn(E) к R равно freeOn(R): (freeOn E)|R = freeOn R при R ⊆ E.

LaTeX

$$$ (freeOn E)|_R = freeOn R \quad\text{whenever } R \subseteq E $$$

Lean4

theorem freeOn_restrict (h : R ⊆ E) : (freeOn E) ↾ R = freeOn R := by simp [h, eq_freeOn_iff]

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

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

Разделы

Аффилиация

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