instFinitaryMapEmbedding — Mathlib

English

Let M be a matroid on α and f an embedding α → β. If M is finitary, then M.mapEmbedding f is finitary.

Русский

Пусть M — матроид на α и f — вложение α → β. Тогда если M является финитным, то M.mapEmbedding f тоже финитен.

LaTeX

$$$\operatorname{Finitary}(M) \Rightarrow \operatorname{Finitary}(M.mapEmbedding f)$$$

Lean4

instance [M.Finitary] {f : α ↪ β} : (M.mapEmbedding f).Finitary :=
  inferInstanceAs (M.map f f.injective.injOn).Finitary

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