mapEquiv_ground_eq — Mathlib

English

The matroid obtained by mapping M along an equivalence f is the same as mapping along the embedding underlying f.

Русский

Матроид, полученный из M по переносу через эквивалентность f, совпадает с матроидом, полученным перенесением через вложение, связанное с f.

LaTeX

$$$M.mapEquiv f = M.mapEmbedding f.toEmbedding$$$

Lean4

@[simp]
theorem mapEquiv_ground_eq (M : Matroid α) (f : α ≃ β) : (M.mapEquiv f).E = f '' M.E :=
  rfl

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