Stream: new members
Abhimanyu Pallavi Sudhir (Nov 28 2018 at 22:41):
I'm trying to write something like this:
theorem bob (a : ℕ → ℝ) (rad : ℝ) ( hc : ∀ x, -rad < x ∧ x < rad → is_cau_seq abs (λ (n : ℕ), finset.sum (finset.range n) (λ (k : ℕ), a k * x ^ k)) ) ( f : ℝ → ℝ := λ x, if (hr : - rad < x ∧ x < rad) then cau_seq.lim ((⟨λ n, (finset.range n).sum (λ k, a k * x ^ k) , (λ x, hc x hr) ⟩) : cau_seq ℝ abs) else 0 ) : sorry
Of course, this doesn't work because I can only put a proposition in the if condition, not a proof -- but shouldn't there be some way of achieving this -- of referring to the condition for the
if in the output for
French brackets don't work either because the condition isn't recorded as an assumption at all.
Is this where
dite comes in?
Reid Barton (Nov 28 2018 at 22:44):
try deleting those parentheses?
Reid Barton (Nov 28 2018 at 22:45):
hr : - rad < x ∧ x < rad
Last updated: May 09 2021 at 19:11 UTC