English
Let P, Q be antitone predicates on a semilattice with infimum. Then ((∃ x, P x) ∧ (∃ x, Q x)) is equivalent to (∃ x, P x ∧ Q x). In particular, if there exist x with P x and y with Q y, then there exists z with P z ∧ Q z, namely z = x ⊓ y; conversely, if there exists z with P z ∧ Q z, then there exist x, y with P x and Q y.
Русский
Пусть P, Q : α → Prop — антитональные предикаты на полупорядоченном множестве α с операцией meet. Тогда ((∃ x, P x) ∧ (∃ x, Q x)) эквивалентно (∃ x, P x ∧ Q x). Другими словами, если существуют x с P x и y с Q y, то существует z с P z и Q z (возьмем z = x ⊓ y); обратно, если существует z с P z ∧ Q z, то существуют x и y с P x и Q y соответственно.
LaTeX
$$$((\\exists x\\, P(x)) \\land (\\exists x\\, Q(x))) \\iff (\\exists x\\, (P(x) \\land Q(x))).$$$
Lean4
theorem exists_and_iff_of_antitone {P Q : α → Prop} (hP : Antitone P) (hQ : Antitone Q) :
((∃ x, P x) ∧ ∃ x, Q x) ↔ (∃ x, P x ∧ Q x) :=
⟨fun ⟨⟨x, hPx⟩, ⟨y, hQx⟩⟩ ↦ ⟨x ⊓ y, ⟨hP inf_le_left hPx, hQ inf_le_right hQx⟩⟩, fun ⟨x, hPx, hQx⟩ ↦
⟨⟨x, hPx⟩, ⟨x, hQx⟩⟩⟩
