English
If B is a base of M and B ∩ X is a basis of X, then the dual base on complements is a basis of X's complement.
Русский
Если B — база M, и B ∩ X является базисом X, то дуальный базис на дополнениях является базисом дополнения X.
LaTeX
$$∀ {α} {M : Matroid α} {B X : Set α}, M.IsBase B → M.IsBasis (B ∩ X) X → M.dual.IsBasis ((M.E \ B) ∩ (M.E \ X)) (M.E \ X)$$
Lean4
theorem compl_inter_isBasis_of_inter_isBasis (hB : M.IsBase B) (hBX : M.IsBasis (B ∩ X) X) :
M✶.IsBasis ((M.E \ B) ∩ (M.E \ X)) (M.E \ X) :=
by
refine Indep.isBasis_of_forall_insert ?_ inter_subset_right (fun e he ↦ ?_)
· rw [dual_indep_iff_exists]
exact ⟨B, hB, disjoint_of_subset_left inter_subset_left disjoint_sdiff_left⟩
simp only [diff_inter_self_eq_diff, mem_diff, not_and, not_not, imp_iff_right he.1.1] at he
simp_rw [dual_dep_iff_forall, insert_subset_iff, and_iff_right he.1.1,
and_iff_left (inter_subset_left.trans diff_subset)]
refine fun B' hB' ↦ by_contra (fun hem ↦ ?_)
rw [nonempty_iff_ne_empty, not_ne_iff, ← union_singleton, diff_inter_diff, union_inter_distrib_right, union_empty_iff,
singleton_inter_eq_empty, diff_eq, inter_right_comm, inter_eq_self_of_subset_right hB'.subset_ground, ← diff_eq,
diff_eq_empty] at hem
obtain ⟨f, hfb, hBf⟩ := hB.exchange hB' ⟨he.2, hem.2⟩
have hi : M.Indep (insert f (B ∩ X)) :=
by
refine hBf.indep.subset (insert_subset_insert ?_)
simp_rw [subset_diff, and_iff_right inter_subset_left, disjoint_singleton_right, mem_inter_iff,
iff_false_intro he.1.2, and_false, not_false_iff]
exact hfb.2 (hBX.mem_of_insert_indep (Or.elim (hem.1 hfb.1) (False.elim ∘ hfb.2) id) hi).1
