isNonloop_of_mem_of_one_lt_card — Mathlib

English

If C is a circuit with encard > 1 and e ∈ C, then e is a nonloop.

Русский

Если C — циркит и encard(C) > 1 и e ∈ C, тогда e — не петля.

LaTeX

$$$ M.IsCircuit C \rightarrow 1 < C.encard \rightarrow e \in C \rightarrow M.IsNonloop e $$$

Lean4

theorem isNonloop_of_mem_of_one_lt_card (hC : M.IsCircuit C) (h : 1 < C.encard) (he : e ∈ C) : M.IsNonloop e :=
  by
  refine isNonloop_of_not_isLoop (hC.subset_ground he) (fun hlp ↦ ?_)
  rw [hlp.eq_of_isCircuit_mem hC he, encard_singleton] at h
  exact h.ne rfl

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