exists_isCircuit_of_mem_closure — Mathlib

English

If e ∈ closure X and e ∉ X, there exists a circuit C ⊆ insert e X with e ∈ C.

Русский

Если e ∈ closure X и e ∉ X, существует окружность C ⊆ insert e X такая, что e ∈ C.

LaTeX

$$$\\forall {\\alpha} {M : Matroid \\alpha} {X : Set α} {e : α}, e ∈ M.closure X \\to e \\notin X \\to ∃ C \\subseteq insert e X, M.IsCircuit C \\land e \\in C$$$

Lean4

theorem exists_isCircuit_of_mem_closure (he : e ∈ M.closure X) (heX : e ∉ X) :
    ∃ C ⊆ insert e X, M.IsCircuit C ∧ e ∈ C :=
  let ⟨I, hI⟩ := M.exists_isBasis' X
  ⟨_, (fundCircuit_subset_insert ..).trans (insert_subset_insert hI.subset),
    hI.indep.fundCircuit_isCircuit (by rwa [hI.closure_eq_closure]) (notMem_subset hI.subset heX),
    M.mem_fundCircuit e I⟩

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