isBasis_iff_insert_eq — Mathlib

English

For a circuit C, IsBasis I C is equivalent to 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 = insert e I$$$

Lean4

theorem isBasis_iff_insert_eq (hC : M.IsCircuit C) : M.IsBasis I C ↔ ∃ e ∈ C \ I, C = insert e I :=
  by
  rw [hC.isBasis_iff_eq_diff_singleton]
  refine ⟨fun ⟨e, he, hI⟩ ↦ ⟨e, ⟨he, fun heI ↦ (hI.subset heI).2 rfl⟩, ?_⟩, fun ⟨e, he, hC⟩ ↦ ⟨e, he.1, ?_⟩⟩
  · rw [hI, insert_diff_singleton, insert_eq_of_mem he]
  rw [hC, insert_diff_self_of_notMem he.2]

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