contractElem_isCircuit — Mathlib

English

If C is a circuit and e ∈ C with C nontrivial, then contracting by {e} yields a circuit on C \ {e}: (M / {e}).IsCircuit(C \ {e}).

Русский

Если C — цикл и e ∈ C, и C не тривиален, то сжатие по {e} дает цикл на C \ {e}: (M / {e}).IsCircuit(C \ {e}).

LaTeX

$$(M / \{e\}).IsCircuit(C \ {e})$$

Lean4

theorem contractElem_isCircuit (hC : M.IsCircuit C) (hnt : C.Nontrivial) (heC : e ∈ C) :
    (M ／ { e }).IsCircuit (C \ { e }) :=
  hC.contract_isCircuit (ssubset_of_ne_of_subset hnt.ne_singleton.symm (by simpa))

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