pred_update — Mathlib

English

For all α, α', β and functions f, g, i, v, the composition distributes over update: f ∘ update g i v = update (f ∘ g) i (f v).

Русский

Сочетание композиции и обновления: $f \\circ update\\ g\\ i\\ v = update\\ (f \\circ g)\\ i\\ (f v)$.

LaTeX

$$$f \\circ update\\ g i v = update (f \\circ g) i (f v)$$

Lean4

theorem pred_update (P : ∀ ⦃a⦄, β a → Prop) (f : ∀ a, β a) (a' : α) (v : β a') (a : α) :
    P (update f a' v a) ↔ a = a' ∧ P v ∨ a ≠ a' ∧ P (f a) := by rw [apply_update P, update_apply, ite_prop_iff_or]

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