elim_apply — Mathlib

English

For any i in an Option γ, and any x, f, y, the elimination of i applied to x, f, y equals the elimination of i applied to x y and to the function λj. f j y.

Русский

Пусть i ∈ Option γ и даны x, f, y. Тогда применение элиминации к i на x, f, y равно применению элиминации к i на x y и функции λj. f j y.

LaTeX

$$$ i\elim x f y = i\elim (x y) (\lambda j. f j y) $$$

Lean4

theorem elim_apply {f : γ → α → β} {x : α → β} {i : Option γ} {y : α} : i.elim x f y = i.elim (x y) fun j => f j y := by
  rw [elim_comp fun f : α → β => f y]

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