## Stream: new members

### Topic: Use "if" condition within "then" output

#### 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 then?

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):

around hr : - rad < x ∧ x < rad

Last updated: May 09 2021 at 19:11 UTC