English
A set I is a basis with respect to X in disjointSigma iff for each i the restricted pair (I ∩ E_i, X ∩ E_i) is a basis for M_i, and the inclusions I ⊆ X ⊆ ⋃ E_i hold.
Русский
Набор I является базисом для пары (I,X) в disjointSigma тогда и только тогда, когда для каждого i пара (I ∩ E_i, X ∩ E_i) является базисом M_i и выполняются включения I ⊆ X ⊆ ⋃ E_i.
LaTeX
$$$$ (\mathrm{Matroid.disjointSigma} M h).IsBasis I X \iff (\forall i, (M i).IsBasis (I \cap (M i).E) (X \cap (M i).E)) \land I \subseteq X \land X \subseteq ⋃ i\,(M i).E. $$$$
Lean4
@[simp]
theorem disjointSigma_isBasis_iff {h I X} :
(Matroid.disjointSigma M h).IsBasis I X ↔
(∀ i, (M i).IsBasis (I ∩ (M i).E) (X ∩ (M i).E)) ∧ I ⊆ X ∧ X ⊆ ⋃ i, (M i).E :=
by simp [Matroid.disjointSigma, Function.Embedding.sigmaSet_preimage h]
