extend_apply'

Mathlib.Logic.Function.Basic

URI: https://scilib.ai/kg/mathlib#Function.extend_apply'

← MathLib Explorer

English

If there is no a with f a = b, then extend f g e' b = e' b.

Русский

Если не существует a such that f a = b, то extend f g e' b = e' b.

LaTeX

$$$\neg\exists a, f\,a = b \Rightarrow \operatorname{extend} f g e' b = e' b$$$

Lean4

@[simp]
theorem extend_apply' (g : α → γ) (e' : β → γ) (b : β) (hb : ¬∃ a, f a = b) : extend f g e' b = e' b := by
  classical simp [Function.extend_def, hb]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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