diagonal_apply — Mathlib

English

For nonempty ι, the diagonal line diagonal α ι maps x to the constant function sending any index to x.

Русский

Для непустого ι диагональная линия диагональ α ι отображает x в константную функцию, отправляющую любой индекс в x.

LaTeX

$$$[Nonempty\\ ι]\\ (diagonal\\ α\\ ι)(x) = (\\lambda\\_:ι, x).$$$

Lean4

@[simp]
theorem diagonal_apply {α ι} [Nonempty ι] (x : α) : diagonal α ι x = fun _ => x := by ext; simp [diagonal]

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