Zulip Chat Archive

Stream: general

Topic: double cases


view this post on Zulip orlando (Apr 08 2020 at 18:30):

Hello, a Little question :

i have a property truc : ∃ (s : S ) (u : U), blabla it's possible obtain directly s, u, hyp_blabla
for the moment i do 2 line :

cases truc with s h_s,
cases h_s with u hyp_blabla,

I'm sure this is possible but i don't remember :confused:

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 18:30):

rcases truc with \<s, u, hyp\>

view this post on Zulip orlando (Apr 08 2020 at 18:32):

ohhh my bad : i use rcases truc with ⟨s, u hyp⟩, i forget the , stupid me !!!

Thx Kevin !

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 18:34):

I watched 20 undergraduates playing a preliminary version of the natural number game last year and they always forgot the comma :-)


Last updated: May 11 2021 at 12:15 UTC