restrict_loops_eq

Mathlib.Combinatorics.Matroid.Loop

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

English

If R ⊆ M.E, then (M|R).loops = M.loops ∩ R.

Русский

Если R ⊆ M.E, то (M|R).loops = M.loops ∩ R.

LaTeX

$$$ (M \restriction R).loops = M.loops \cap R $$$

Lean4

theorem restrict_loops_eq {R : Set α} (hR : R ⊆ M.E) : (M ↾ R).loops = M.loops ∩ R := by
  rw [restrict_loops_eq', diff_eq_empty.2 hR, union_empty]

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

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

Разделы

Аффилиация

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