fundCocircuit_eq_of_notMem_ground

English

If e is not in the ground M.E of the matroid M, then the fundamental cocircuit of e with respect to X is exactly {e}.

Русский

Если e не принадлежит к базовому множеству M.E, то фундаментальная кококартe e относительно X равна {e}.

LaTeX

$$$ M.fundCocircuit e X = \{ e \} $$$

Lean4

/-- The fundamental cocircuit of `X` and `e` has the junk value `{e}` if `e ∉ M.E` -/
theorem fundCocircuit_eq_of_notMem_ground (X : Set α) (he : e ∉ M.E) : M.fundCocircuit e X = { e } := by
  rwa [fundCocircuit, fundCircuit_eq_of_notMem_ground]

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