Sets #
This file sets up the theory of sets whose elements have a given type.
Main definitions #
Given a type X
and a predicate p : X → Prop
:
Set X
: the type of sets whose elements have typeX
{a : X | p a} : Set X
: the set of all elements ofX
satisfyingp
{a | p a} : Set X
: a more concise notation for{a : X | p a}
{a ∈ S | p a} : Set X
: givenS : Set X
, the subset ofS
consisting of its elements satisfyingp
.
Implementation issues #
As in Lean 3, Set X := X → Prop
I didn't call this file Data.Set.Basic because it contains core Lean 3
stuff which happens before mathlib3's data.set.basic .
This file is a port of the core Lean 3 file lib/lean/library/init/data/set.lean
.
Porting note: we introduce ≤
before ⊆
to help the unifier when applying lattice theorems
to subset hypotheses.