isColoop_iff_forall_mem_compl_isCircuit

English

Under suitable rank positivity, e is a coloop iff e lies in every ground set element outside every circuit, i.e., e ∈ E \ C for all circuits C.

Русский

При условии положительной ранговости, e является колоопом тогда и только тогда, когда e лежит в E \ C для каждого цикла C.

LaTeX

$$$M.IsColoop e \\iff \\forall C\\, (M.IsCircuit C \\to e \\in M.E \\setminus C)$$$

Lean4

theorem isColoop_iff_forall_mem_compl_isCircuit [RankPos M✶] : M.IsColoop e ↔ ∀ C, M.IsCircuit C → e ∈ M.E \ C :=
  by
  by_cases he : e ∈ M.E
  · simp [isColoop_iff_forall_notMem_isCircuit, he]
  obtain ⟨C, hC⟩ := M.exists_isCircuit
  exact iff_of_false (fun h ↦ he h.mem_ground) fun h ↦ he (h C hC).1

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