fundCocircuit_inter_eq — Mathlib

English

Let M be a matroid on α, B a subset of α, and e ∈ B. Then the intersection of the fundamental cocircuit of e with respect to B and B itself is exactly {e}.

Русский

Пусть M – матроид на α, B ⊆ α и e ∈ B. Тогда пересечение фундаментальной кококартe e относительно B с B равно {e}.

LaTeX

$$$ (M.fundCocircuit e B) \\cap B = \\{ e \\} $$$

Lean4

theorem fundCocircuit_inter_eq (M : Matroid α) {B : Set α} (he : e ∈ B) : (M.fundCocircuit e B) ∩ B = { e } :=
  by
  refine subset_antisymm ?_ (singleton_subset_iff.2 ⟨M.mem_fundCocircuit _ _, he⟩)
  refine (inter_subset_inter_left _ (M.fundCocircuit_subset_insert_compl _ _)).trans ?_
  simp +contextual

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