disjointSigma_ground_eq — Mathlib

English

The ground of the disjointSigma matroid is the union of the grounds Ei of the components.

Русский

Основание матроидa disjointSigma есть объединение оснований компонентов.

LaTeX

$$$$ (\mathrm{Matroid.disjointSigma} M h).E = ⋃ i\, (M i).E. $$$$

Lean4

@[simp]
theorem disjointSigma_ground_eq {h} : (Matroid.disjointSigma M h).E = ⋃ i : ι, (M i).E := by ext;
  simp [Matroid.disjointSigma, mapEmbedding, restrictSubtype]

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