extend_one — Mathlib

English

Let γ be a type with a multiplicative identity. For any function f: α → β, extending f by the constant maps 1: α → γ and 1: β → γ yields the constant-1 function on α.

Русский

Пусть γ имеет единичный элемент. Пусть f: α → β — произвольная функция. Расширение f константными отображениями 1: α → γ и 1: β → γ дают константную единичную функцию на α.

LaTeX

$$$ \mathrm{extend} f (1 : \alpha \to \gamma) (1 : \beta \to \gamma) = 1 $$$

Lean4

@[to_additive]
theorem extend_one [One γ] (f : α → β) : Function.extend f (1 : α → γ) (1 : β → γ) = 1 :=
  funext fun _ => by apply ite_self

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