extend_val_apply — Mathlib

English

Let p : β → Prop, g : { x // p x } → γ, j : β → γ, b : β with hb : p b. Then the extend of g along val at b equals g applied to the pair (b, hb).

Русский

Пусть p : β → Prop, g : подтип β → γ, j : β → γ, и hb : p b. Тогда продолжение g по коэффициенту val в точке b равно g(⟨b, hb⟩).

LaTeX

$$$$ \text{If } hb : p(b) \text{, then } \operatorname{extend}_{\mathrm{val}}(g)\ j\ b = g(\langle b, hb \rangle). $$$$

Lean4

theorem _root_.Function.extend_val_apply {p : β → Prop} {g : { x // p x } → γ} {j : β → γ} {b : β} (hb : p b) :
    val.extend g j b = g ⟨b, hb⟩ :=
  val_injective.extend_apply g j ⟨b, hb⟩

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