exists_update_iff — Mathlib

English

For f, a, b and a predicate p on pairs (a, β a), there exists x with p x (update f a b x) iff p a b or there exists x ≠ a with p x (f x).

Русский

Для заданного f, a, b и предиката p существует x такой, что p x (обновление f a b x), тогда и только тогда, когда p a b выполняется или существует x ≠ a с p x (f x).

LaTeX

$$$\\exists x,\\ p\\ x\\ (update\\ f\\ a\\ b\\ x) \\iff p\\ a\\ b \\lor \\exists x \\neq a, \\ p\\ x\\ (f\\ x)$$$

Lean4

theorem exists_update_iff (f : ∀ a, β a) {a : α} {b : β a} (p : ∀ a, β a → Prop) :
    (∃ x, p x (update f a b x)) ↔ p a b ∨ ∃ x ≠ a, p x (f x) :=
  by
  rw [← not_forall_not, forall_update_iff f fun a b ↦ ¬p a b]
  simp [-not_and, not_and_or]

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