exists_mem_isCircuit_of_not_isColoop

English

If e ∈ E and e is not a coloop, there exists a circuit C with e ∈ C.

Русский

Если e ∈ E и e не колооп, существует цикл C, такой что e ∈ C.

LaTeX

$$$e \\in M.E \\land \\lnot M.IsColoop e \\Rightarrow \\exists C,\\ M.IsCircuit C \\land e \\in C$$$

Lean4

theorem exists_mem_isCircuit_of_not_isColoop (heE : e ∈ M.E) (he : ¬M.IsColoop e) : ∃ C, M.IsCircuit C ∧ e ∈ C :=
  by
  simp only [isColoop_iff_forall_mem_isBase, not_forall, exists_prop] at he
  obtain ⟨B, hB, heB⟩ := he
  exact ⟨M.fundCircuit e B, hB.fundCircuit_isCircuit heE heB, .inl rfl⟩

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