Skip to content

Instantly share code, notes, and snippets.

@arademaker

arademaker/powerset.lean

Created October 15, 2019 13:29
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save arademaker/319a66d1503551ce152e3ba995f91c9e to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save arademaker/319a66d1503551ce152e3ba995f91c9e to your computer and use it in GitHub Desktop.
Download ZIP
powerset in lean
Raw
powerset.lean
open set
variable {U : Type}
example (A B : set U) : A ∈ powerset (A ∪ B) :=
assume x,
assume : x ∈ A,
show x ∈ A ∪ B, from or.inl ‹x ∈ A›
@arademaker
Copy link
Copy Markdown
Author

arademaker commented Oct 17, 2019

The open can be avoided with

variable {U : Type}

example (A B : set U) : A ∈ set.powerset (A ∪ B) :=
assume x,
assume : x ∈ A,
show x ∈ A ∪ B, from or.inl ‹x ∈ A›

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment