Skip to content

Instantly share code, notes, and snippets.

@arademaker

arademaker/powerset.lean

Created October 15, 2019 13:29
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save arademaker/319a66d1503551ce152e3ba995f91c9e to your computer and use it in GitHub Desktop.
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
Author

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