Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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?

view this post on Zulip Reid Barton (Nov 28 2018 at 22:44):

try deleting those parentheses?

view this post on Zulip Reid Barton (Nov 28 2018 at 22:45):

around hr : - rad < x ∧ x < rad


Last updated: May 09 2021 at 19:11 UTC