mapDomain_single — Mathlib

English

The mapDomain of a single coordinate remains a single coordinate at the image of that coordinate.

Русский

Образ координаты остаётся одиночной координатой в образе этого аргумента.

LaTeX

$$$\\operatorname{mapDomain} f(\\operatorname{single} a\\, b) = \\operatorname{single} (f a)\\, b$.$$

Lean4

@[simp]
theorem mapDomain_single {f : α → β} {a : α} {b : M} : mapDomain f (single a b) = single (f a) b :=
  sum_single_index <| single_zero _

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