Zulip Chat Archive
Stream: new members
Topic: How to Extract
Debendro Mookerjee (Apr 01 2020 at 15:28):
I have a statement Ha: \exists (\delta : \reals)(H: \delta > 0), \forall (otherstuff).
How to I extract \delta > 0?
Jason KY. (Apr 01 2020 at 15:31):
Try rcases Ha with ⟨δ, hδ₀, hδ₁⟩
Kenny Lau (Apr 01 2020 at 15:36):
exists _ _ is shorthand for exists _, exists _
Last updated: May 02 2025 at 03:31 UTC