proposition: Lemma existence_next_el_to_fun : ∀ (a : ℕ → ℝ) (P : ℕ → ℝ → Prop), (∀ (m : ℕ) (N : ℕ), ∃ k : ℕ, (N ≤ k)%nat ∧ (P m (a k))) ⇒ ∃ f : ℕ → ℕ → ℕ, ∀ (m : ℕ) (N : ℕ), (N ≤ f m N)%nat ∧ P m (a (f m N)).
proof: Proof. Take a : (ℕ → ℝ). Take P : (ℕ → ℝ → Prop). Assume that (for all m N : ℕ, there exists k : ℕ , (N ≤ k)%nat ∧ P m (a k)) (i). We claim that (∀ (m : ℕ), ∃ g : ℕ → ℕ, ∀ N : ℕ, (N ≤ g N)%nat ∧ (P m (a (g N)))) (ii). { Take m : ℕ. apply choice with (R := fun (k : ℕ) (l : ℕ) ↦ ((k ≤ l)%nat ∧ P m (a l))). apply (i). } apply choice with (R := fun (m : ℕ) (h : ℕ → ℕ) ↦ ( ∀ N : ℕ, (N ≤ h N)%nat ∧ P m (a (h N)) ) ). apply (ii). Qed.
imports: Coq.Reals.Reals ZArith Lra Classical Classical_Pred_Type ClassicalChoice Automation Libs.Negation Notations Tactics Waterprove