exists — Mathlib

English

Let p and q be propositions and f a function from p ∧ q to Prop. Then (∃ h, f h) is equivalent to ∃ hp, ∃ hq, f ⟨hp, hq⟩.

Русский

Пусть p и q — propositions, f: p ∧ q → Prop. Тогда (∃ h, f h) эквивалентно ∃ hp, ∃ hq, f ⟨hp, hq⟩.

LaTeX

$$$$\\exists h:\\, p \\land q,\\; f(h)$$ эквивалентно $$\\exists p', \\exists q',\\; f\\langle p', q'\\rangle.$$$$

Lean4

theorem «exists» {p q : Prop} {f : p ∧ q → Prop} : (∃ h, f h) ↔ ∃ hp hq, f ⟨hp, hq⟩ :=
  ⟨fun ⟨h, H⟩ ↦ ⟨h.1, h.2, H⟩, fun ⟨hp, hq, H⟩ ↦ ⟨⟨hp, hq⟩, H⟩⟩

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