extend_id

Mathlib.Logic.Function.Basic

URI: https://scilib.ai/kg/mathlib#Function.extend_id

English

Extend id g e' equals g.

Русский

Расширение идентичности даёт исходную функцию g.

LaTeX

$$$\operatorname{extend} \operatorname{id} g e' = g$$$

Lean4

@[simp]
theorem extend_id (g : α → γ) (e' : α → γ) : extend id g e' = g :=
  funext <| injective_id.extend_apply g _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru