map_single — Mathlib

English

The map evaluated at a single generator equals the corresponding relation: map (single r 1) = relation r.

Русский

Оценка отображения на единственный генератор равна соответствующему отношению: map (single r 1) = relation r.

LaTeX

$$@[simp] theorem map_single (r : relations.R) : relations.map (Finsupp.single r 1) = relations.relation r := by simp [map].$$

Lean4

@[simp]
theorem map_single (r : relations.R) : relations.map (Finsupp.single r 1) = relations.relation r := by simp [map]

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