exists_isCircuit_subset — Mathlib

English

If X is a subset of the ground such that X is dependent, then there exists a circuit C with C ⊆ X.

Русский

Если X является зависимым подмножеством базисного множества, то внутри X существует окружность C, такая что C ⊆ X.

LaTeX

$$$\\forall X, M.Dep X \\Rightarrow \\exists C \\subseteq X\\, M.IsCircuit C$$$

Lean4

theorem exists_isCircuit_subset (hX : M.Dep X) : ∃ C, C ⊆ X ∧ M.IsCircuit C :=
  by
  obtain ⟨I, hI⟩ := M.exists_isBasis X
  obtain ⟨e, heX, heI⟩ := exists_of_ssubset (hI.subset.ssubset_of_ne (by rintro rfl; exact hI.indep.not_dep hX))
  exact
    ⟨M.fundCircuit e I, (M.fundCircuit_subset_insert e I).trans (insert_subset heX hI.subset),
      hI.indep.fundCircuit_isCircuit (hI.subset_closure heX) heI⟩

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