sigma_ground_eq — Mathlib

English

The ground set of the sigma matroid equals the sigma of the ground sets: E((sigma M)) = univ.sigma (i ↦ E(M_i)).

Русский

Множество оснований σ-матроида совпадает с сигма-образом множеств-подмножеств E каждого компонента.

LaTeX

$$$ (\\mathrm{sigma}\,M).E = \\mathrm{univ}.\\sigma (i \\mapsto (M_i).E) $$$

Lean4

@[simp]
theorem sigma_ground_eq : (Matroid.sigma M).E = univ.sigma fun i ↦ (M i).E :=
  rfl

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