subset

Mathlib.Combinatorics.Matroid.Minor.Restrict

URI: https://scilib.ai/kg/mathlib#Matroid.IsRestriction.subset

English

If N ≤r M and R ⊆ M.E, then (N restricted to R) is a restriction of M restricted to R.

Русский

Если N ≤r M и R ⊆ M.E, то ограничение N до R является ограничением M до R.

LaTeX

$$$ N \\le_r M \\Rightarrow (N.restrict R) \\text{IsRestriction} (M.restrict R) $$$

Lean4

theorem subset (h : N ≤r M) : N.E ⊆ M.E := by obtain ⟨R, hR, rfl⟩ := h; exact hR

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

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

Разделы

Аффилиация

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