mapEmbedding — Mathlib

English

For an embedding f, independence in the mapped matroid is equivalent to independence in the preimage under f and the range condition I ⊆ range f.

Русский

Для вложения f независимость в перенесённом матроиде эквивалентна независимости в предобразе по f и условию I ⊆ range f.

LaTeX

$$$(M.mapEmbedding f).Indep I \\iff M.Indep (f^{-1}' I) \\wedge I \\subseteq \\operatorname{range} f$$$

Lean4

theorem mapEmbedding (hI : M.Indep I) (f : α ↪ β) : (M.mapEmbedding f).Indep (f '' I) := by
  simpa [preimage_image_eq I f.injective]

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