diff_singleton_indep — Mathlib

English

If C is a circuit and e ∈ C, then removing e from C yields an independent set: C \ {e} is independent.

Русский

Если C — цикл, и e ∈ C, то исключение e из C даёт независимое множество: C \ {e} независимо.

LaTeX

$$$M.IsCircuit(C)\;\wedge\; e\in C\Rightarrow M.Indep(C\setminus\{e\})$$$

Lean4

theorem diff_singleton_indep (hC : M.IsCircuit C) (he : e ∈ C) : M.Indep (C \ { e }) :=
  hC.ssubset_indep (diff_singleton_ssubset.2 he)

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