isNonloop_of_mem — Mathlib

English

If M is a circuit on C with C nontrivial and e ∈ C, then e is a nonloop.

Русский

Если M образует циркит на C, C не тривиально и e ∈ C, то e — не петля.

LaTeX

$$$ \text{Given } hC : M.IsCircuit C,\ hC' : C.Nontrivial,\ he : e \in C, \text{ then } M.IsNonloop e $$$

Lean4

theorem isNonloop_of_mem (hC : M.IsCircuit C) (hC' : C.Nontrivial) (he : e ∈ C) : M.IsNonloop e :=
  isNonloop_of_not_isLoop (hC.subset_ground he) (fun hL ↦ by simp [hL.eq_of_isCircuit_mem hC he] at hC')

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