English
If P and Q are antitone on sets, then ((∃ u ∈ f, P(u)) ∧ (∃ u ∈ f, Q(u))) is equivalent to ∃ u ∈ f, P(u) ∧ Q(u).
Русский
Если P и Q антитонированы по множествам, тогда ((∃ u ∈ f, P(u)) ∧ (∃ u ∈ f, Q(u))) эквивалентно ∃ u ∈ f, P(u) ∧ Q(u).
LaTeX
$$$ ((\exists u \in f, P(u)) \land (\exists u \in f, Q(u))) \iff (\exists u \in f, P(u) \land Q(u)). $$$
Lean4
theorem exists_mem_and_iff {P : Set α → Prop} {Q : Set α → Prop} (hP : Antitone P) (hQ : Antitone Q) :
((∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u) ↔ ∃ u ∈ f, P u ∧ Q u :=
by
constructor
· rintro ⟨⟨u, huf, hPu⟩, v, hvf, hQv⟩
exact ⟨u ∩ v, inter_mem huf hvf, hP inter_subset_left hPu, hQ inter_subset_right hQv⟩
· rintro ⟨u, huf, hPu, hQu⟩
exact ⟨⟨u, huf, hPu⟩, u, huf, hQu⟩
