isLoop_iff_forall_mem_compl_isBase

English

For any matroid M and element e, M.IsLoop e holds if and only if e lies outside every base: for all bases B, e ∈ E \ B.

Русский

Для матроида M и элемента e условие M.IsLoop e эквивалентно тому, что e лежит вне каждого базиса: для всех базисов B выполняется e ∈ E \ B.

LaTeX

$$$ M.IsLoop e \iff \forall B\, (M.IsBase B \to e \in M.E \setminus B) $$$

Lean4

theorem isLoop_iff_forall_mem_compl_isBase : M.IsLoop e ↔ ∀ B, M.IsBase B → e ∈ M.E \ B :=
  (M.isLoop_tfae e).out 0 4

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