extend_val_apply'

Mathlib.Data.Subtype

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

← MathLib Explorer

English

If not p b, then the same extension reduces to j b.

Русский

Если не выполняется p b, тогда продолжение дает j b.

LaTeX

$$$$ \text{If } \neg p(b) \text{ then } \operatorname{extend}_{\mathrm{val}}(g)\ j\ b = j(b). $$$$

Lean4

theorem _root_.Function.extend_val_apply' {p : β → Prop} {g : { x // p x } → γ} {j : β → γ} {b : β} (hb : ¬p b) :
    val.extend g j b = j b := by grind [Function.extend]

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

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

Разделы

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

Аффилиация

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