mapEmbedding — Mathlib

English

If B is a base of M, then its image f''B is a base of the mapped matroid M.mapEmbedding f.

Русский

Если B является базой M, тогда образ f''B является базой перенесённого матроида M.mapEmbedding f.

LaTeX

$$$M.IsBase B \\rightarrow (M.mapEmbedding f).IsBase (f '' B)$$$

Lean4

theorem mapEmbedding {B : Set α} (hB : M.IsBase B) (f : α ↪ β) : (M.mapEmbedding f).IsBase (f '' B) :=
  by
  rw [Matroid.mapEmbedding, map_isBase_iff]
  exact ⟨B, hB, rfl⟩

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