comapOn — Mathlib

English

The comapOn construction is the pullback of a matroid on β by f to α, restricted to E.

Русский

Конструкция comapOn представляет собой проекции обратно матроидa на β по f на множество E, ограниченную до α.

LaTeX

$$def comapOn (N : Matroid β) (E : Set α) (f : α → β) : Matroid α := (N.comap f) ↾ E$$

Lean4

/-- The pullback of a matroid on `β` by a function `f : α → β` to a matroid on `α`,
restricted to a ground set `E`.
The matroids `M.comapOn f E` and `M ↾ (f '' E)` have isomorphic simplifications;
elements with the same nonloop image are parallel. -/
def comapOn (N : Matroid β) (E : Set α) (f : α → β) : Matroid α :=
  (N.comap f) ↾ E

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