sigma_indep_iff — Mathlib

English

If every component matroid M_i is finitary, then the direct sum Matroid.sigma M is finitary.

Русский

Если каждый компонент матроид M_i конечный по определению (finitary), то сумма по индексу сигма M конечна.

LaTeX

$$$ \\bigl( \\forall i, (M(i)).Finitary \\bigr) \\Rightarrow (\\mathrm{Matroid}.sigma M).Finitary $$$

Lean4

@[simp]
theorem sigma_indep_iff {I} : (Matroid.sigma M).Indep I ↔ ∀ i, (M i).Indep (Sigma.mk i ⁻¹' I) :=
  Iff.rfl

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