Basic properties of sets #
Sets in Lean are homogeneous; all their elements have the same type. Sets whose elements
have type X
are thus defined as set X := X → Prop
. Note that this function need not
be decidable. The definition is in the core library.
This file provides some basic definitions related to sets and functions not present in the core library, as well as extra lemmas for functions in the core library (empty set, univ, union, intersection, insert, singleton, set-theoretic difference, complement, and powerset).
Note that a set is a term, not a type. There is a coercion from set α
to Type*
sending
s
to the corresponding subtype ↥s
.
See also the file set_theory/zfc.lean
, which contains an encoding of ZFC set theory in Lean.
Main definitions #
Notation used here:
Definitions in the file:
-
nonempty s : Prop
: the predicates ≠ ∅
. Note that this is the preferred way to express the fact thats
has an element (see the Implementation Notes). -
preimage f t : set α
: the preimage f⁻¹(t) (writtenf ⁻¹' t
in Lean) of a subset of β. -
subsingleton s : Prop
: the predicate saying thats
has at most one element. -
nontrivial s : Prop
: the predicate saying thats
has at least two distinct elements. -
range f : set β
: the image ofuniv
underf
. Also works for{p : Prop} (f : p → α)
(unlikeimage
) -
inclusion s₁ s₂ : ↥s₁ → ↥s₂
: the map↥s₁ → ↥s₂
induced by an inclusions₁ ⊆ s₂
.
Notation #
-
f ⁻¹' t
forpreimage f t
-
f '' s
forimage f s
-
sᶜ
for the complement ofs
Implementation notes #
-
s.nonempty
is to be preferred tos ≠ ∅
or∃ x, x ∈ s
. It has the advantage that thes.nonempty
dot notation can be used. -
For
s : set α
, do not usesubtype s
. Instead use↥s
or(s : Type*)
ors
.
Tags #
set, sets, subset, subsets, image, preimage, pre-image, range, union, intersection, insert, singleton, complement, powerset
Set coercion to a type #
Equations
Equations
- set.boolean_algebra = {sup := λ (s t : set α), {x : α | x ∈ s ∨ x ∈ t}, le := has_le.le set.has_le, lt := λ (s t : set α), s ⊆ t ∧ ¬t ⊆ s, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := λ (s t : set α), {x : α | x ∈ s ∧ x ∈ t}, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, compl := λ (s : set α), {x : α | x ∉ s}, sdiff := λ (s t : set α), {x : α | x ∈ s ∧ x ∉ t}, himp := boolean_algebra.himp infer_instance, top := set.univ α, bot := ∅, inf_compl_le_bot := _, top_le_sup_compl := _, le_top := _, bot_le := _, sdiff_eq := _, himp_eq := _}
Equations
- set.has_ssubset = {ssubset := has_lt.lt (preorder.to_has_lt (set α))}
Equations
- set.has_union = {union := has_sup.sup (semilattice_sup.to_has_sup (set α))}
Equations
- set.has_inter = {inter := has_inf.inf (semilattice_inf.to_has_inf (set α))}
Coercion from a set to the corresponding subtype.
Equations
- set.pi_set_coe.can_lift ι α s = {coe := λ (f : Π (i : ι), α i) (i : ↥s), f ↑i, cond := can_lift.cond (Π (i : ι), α i) (pi_subtype.can_lift ι α s), prf := _}
Equations
- set.pi_set_coe.can_lift' ι α s = set.pi_set_coe.can_lift ι (λ (_x : ι), α) s
Equations
- set.inhabited = {default := ∅}
If h : a ∈ {x | p x}
then h.out : p x
. These are definitionally equal, but this can
nevertheless be useful for various reasons, e.g. to apply further projection notation or in an
argument to simp
.
Subset and strict subset relations #
Definition of strict subsets s ⊂ t
and basic properties. #
Non-empty sets #
The property s.nonempty
expresses the fact that the set s
is not empty. It should be used
in theorem assumptions instead of ∃ x, x ∈ s
or s ≠ ∅
as it gives access to a nice API thanks
to the dot notation.
Extract a witness from s.nonempty
. This function might be used instead of case analysis
on the argument. Note that it makes a proof depend on the classical.choice
axiom.
Equations
- h.some = classical.some h
Lemmas about the empty set #
There is exactly one set of a type that is empty.
Equations
- set.unique_empty = {to_inhabited := {default := ∅}, uniq := _}
Universal set. #
In Lean @univ α
(or univ : set α
) is the set that contains all elements of type α
.
Mathematically it is the same as α
but it has a different type.
Lemmas about union #
Lemmas about intersection #
Distributivity laws #
Lemmas about insert
#
insert α s
is the set {α} ∪ s
.
Lemmas about singletons #
Equations
- set.unique_singleton a = {to_inhabited := {default := ⟨a, _⟩}, uniq := _}
Lemmas about sets defined as {x ∈ s | p x}
. #
Disjointness #
Lemmas about complement #
Alias of the reverse direction of set.subset_compl_iff_disjoint_right
.
Alias of the reverse direction of set.subset_compl_iff_disjoint_left
.
Alias of the reverse direction of set.disjoint_compl_left_iff_subset
.
Alias of the reverse direction of set.disjoint_compl_right_iff_subset
.
Lemmas about set difference #
Powerset #
𝒫 s = set.powerset s
is the set of all subsets of s
.
If-then-else for sets #
Inverse image #
The preimage of s : set β
by f : α → β
, written f ⁻¹' s
,
is the set of x : α
such that f x ∈ s
.
Image of a set under a function #
The image of s : set α
by f : α → β
, written f '' s
,
is the set of y : β
such that f x = y
for some x ∈ s
.
Instances for set.image
Instances for ↥set.image
Image is monotone with respect to ⊆
. See set.monotone_image
for the statement in
terms of ≤
.
A variant of image_id
If the only elements outside s
are those left fixed by σ
, then mapping by σ
has no effect.
Subsingleton #
A set s
is a subsingleton
if it has at most one element.
Equations
- s.subsingleton = ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y
s
, coerced to a type, is a subsingleton type if and only if s
is a subsingleton set.
The coe_sort
of a set s
in a subsingleton type is a subsingleton.
For the corresponding result for subtype
, see subtype.subsingleton
.
The image of a subsingleton is a subsingleton.
The preimage of a subsingleton under an injective map is a subsingleton.
If the image of a set under an injective map is a subsingleton, the set is a subsingleton.
If the preimage of a set under an surjective map is a subsingleton, the set is a subsingleton.
Nontrivial #
A set s
is nontrivial
if it has at least two distinct elements.
Equations
- s.nontrivial = ∃ (x : α) (H : x ∈ s) (y : α) (H : y ∈ s), x ≠ y
Extract witnesses from s.nontrivial. This function might be used instead of case analysis on the argument. Note that it makes a proof depend on the classical.choice axiom.
Equations
- hs.some = (Exists.some hs, Exists.some _)
s
, coerced to a type, is a nontrivial type if and only if s
is a nontrivial set.
A type with a set s
whose coe_sort
is a nontrivial type is nontrivial.
For the corresponding result for subtype
, see subtype.nontrivial_iff_exists_ne
.
The preimage of a nontrivial set under a surjective map is nontrivial.
The image of a nontrivial set under an injective map is nontrivial.
If the image of a set is nontrivial, the set is nontrivial.
If the preimage of a set under an injective map is nontrivial, the set is nontrivial.
Monotonicity on singletons #
Lemmas about range of a function. #
Range of a function.
This function is more flexible than f '' univ
, as the image requires that the domain is in Type
and not an arbitrary Sort.
Instances for set.range
Alias of the reverse direction of set.range_iff_surjective
.
Equations
- set.can_lift = {coe := λ (s : set β), can_lift.coe '' s, cond := λ (s : set α), ∀ (x : α), x ∈ s → can_lift.cond β x, prf := _}
Any map f : ι → β
factors through a map range_factorization f : ι → range f
.
Equations
- set.range_factorization f = λ (i : ι), ⟨f i, _⟩
The range of a function from a unique
type contains just the
function applied to its single value.
We can use the axiom of choice to pick a preimage for every element of range f
.
Equations
- set.range_splitting f = λ (x : ↥(set.range f)), Exists.some _
Image and preimage on subtypes #
A variant of range_coe
. Try to use range_coe
if possible.
This version is useful when defining a new type that is defined as the subtype of something.
In that case, the coercion doesn't fire anymore.
Lemmas about inclusion
, the injection of subtypes induced by ⊆
#
Injectivity and surjectivity lemmas for image and preimage #
Images of binary and ternary functions #
This section is very similar to order.filter.n_ary
. Please keep them in sync.
The image of a binary function f : α → β → γ
as a function set α → set β → set γ
.
Mathematically this should be thought of as the image of the corresponding function α × β → γ
.
Instances for ↥set.image2
image2 is monotone with respect to ⊆
.
A common special case of image2_congr
The image of a ternary function f : α → β → γ → δ
as a function
set α → set β → set γ → set δ
. Mathematically this should be thought of as the image of the
corresponding function α × β × γ → δ
.
A common special case of image3_congr
Symmetric of set.image2_image_left_comm
.
Symmetric of set.image_image2_right_comm
.
Symmetric of set.image_image2_distrib_left
.
Symmetric of set.image_image2_distrib_right
.
The other direction does not hold because of the s
-s
cross terms on the RHS.
The other direction does not hold because of the u
-u
cross terms on the RHS.
Symmetric of set.image2_image_left_anticomm
.
Symmetric of set.image_image2_right_anticomm
.
Symmetric of set.image_image2_antidistrib_left
.
Symmetric of set.image_image2_antidistrib_right
.
Decidability instances for sets #
Equations
- s.decidable_sdiff t a = and.decidable
Equations
- s.decidable_inter t a = and.decidable
Equations
- s.decidable_union t a = or.decidable
Equations
Equations
- set.decidable_emptyset = λ (_x : α), decidable.is_false _
Equations
- set.decidable_univ = λ (_x : α), decidable.is_true _
Equations
- set.decidable_set_of a p = _inst_1