isLoop_isRestriction

Mathlib.Combinatorics.Matroid.Loop

URI: https://scilib.ai/kg/mathlib#Matroid.IsLoop.isLoop_isRestriction

English

If e is a loop in M, N ≤r M, and e ∈ N.E, then e is a loop in N.

Русский

Если e является петлей в M, N ≤r M и e ∈ N.E, то e является петлей в N.

LaTeX

$$$ (M.IsLoop e) \land (N \le_r M) \land (e \in N.E) \rightarrow N.IsLoop e $$$

Lean4

theorem isLoop_isRestriction (he : M.IsLoop e) (hNM : N ≤r M) (heN : e ∈ N.E) : N.IsLoop e :=
  (hNM.isLoop_iff).2 ⟨heN, he⟩

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

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

Разделы

Аффилиация

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