mem_of_isFlat

Mathlib.Combinatorics.Matroid.Loop

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

English

If e is a loop and F is a flat, then e ∈ F.

Русский

Если e является петлей и F — плоскость (flat), то e принадлежит F.

LaTeX

$$$ M.IsLoop e \land M.IsFlat F \Rightarrow e \in F $$$

Lean4

theorem mem_of_isFlat (he : M.IsLoop e) {F : Set α} (hF : M.IsFlat F) : e ∈ F :=
  hF.closure ▸ he.mem_closure F

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

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

Разделы

Аффилиация

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