English
A circuit and a cocircuit cannot meet in exactly one element.
Русский
Контур и кококрит не пересекаются в ровно одном элементе.
LaTeX
$$$\text{inter}(C,K) \neq \{e\}$ для любой $e$; если $M.IsCircuit(C)$ и $M.IsCocircuit(K)$, тогда $C \cap K$ не является одиночным.$$
Lean4
/-- A cocircuit and a circuit cannot meet in exactly one element. -/
theorem inter_isCocircuit_ne_singleton (hC : M.IsCircuit C) (hK : M.IsCocircuit K) : C ∩ K ≠ { e } :=
by
intro he
have heC : e ∈ C := (he.symm.subset rfl).1
simp_rw [isCocircuit_iff_minimal_compl_nonspanning, minimal_iff_forall_ssubset, not_not] at hK
have' hKe := hK.2 (t := K \ { e }) (diff_singleton_ssubset.2 (he.symm.subset rfl).2)
apply hK.1
rw [spanning_iff_ground_subset_closure]
nth_rw 1 [← hKe.closure_eq, diff_diff_eq_sdiff_union]
· refine (M.closure_subset_closure (subset_union_left (t := C))).trans ?_
rw [union_assoc, singleton_union, insert_eq_of_mem heC, ←
closure_union_congr_right (hC.closure_diff_singleton_eq e), union_eq_self_of_subset_right]
rw [← he, diff_self_inter]
exact diff_subset_diff_left hC.subset_ground
rw [← he]
exact inter_subset_left.trans hC.subset_ground
