isCocircuit_inter_nontrivial — Mathlib

English

If C ∩ K is nonempty, then it is nontrivial.

Русский

Если C ∩ K непусто, то оно не тривиально (содержит по меньшей мере два элемента).

LaTeX

$$$(C \cap K) \neq \emptyset \Rightarrow (C \cap K) \text{ is nontrivial}$$$

Lean4

theorem isCocircuit_inter_nontrivial (hC : M.IsCircuit C) (hK : M.IsCocircuit K) (hCK : (C ∩ K).Nonempty) :
    (C ∩ K).Nontrivial := by
  obtain ⟨e, heCK⟩ := hCK
  rw [nontrivial_iff_ne_singleton heCK]
  exact hC.inter_isCocircuit_ne_singleton hK

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