map_emptyOn — Mathlib

English

The image of an empty ground matroid under any map is again an empty ground matroid on the target set.

Русский

Образ матроида с пустым множеством опор под отображением есть матроид с пустым основанием на целевом множестве.

LaTeX

$$$ (emptyOn\; \alpha).map\; f \; hf = emptyOn\; \beta $$$

Lean4

@[simp]
theorem map_emptyOn (f : α → β) : (emptyOn α).map f (by simp) = emptyOn β := by simp [← ground_eq_empty_iff]

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