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 coersion 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:
strict_subset s₁ s₂ : Prop: the predicates₁ ⊆ s₂buts₁ ≠ s₂.nonempty s : Prop: the predicates ≠ ∅. Note that this is the preferred way to express the fact thatshas an element (see the Implementation Notes).preimage f t : set α: the preimage f⁻¹(t) (writtenf ⁻¹' tin Lean) of a subset of β.subsingleton s : Prop: the predicate saying thatshas at most one element.range f : set β: the image ofunivunderf. Also works for{p : Prop} (f : p → α)(unlikeimage)inclusion s₁ s₂ : ↥s₁ → ↥s₂: the map↥s₁ → ↥s₂induced by an inclusions₁ ⊆ s₂.
Notation
f ⁻¹' tforpreimage f tf '' sforimage f ssᶜfor the complement ofs
Implementation notes
s.nonemptyis to be preferred tos ≠ ∅or∃ x, x ∈ s. It has the advantage that thes.nonemptydot notation can be used.For
s : set α, do not usesubtype s. Instead use↥sor(s : Type*)ors.
Tags
set, sets, subset, subsets, image, preimage, pre-image, range, union, intersection, insert, singleton, complement, powerset
Set coercion to a type
@[instance]
Equations
@[instance]
Equations
- set.boolean_algebra = {sup := has_union.union set.has_union, le := has_le.le set.has_le, lt := has_lt.lt set.has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inter.inter set.has_inter, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, top := set.univ α, le_top := _, bot := ∅, bot_le := _, compl := set.compl α, sdiff := has_sdiff.sdiff set.has_sdiff, inf_compl_le_bot := _, top_le_sup_compl := _, sdiff_eq := _}
@[instance]
Coercion from a set to the corresponding subtype.
@[instance]
Equations
- set.inhabited = {default := ∅}
Lemmas about mem and set_of
@[simp]
@[instance]
Equations
- s.decidable_mem = H
@[instance]
def
set.decidable_set_of
{α : Type u}
(p : α → Prop)
[H : decidable_pred p] :
decidable_pred {a : α | p a}
Equations
@[simp]
@[simp]
Lemmas about subsets
Definition of strict subsets s ⊂ t and basic properties.
@[instance]
Equations
Non-empty sets
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
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.
@[instance]
Equations
- set.univ_decidable = λ (x : α), decidable.is_true trivial
diagonal α is the subset of α × α consisting of all pairs of the form (a, a).
Lemmas about union
@[instance]
Equations
@[instance]
Equations
Lemmas about intersection
@[instance]
Equations
@[instance]
Equations
Distributivity laws
Lemmas about insert
insert α s is the set {α} ∪ s.
theorem
set.insert_def
{α : Type u}
(x : α)
(s : set α) :
has_insert.insert x s = {y : α | y = x ∨ y ∈ s}
@[simp]
theorem
set.mem_insert_of_mem
{α : Type u}
{x : α}
{s : set α}
(y : α) :
x ∈ s → x ∈ has_insert.insert y s
theorem
set.eq_or_mem_of_mem_insert
{α : Type u}
{x a : α}
{s : set α} :
x ∈ has_insert.insert a s → x = a ∨ x ∈ s
theorem
set.mem_of_mem_insert_of_ne
{α : Type u}
{x a : α}
{s : set α} :
x ∈ has_insert.insert a s → x ≠ a → x ∈ s
@[simp]
@[simp]
theorem
set.ne_insert_of_not_mem
{α : Type u}
{s : set α}
(t : set α)
{a : α} :
a ∉ s → s ≠ has_insert.insert a t
theorem
set.insert_subset_insert
{α : Type u}
{a : α}
{s t : set α} :
s ⊆ t → has_insert.insert a s ⊆ has_insert.insert a t
theorem
set.ssubset_iff_insert
{α : Type u}
{s t : set α} :
s ⊂ t ↔ ∃ (a : α) (H : a ∉ s), has_insert.insert a s ⊆ t
theorem
set.insert_comm
{α : Type u}
(a b : α)
(s : set α) :
has_insert.insert a (has_insert.insert b s) = has_insert.insert b (has_insert.insert a s)
theorem
set.insert_union
{α : Type u}
{a : α}
{s t : set α} :
has_insert.insert a s ∪ t = has_insert.insert a (s ∪ t)
@[simp]
theorem
set.union_insert
{α : Type u}
{a : α}
{s t : set α} :
s ∪ has_insert.insert a t = has_insert.insert a (s ∪ t)
theorem
set.insert_inter
{α : Type u}
(x : α)
(s t : set α) :
has_insert.insert x (s ∩ t) = has_insert.insert x s ∩ has_insert.insert x t
theorem
set.forall_of_forall_insert
{α : Type u}
{P : α → Prop}
{a : α}
{s : set α}
(h : ∀ (x : α), x ∈ has_insert.insert a s → P x)
(x : α) :
x ∈ s → P x
theorem
set.forall_insert_of_forall
{α : Type u}
{P : α → Prop}
{a : α}
{s : set α}
(h : ∀ (x : α), x ∈ s → P x)
(ha : P a)
(x : α) :
x ∈ has_insert.insert a s → P x
theorem
set.bex_insert_iff
{α : Type u}
{P : α → Prop}
{a : α}
{s : set α} :
(∃ (x : α) (H : x ∈ has_insert.insert a s), P x) ↔ (∃ (x : α) (H : x ∈ s), P x) ∨ P a
theorem
set.ball_insert_iff
{α : Type u}
{P : α → Prop}
{a : α}
{s : set α} :
(∀ (x : α), x ∈ has_insert.insert a s → P x) ↔ P a ∧ ∀ (x : α), x ∈ s → P x
Lemmas about singletons
@[simp]
@[simp]
@[instance]
Equations
- set.unique_singleton a = {to_inhabited := {default := ⟨a, _⟩}, uniq := _}
Lemmas about sets defined as {x ∈ s | p x}.
@[simp]
Lemmas about complement
Lemmas about set difference
@[simp]
theorem
set.diff_singleton_subset_iff
{α : Type u}
{x : α}
{s t : set α} :
s \ {x} ⊆ t ↔ s ⊆ has_insert.insert x t
theorem
set.subset_insert_diff_singleton
{α : Type u}
(x : α)
(s : set α) :
s ⊆ has_insert.insert x (s \ {x})
@[simp]
theorem
set.insert_diff_of_mem
{α : Type u}
{a : α}
{t : set α}
(s : set α) :
a ∈ t → has_insert.insert a s \ t = s \ t
theorem
set.insert_diff_of_not_mem
{α : Type u}
{a : α}
{t : set α}
(s : set α) :
a ∉ t → has_insert.insert a s \ t = has_insert.insert a (s \ t)
theorem
set.insert_diff_self_of_not_mem
{α : Type u}
{a : α}
{s : set α} :
a ∉ s → has_insert.insert a s \ {a} = s
@[simp]
theorem
set.insert_diff_singleton
{α : Type u}
{a : α}
{s : set α} :
has_insert.insert a (s \ {a}) = has_insert.insert a s
Powerset
Inverse image
@[simp]
Image of a set under a function
theorem
set.mem_image_of_injective
{α : Type u}
{β : Type v}
{f : α → β}
{a : α}
{s : set α} :
function.injective f → (f a ∈ f '' s ↔ a ∈ s)
Image is monotone with respect to ⊆. See set.monotone_image for the statement in
terms of ≤.
theorem
set.image_univ_of_surjective
{β : Type v}
{ι : Type u_1}
{f : ι → β} :
function.surjective f → f '' set.univ = set.univ
@[simp]
@[simp]
A variant of image_id
theorem
set.compl_compl_image
{α : Type u}
(S : set (set α)) :
has_compl.compl '' (has_compl.compl '' S) = S
theorem
set.image_insert_eq
{α : Type u}
{β : Type v}
{f : α → β}
{a : α}
{s : set α} :
f '' has_insert.insert a s = has_insert.insert (f a) (f '' s)
theorem
set.image_subset_preimage_of_inverse
{α : Type u}
{β : Type v}
{f : α → β}
{g : β → α}
(I : function.left_inverse g f)
(s : set α) :
theorem
set.preimage_subset_image_of_inverse
{α : Type u}
{β : Type v}
{f : α → β}
{g : β → α}
(I : function.left_inverse g f)
(s : set β) :
theorem
set.image_eq_preimage_of_inverse
{α : Type u}
{β : Type v}
{f : α → β}
{g : β → α} :
function.left_inverse g f → function.right_inverse g f → set.image f = set.preimage g
theorem
set.mem_image_iff_of_inverse
{α : Type u}
{β : Type v}
{f : α → β}
{g : β → α}
{b : β}
{s : set α} :
function.left_inverse g f → function.right_inverse g f → (b ∈ f '' s ↔ g b ∈ s)
theorem
set.image_diff
{α : Type u}
{β : Type v}
{f : α → β}
(hf : function.injective f)
(s t : set α) :
theorem
set.preimage_image_eq
{α : Type u}
{β : Type v}
{f : α → β}
(s : set α) :
function.injective f → f ⁻¹' (f '' s) = s
theorem
set.image_preimage_eq
{α : Type u}
{β : Type v}
{f : α → β}
{s : set β} :
function.surjective f → f '' (f ⁻¹' s) = s
theorem
set.prod_quotient_preimage_eq_image
{α : Type u}
{β : Type v}
[s : setoid α]
(g : quotient s → β)
{h : α → β}
(Hh : h = g ∘ quotient.mk)
(r : set (β × β)) :
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
theorem
set.subsingleton.mono
{α : Type u}
{s t : set α} :
t.subsingleton → s ⊆ t → s.subsingleton
theorem
set.subsingleton.image
{α : Type u}
{β : Type v}
{s : set α}
(hs : s.subsingleton)
(f : α → β) :
(f '' s).subsingleton
theorem
set.subsingleton.eq_singleton_of_mem
{α : Type u}
{s : set α}
(hs : s.subsingleton)
{x : α} :
theorem
set.subsingleton.eq_empty_or_singleton
{α : Type u}
{s : set α} :
s.subsingleton → (s = ∅ ∨ ∃ (x : α), s = {x})
Lemmas about range of a function.
@[simp]
@[simp]
@[simp]
Any map f : ι → β factors through a map range_factorization f : ι → range f.
Equations
- set.range_factorization f = λ (i : ι), ⟨f i, _⟩
theorem
set.range_ite_subset
{α : Type u}
{β : Type v}
{p : α → Prop}
[decidable_pred p]
{f g : α → β} :
theorem
set.range_unique
{α : Type u}
{ι : Sort x}
{f : ι → α}
[h : unique ι] :
set.range f = {f (inhabited.default ι)}
The range of a function from a unique type contains just the
function applied to its single value.
The set s is pairwise r if r x y for all distinct x y ∈ s.
Equations
- s.pairwise_on r = ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → r x y
theorem
set.pairwise_on.mono
{α : Type u}
{s t : set α}
{r : α → α → Prop} :
t ⊆ s → s.pairwise_on r → t.pairwise_on r
theorem
set.pairwise_on.mono'
{α : Type u}
{s : set α}
{r r' : α → α → Prop} :
(∀ (a b : α), r a b → r' a b) → s.pairwise_on r → s.pairwise_on r'
theorem
set.pairwise_on_eq_iff_exists_eq
{α : Type u}
{β : Type v}
[nonempty β]
(s : set α)
(f : α → β) :
s.pairwise_on (λ (x y : α), f x = f y) ↔ ∃ (z : β), ∀ (x : α), x ∈ s → f x = z
If and only if f takes pairwise equal values on s, there is
some value it takes everywhere on s.
theorem
function.surjective.preimage_subset_preimage_iff
{α : Type u_2}
{β : Type u_3}
{f : α → β}
{s t : set β} :
theorem
function.surjective.range_comp
{ι : Sort u_1}
{α : Type u_2}
{ι' : Sort u_3}
{f : ι → ι'}
(hf : function.surjective f)
(g : ι' → α) :
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.
theorem
subtype.range_val_subtype
{α : Type u_1}
{p : α → Prop} :
set.range subtype.val = {x : α | p x}
theorem
subtype.image_preimage_val
{α : Type u_1}
(s t : set α) :
subtype.val '' (subtype.val ⁻¹' t) = t ∩ s
theorem
subtype.preimage_val_eq_preimage_val_iff
{α : Type u_1}
(s t u : set α) :
subtype.val ⁻¹' t = subtype.val ⁻¹' u ↔ t ∩ s = u ∩ s
Lemmas about cartesian product of sets
Lemmas about set-indexed products of sets
@[simp]
theorem
set.insert_pi
{ι : Type u_1}
{α : ι → Type u_2}
(i : ι)
(s : set ι)
(t : Π (i : ι), set (α i)) :
(has_insert.insert i s).pi t = function.eval i ⁻¹' t i ∩ s.pi t
@[simp]
theorem
set.singleton_pi
{ι : Type u_1}
{α : ι → Type u_2}
(i : ι)
(t : Π (i : ι), set (α i)) :
{i}.pi t = function.eval i ⁻¹' t i
theorem
set.update_preimage_univ_pi
{ι : Type u_1}
{α : ι → Type u_2}
{t : Π (i : ι), set (α i)}
{i : ι}
{f : Π (i : ι), α i} :
theorem
set.subset_pi_eval_image
{ι : Type u_1}
{α : ι → Type u_2}
(s : set ι)
(u : set (Π (i : ι), α i)) :
u ⊆ s.pi (λ (i : ι), function.eval i '' u)
Lemmas about inclusion, the injection of subtypes induced by ⊆
@[simp]
@[simp]
theorem
set.inclusion_inclusion
{α : Type u_1}
{s t u : set α}
(hst : s ⊆ t)
(htu : t ⊆ u)
(x : ↥s) :
set.inclusion htu (set.inclusion hst x) = set.inclusion _ x
@[simp]
theorem
set.coe_inclusion
{α : Type u_1}
{s t : set α}
(h : s ⊆ t)
(x : ↥s) :
↑(set.inclusion h x) = ↑x
Injectivity and surjectivity lemmas for image and preimage
@[simp]
@[simp]
@[simp]
@[simp]
Lemmas about images of binary and ternary functions
theorem
set.mem_image2_of_mem
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{s : set α}
{t : set β}
{a : α}
{b : β} :
a ∈ s → b ∈ t → f a b ∈ set.image2 f s t
theorem
set.mem_image2_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{s : set α}
{t : set β}
{a : α}
{b : β} :
function.injective2 f → (f a b ∈ set.image2 f s t ↔ a ∈ s ∧ b ∈ t)
theorem
set.image2_subset
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{s s' : set α}
{t t' : set β} :
s ⊆ s' → t ⊆ t' → set.image2 f s t ⊆ set.image2 f s' t'
image2 is monotone with respect to ⊆.
theorem
set.image2_union_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{s s' : set α}
{t : set β} :
set.image2 f (s ∪ s') t = set.image2 f s t ∪ set.image2 f s' t
theorem
set.image2_union_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{s : set α}
{t t' : set β} :
set.image2 f s (t ∪ t') = set.image2 f s t ∪ set.image2 f s t'
@[simp]
theorem
set.image2_empty_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{t : set β} :
set.image2 f ∅ t = ∅
@[simp]
theorem
set.image2_empty_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{s : set α} :
set.image2 f s ∅ = ∅
theorem
set.image2_inter_subset_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{s s' : set α}
{t : set β} :
set.image2 f (s ∩ s') t ⊆ set.image2 f s t ∩ set.image2 f s' t
theorem
set.image2_inter_subset_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{s : set α}
{t t' : set β} :
set.image2 f s (t ∩ t') ⊆ set.image2 f s t ∩ set.image2 f s t'
@[simp]
theorem
set.image2_singleton
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{a : α}
{b : β} :
set.image2 f {a} {b} = {f a b}
theorem
set.image2_singleton_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{t : set β}
{a : α} :
set.image2 f {a} t = f a '' t
theorem
set.image2_singleton_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{s : set α}
{b : β} :
set.image2 f s {b} = (λ (a : α), f a b) '' s
theorem
set.image2_congr
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f f' : α → β → γ}
{s : set α}
{t : set β} :
(∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → f a b = f' a b) → set.image2 f s t = set.image2 f' s t
theorem
set.image2_congr'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f f' : α → β → γ}
{s : set α}
{t : set β} :
(∀ (a : α) (b : β), f a b = f' a b) → set.image2 f s t = set.image2 f' s t
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 α × β × γ → δ.
theorem
set.image3_congr
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{g g' : α → β → γ → δ}
{s : set α}
{t : set β}
{u : set γ} :
(∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → ∀ (c : γ), c ∈ u → g a b c = g' a b c) → set.image3 g s t u = set.image3 g' s t u
theorem
set.image3_congr'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{g g' : α → β → γ → δ}
{s : set α}
{t : set β}
{u : set γ} :
(∀ (a : α) (b : β) (c : γ), g a b c = g' a b c) → set.image3 g s t u = set.image3 g' s t u
A common special case of image3_congr
theorem
set.image2_image2_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{ε : Type u_5}
{s : set α}
{t : set β}
{u : set γ}
(f : δ → γ → ε)
(g : α → β → δ) :
set.image2 f (set.image2 g s t) u = set.image3 (λ (a : α) (b : β) (c : γ), f (g a b) c) s t u
theorem
set.image2_image2_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{ε : Type u_5}
{s : set α}
{t : set β}
{u : set γ}
(f : α → δ → ε)
(g : β → γ → δ) :
set.image2 f s (set.image2 g t u) = set.image3 (λ (a : α) (b : β) (c : γ), f a (g b c)) s t u
theorem
set.image_image2
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{s : set α}
{t : set β}
(f : α → β → γ)
(g : γ → δ) :
g '' set.image2 f s t = set.image2 (λ (a : α) (b : β), g (f a b)) s t
theorem
set.image2_image_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{s : set α}
{t : set β}
(f : γ → β → δ)
(g : α → γ) :
set.image2 f (g '' s) t = set.image2 (λ (a : α) (b : β), f (g a) b) s t
theorem
set.image2_image_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{s : set α}
{t : set β}
(f : α → γ → δ)
(g : β → γ) :
set.image2 f s (g '' t) = set.image2 (λ (a : α) (b : β), f a (g b)) s t
theorem
set.image2_swap
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → γ)
(s : set α)
(t : set β) :
set.image2 f s t = set.image2 (λ (a : β) (b : α), f b a) t s
@[simp]
theorem
set.image2_left
{α : Type u_1}
{β : Type u_2}
{s : set α}
{t : set β} :
t.nonempty → set.image2 (λ (x : α) (y : β), x) s t = s
@[simp]
theorem
set.image2_right
{α : Type u_1}
{β : Type u_2}
{s : set α}
{t : set β} :
s.nonempty → set.image2 (λ (x : α) (y : β), y) s t = t
theorem
set.nonempty.image2
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{s : set α}
{t : set β} :
s.nonempty → t.nonempty → (set.image2 f s t).nonempty
theorem
subsingleton.set_cases
{α : Type u_1}
[subsingleton α]
{p : set α → Prop}
(h0 : p ∅)
(h1 : p set.univ)
(s : set α) :
p s