exists_mem_isCocircuit — Mathlib

English

If e is a nonloop, there exists a cocircuit K containing e.

Русский

Если e не петля, существует кококруг K, содержащий e.

LaTeX

$$$\forall e, M.IsNonloop e \rightarrow \exists K, M.IsCocircuit K \land e \in K$$$

Lean4

theorem exists_mem_isCocircuit (he : M.IsNonloop e) : ∃ K, M.IsCocircuit K ∧ e ∈ K :=
  by
  obtain ⟨B, hB, heB⟩ := he.exists_mem_isBase
  exact ⟨_, fundCocircuit_isCocircuit heB hB, mem_fundCocircuit M e B⟩

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