diff_singleton_isBasis — Mathlib

English

For a circuit C and a set I, IsBasis I C holds iff there exists e ∈ C \ I with C = I ∪ {e}.

Русский

Для цикла C и множества I свойство IsBasis I C эквивалентно существованию e ∈ C \ I такое, что C = I ∪ {e}.

LaTeX

$$$M.IsCircuit C \rightarrow (M.IsBasis I C) \iff (\exists e \in C \setminus I,\ C = I \cup \{e\})$$$

Lean4

theorem diff_singleton_isBasis (hC : M.IsCircuit C) (he : e ∈ C) : M.IsBasis (C \ { e }) C :=
  by
  nth_rw 2 [← insert_eq_of_mem he]
  rw [← insert_diff_singleton, (hC.diff_singleton_indep he).isBasis_insert_iff, insert_diff_singleton,
    insert_eq_of_mem he]
  exact Or.inl hC.dep

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