English
A pair (I,X) is a basis for the sum M.sum N precisely when for each i, (I∩E_i, X∩E_i) is a basis for M_i, reflecting the fiberwise nature of a basis in the sum.
Русский
Пара (I,X) является базисом суммы тогда и только тогда, когда для каждого i пара (I∩E_i, X∩E_i) является базисом M_i, что отражает волокну базиса в сумме.
LaTeX
$$$$ (M.sum N).IsBasis I X \iff \forall i, (M i).IsBasis (I \cap (M i).E) (X \cap (M i).E). $$$$
Lean4
@[simp]
theorem sum_isBasis_iff {M : Matroid α} {N : Matroid β} {I X : Set (α ⊕ β)} :
(M.sum N).IsBasis I X ↔ (M.IsBasis (Sum.inl ⁻¹' I) (Sum.inl ⁻¹' X) ∧ N.IsBasis (Sum.inr ⁻¹' I) (Sum.inr ⁻¹' X)) :=
by
simp only [Matroid.sum, mapEquiv_isBasis_iff, Equiv.sumCongr_symm, Equiv.sumCongr_apply, Equiv.symm_symm,
sigma_isBasis_iff, Bool.forall_bool, Equiv.sumEquivSigmaBool, Equiv.coe_fn_mk, Equiv.ulift]
convert Iff.rfl <;> exact ext <| by simp
