exists_and_iff_of_monotone — Mathlib

English

If P and Q are monotone on a semilattice with sup, then ((∃ x, P x) ∧ (∃ x, Q x)) ⇔ ∃ x, P x ∧ Q x.

Русский

Если P и Q монотонны на полурешётке с объединением, то ((∃ x, P x) ∧ (∃ x, Q x)) эквивалентно ∃ x, P x ∧ Q x.

LaTeX

$$$((\\exists x, P(x)) \\land (\\exists x, Q(x))) \\;\\iff\\; \\exists x, (P(x) \\land Q(x))$$$

Lean4

theorem exists_and_iff_of_monotone {P Q : α → Prop} (hP : Monotone P) (hQ : Monotone Q) :
    ((∃ x, P x) ∧ ∃ x, Q x) ↔ (∃ x, P x ∧ Q x) :=
  ⟨fun ⟨⟨x, hPx⟩, ⟨y, hQx⟩⟩ ↦ ⟨x ⊔ y, ⟨hP le_sup_left hPx, hQ le_sup_right hQx⟩⟩, fun ⟨x, hPx, hQx⟩ ↦
    ⟨⟨x, hPx⟩, ⟨x, hQx⟩⟩⟩

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