fundCocircuit_subset_insert_compl

English

The fundamental cocircuit is contained in the set insert e of the complement of B inside E.

Русский

Фундаментальная кококритика содержится в вставке e множества (E \ B).

LaTeX

$$$M.fundCocircuit(e,B) \subseteq \text{insert}(e, (M.E \setminus B))$$$

Lean4

theorem fundCocircuit_subset_insert_compl (M : Matroid α) (e : α) (B : Set α) :
    M.fundCocircuit e B ⊆ insert e (M.E \ B) :=
  fundCircuit_subset_insert ..

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