English
A subset I of α ⊕ β is independent in the sum M.sum N iff its left preimage is independent in M and its right preimage is independent in N.
Русский
Подмножество I ⊆ α ⊕ β независимо в сумме M.sum N тогда и только тогда, когда его прообраз слева по Sum.inl независим в M, а прообраз справа по Sum.inr независим в N.
LaTeX
$$$$ (M.sum N).Indep I \iff M.Indep (\mathrm{preimage}(\mathrm{Sum.inl}) I) \land N.Indep (\mathrm{preimage}(\mathrm{Sum.inr}) I). $$$$
Lean4
@[simp]
theorem sum_indep_iff (M : Matroid α) (N : Matroid β) {I : Set (α ⊕ β)} :
(M.sum N).Indep I ↔ M.Indep (.inl ⁻¹' I) ∧ N.Indep (.inr ⁻¹' I) :=
by
simp only [Matroid.sum, mapEquiv_indep_iff, Equiv.sumCongr_symm, Equiv.sumCongr_apply, Equiv.symm_symm,
sigma_indep_iff, Bool.forall_bool]
convert Iff.rfl <;> simp [Set.ext_iff, Equiv.ulift, Equiv.sumEquivSigmaBool]
