English
For a family M: ι → Matroid α, a subset B of ι × α is a base of the sum if and only if for every i ∈ ι, the fiber B_i := { a ∈ α : (i,a) ∈ B } is a base of M_i.
Русский
Для семейства M: ι → Matroid α множество B ⊆ ι × α является базисом суммы тогда и только тогда, когда для каждого i ∈ ι подмножество B_i = { a ∈ α : (i,a) ∈ B } является базисом матроида M_i.
LaTeX
$$$$ (\operatorname{sum}' M).IsBase B \iff \forall i, (M i).IsBase (\mathrm{Prod.mk} i^{-1}' B). $$$$
Lean4
@[simp]
theorem sum'_indep_iff {I} : (Matroid.sum' M).Indep I ↔ ∀ i, (M i).Indep (Prod.mk i ⁻¹' I) :=
by
simp only [Matroid.sum', mapEquiv_indep_iff, Equiv.sigmaEquivProd_symm_apply, sigma_indep_iff]
convert Iff.rfl
ext
simp
