exists_mem_or_left — Mathlib

English

There is an equivalence: from (∃ x, p x ∨ q x) with a witness r x one can derive either (∃ x, p x, r x) or (∃ x, q x, r x).

Русский

Существует нечто с тягой к p или q и r, и это эквивалентно существованию либо с p и r, либо с q и r.

LaTeX

$$$\exists x,\exists h\, (p(x) \lor q(x)) \land r(x) \iff (\exists x,\exists h\, p(x)) \land r(x) \lor (\exists x,\exists h\, q(x)) \land r(x).$$$

Lean4

theorem exists_mem_or_left : (∃ (x : _) (_ : p x ∨ q x), r x) ↔ (∃ (x : _) (_ : p x), r x) ∨ ∃ (x : _) (_ : q x), r x :=
  by
  simp only [exists_prop]
  exact Iff.trans (exists_congr fun x ↦ or_and_right) exists_or

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