dual_rankPos_iff_exists_isCircuit

English

The dual rank position is equivalent to the existence of a circuit in M.

Русский

Положение ранга двойственного эквивалентно существованию контура в M.

LaTeX

$$$M^{\ast}.RankPos \iff \exists C, M.IsCircuit(C)$$$

Lean4

theorem dual_rankPos_iff_exists_isCircuit : M✶.RankPos ↔ ∃ C, M.IsCircuit C :=
  by
  rw [rankPos_iff, dual_isBase_iff, diff_empty, not_iff_comm, not_exists, ← ground_indep_iff_isBase,
    indep_iff_forall_subset_not_isCircuit]
  exact ⟨fun h C _ ↦ h C, fun h C hC ↦ h C hC.subset_ground hC⟩

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