sigma_isBase_iff — Mathlib

English

A base B of the sigma matroid corresponds to bases in each component: B is a base of the sum iff each preimage is a base in M_i.

Русский

Основание B матроидa сигма соответствует основаниям во всех компонентных матроидах: B является основанием суммы тогда и только тогда, когда предобраз B по каждому i образует основание в M_i.

LaTeX

$$$ (\\mathrm{Matroid}.sigma M).IsBase B \\,\\iff \\, \\forall i, (M(i)).IsBase (\\Sigma.mk i^{-1} B) $$$

Lean4

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

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