isBasis_iff_eq_diff_singleton — Mathlib

English

If C is a circuit, then IsBasis I C is equivalent to the existence of e ∈ C \ I with C = insert e I.

Русский

Если C — цикл, то IsBasis I C эквивалентно существованию e ∈ C \ I такого, что C = insert e I.

LaTeX

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

Lean4

theorem isBasis_iff_eq_diff_singleton (hC : M.IsCircuit C) : M.IsBasis I C ↔ ∃ e ∈ C, I = C \ { e } :=
  by
  refine ⟨fun h ↦ ?_, ?_⟩
  · obtain ⟨e, he⟩ := exists_of_ssubset (h.subset.ssubset_of_ne (by rintro rfl; exact hC.dep.not_indep h.indep))
    exact
      ⟨e, he.1, h.eq_of_subset_indep (hC.diff_singleton_indep he.1) (subset_diff_singleton h.subset he.2) diff_subset⟩
  rintro ⟨e, he, rfl⟩
  exact hC.diff_singleton_isBasis he

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