disjointSigma_isBase_iff — Mathlib

English

A base for disjointSigma is determined fiberwise: I is a base for all Mi on Ii, and subset relations hold globally with respect to unions of Ei.

Русский

Базис для disjointSigma определяется по волокнам: I является базисом для всех Mi на Ii, а отношение подмножеств выполняется глобально относительно объединений Ei.

LaTeX

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

Lean4

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

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