not_indep_of_mem

Mathlib.Combinatorics.Matroid.Loop

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

English

If e is a loop and e ∈ X, then X is not independent.

Русский

Если e — петля и e ∈ X, то X не является независимым.

LaTeX

$$$ M.IsLoop e \land e \in X \Rightarrow \neg M.Indep X $$$

Lean4

theorem not_indep_of_mem (he : M.IsLoop e) (h : e ∈ X) : ¬M.Indep X := fun hX ↦
  he.dep.not_indep (hX.subset (singleton_subset_iff.mpr h))

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

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

Разделы

Аффилиация

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