insert_isCircuit_of_forall_of_nontrivial

English

If C is a circuit and e ∈ C, then C \ {e} is a basis of C.

Русский

Если C — цикл и e ∈ C, тогда C \ {e} является базисом C.

LaTeX

$$$M.IsCircuit(C) \wedge e \in C \Rightarrow M.IsBasis(C \ {e}) C$$$

Lean4

theorem insert_isCircuit_of_forall_of_nontrivial (hI : M.Indep I) (hInt : I.Nontrivial) (he : e ∈ M.closure I)
    (h : ∀ f ∈ I, e ∉ M.closure (I \ { f })) : M.IsCircuit (insert e I) :=
  by
  refine hI.insert_isCircuit_of_forall (fun heI ↦ ?_) he h
  obtain ⟨f, hf, hne⟩ := hInt.exists_ne e
  exact h f hf (mem_closure_of_mem' _ (by simp [heI, hne.symm]))

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