English
As above, with motive structure: if p and q eventually hold, then there is a joint eventual hold.
Русский
Как выше, с мотивационной структурой: если p и q выполняются позже, существует совместное позднее выполнение.
LaTeX
$$∀ {α : Type u_2} [inst : LinearOrder α] {p q : α → Prop}, (Exists fun i => ∀ (j : α), GE.ge j i → p j) → (Exists fun i => ∀ (j : α), GE.ge j i → q j) → Exists fun i => ∀ (j : α), GE.ge j i → And (p j) (q j)$$
Lean4
theorem exists_forall_ge_and {p q : α → Prop} : (∃ i, ∀ j ≥ i, p j) → (∃ i, ∀ j ≥ i, q j) → ∃ i, ∀ j ≥ i, p j ∧ q j
| ⟨a, ha⟩, ⟨b, hb⟩ =>
let ⟨c, hac, hbc⟩ := exists_ge_of_linear a b
⟨c, fun _d hcd ↦ ⟨ha _ <| hac.trans hcd, hb _ <| hbc.trans hcd⟩⟩
