Zulip Chat Archive

Stream: general

Topic: double cases

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:

Kevin Buzzard (Apr 08 2020 at 18:30):

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

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 !

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: Aug 03 2023 at 10:10 UTC