Zulip Chat Archive

Stream: new members

Topic: mathematics in Lean: sets


view this post on Zulip Alexandre Rademaker (Oct 13 2020 at 13:55):

example : s  t = t  s :=
subset.antisymm sorry sorry

The book asks to complete the proof term! I was able to complete using two begin/end blocks but I am not sure if it counts as a solution or a pure proof term must be provided. Anyway, I am blocked by the error in

example : s  t = t  s :=
subset.antisymm (λ x h1, and.intro h1.2 h1.1) sorry

From the previous comment at the beginning of the chapter, it seems that we can't have a solution in proof term?

Due to a quirk of how Lean processes its input, the first example fails if we replace theorem foo with example.

view this post on Zulip Johan Commelin (Oct 13 2020 at 14:05):

example {α : Type} (s t : set α) : s  t = t  s :=
subset.antisymm (λ x h1, and.intro (and.right h1) (and.left h1))
  sorry

view this post on Zulip Alexandre Rademaker (Oct 13 2020 at 14:08):

I just found out that

example : s  t = t  s :=
subset.antisymm
 (λ x hs, ht⟩, and.intro ht hs)
sorry

also works. I wonder if we have any explicit way to deconstruct the set.mem


Last updated: May 15 2021 at 23:13 UTC