mapEquiv — Mathlib

English

For any matroid M on α and equivalence f: α ≃ β, the ground set of the transported matroid equals the image of the original ground set under f.

Русский

Для матроида M на α и эквивалентности f: α ≃ β множество оснований переносимого матроида равняется образу исходного множества оснований под f.

LaTeX

$$$(M.mapEquiv f).E = f'' M.E$$$

Lean4

/-- Map `M : Matroid α` across an equivalence `α ≃ β` -/
def mapEquiv (M : Matroid α) (f : α ≃ β) : Matroid β :=
  M.mapEmbedding f.toEmbedding

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