ground — Mathlib

English

For a matroid M and an equivalence e between ground sets, the ground set of the mapped matroid equals the target set E: (M.mapSetEquiv e).E = E.

Русский

Для матроида M и эквивалентности e между множествами оснований, множество оснований перенесённого матроида равно целевому множеству E: (M.mapSetEquiv e).E = E.

LaTeX

$$$ (M.mapSetEquiv e).E = E $$$

Lean4

@[simp]
theorem ground (M : Matroid α) {E : Set β} (e : M.E ≃ E) : (M.mapSetEquiv e).E = E :=
  rfl

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