disjointSigma_indep_iff — Mathlib

English

Independence in disjointSigma is characterized fiberwise: I is independent iff its fiber in each i is independent in Mi, and I is contained in the union of all Ei.

Русский

Независимость в disjointSigma характеризуется по волокнам: I независимо тогда и только тогда, когда его волокно в каждом i является независимым в Mi, и I ⊆ ⋃ i Ei.

LaTeX

$$$$ (\mathrm{Matroid.disjointSigma} M h).Indep I \iff (\forall i, (M i).Indep (I \cap (M i).E)) \land I \subseteq ⋃ i\,(M i).E. $$$$

Lean4

@[simp]
theorem disjointSigma_indep_iff {h I} :
    (Matroid.disjointSigma M h).Indep I ↔ (∀ i, (M i).Indep (I ∩ (M i).E)) ∧ I ⊆ ⋃ i, (M i).E := by
  simp [Matroid.disjointSigma, (Function.Embedding.sigmaSet_preimage h)]

Похожие утверждения