of_restrict

Mathlib.Combinatorics.Matroid.Loop

URI: https://scilib.ai/kg/mathlib#Matroid.IsNonloop.of_restrict

English

If the restricted matroid is nonloop at e, then e is a nonloop in the original matroid.

Русский

Если ограниченный матроид не петля в e, то e не петля в исходном матроиде.

LaTeX

$$$(M \restriction R).IsNonloop e \rightarrow M.IsNonloop e$$$

Lean4

theorem of_restrict {R : Set α} (h : (M ↾ R).IsNonloop e) : M.IsNonloop e :=
  (restrict_isNonloop_iff.1 h).1

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

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

Разделы

Аффилиация

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