isCocircuit_disjoint_or_nontrivial_inter

English

A cocircuit intersecting a circuit either is disjoint or nontrivial.

Русский

Пересечение кококритa и контура либо пусто, либо не тривиально.

LaTeX

$$$\text{Disjoint}(C,K) \lor (C \cap K)\text{ Nontrivial}$$$

Lean4

theorem isCocircuit_disjoint_or_nontrivial_inter (hC : M.IsCircuit C) (hK : M.IsCocircuit K) :
    Disjoint C K ∨ (C ∩ K).Nontrivial :=
  by
  rw [or_iff_not_imp_left, disjoint_iff_inter_eq_empty, ← ne_eq, ← nonempty_iff_ne_empty]
  exact hC.isCocircuit_inter_nontrivial hK

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