exists_and_exists_comm — Mathlib

English

If there exist a with property P(a) and there exists b with Q(b), then there exist a and b with P(a) and Q(b). The reverse direction also holds.

Русский

Если существуют a с P(a) и b с Q(b), то существуют a и b с P(a) и Q(b) и наоборот.

LaTeX

$$$$(\\exists a, P(a)) \\land (\\exists b, Q(b)) \\Longleftrightarrow \\exists a\\, b, P(a) \\land Q(b).$$$$

Lean4

theorem exists_and_exists_comm {P : α → Prop} {Q : β → Prop} : (∃ a, P a) ∧ (∃ b, Q b) ↔ ∃ a b, P a ∧ Q b :=
  ⟨fun ⟨⟨a, ha⟩, ⟨b, hb⟩⟩ ↦ ⟨a, b, ⟨ha, hb⟩⟩, fun ⟨a, b, ⟨ha, hb⟩⟩ ↦ ⟨⟨a, ha⟩, ⟨b, hb⟩⟩⟩

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