sum'_isBase_iff — Mathlib

English

The sum' construction preserves finitary/IsBase status fiberwise: B is a base of sum' M exactly when each fiber B_i is a base of M_i.

Русский

Конструкция суммирования сохраняет статус базиса по волокнам: B является базисом суммы тогда, когда каждый волок B_i является базисом M_i.

LaTeX

$$$$ (\operatorname{sum}' M).IsBase B \iff \forall i, (M i).IsBase (\mathrm{Prod.mk} i^{-1}' B). $$$$

Lean4

@[simp]
theorem sum'_isBase_iff {B} : (Matroid.sum' M).IsBase B ↔ ∀ i, (M i).IsBase (Prod.mk i ⁻¹' B) :=
  by
  simp only [Matroid.sum', mapEquiv_isBase_iff, Equiv.sigmaEquivProd_symm_apply, sigma_isBase_iff]
  convert Iff.rfl
  ext
  simp

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