English
A base B for M.sum N corresponds to bases on each preimage: B is a base iff B_left and B_right are bases in M and N respectively on their fibers.
Русский
Базис B для M.sum N соответствует базисам на каждом прообразе: B является базисом тогда и только тогда, когда B_left и B_right являются базисами M и N на соответствующих волокнах.
LaTeX
$$$$ (M.sum N).IsBase B \iff \forall i, (M i).IsBase (\mathrm{preimage}(\mathrm{Sum.inl}) B). $$$$
Lean4
@[simp]
theorem sum_isBase_iff {M : Matroid α} {N : Matroid β} {B : Set (α ⊕ β)} :
(M.sum N).IsBase B ↔ M.IsBase (.inl ⁻¹' B) ∧ N.IsBase (.inr ⁻¹' B) :=
by
simp only [Matroid.sum, mapEquiv_isBase_iff, Equiv.sumCongr_symm, Equiv.sumCongr_apply, Equiv.symm_symm,
sigma_isBase_iff, Bool.forall_bool]
convert Iff.rfl <;> simp [Set.ext_iff, Equiv.ulift, Equiv.sumEquivSigmaBool]
