exists_mem_or — Mathlib

English

From ∃ x, P x h ∨ Q x h one can deduce either ∃ x, P x h or ∃ x, Q x h.

Русский

Из существования x с P(x,h) ∨ Q(x,h) следует существование либо x с P(x,h), либо x с Q(x,h).

LaTeX

$$$\exists x,\exists h\, (P(x,h) \lor Q(x,h)) \iff (\exists x,\exists h\, P(x,h)) \lor (\exists x,\exists h\, Q(x,h)).$$$

Lean4

theorem exists_mem_or : (∃ x h, P x h ∨ Q x h) ↔ (∃ x h, P x h) ∨ ∃ x h, Q x h :=
  Iff.trans (exists_congr fun _ ↦ exists_or) exists_or

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