mathlib documentation

data.set.basic

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:

Notation #

Implementation notes #

Tags #

set, sets, subset, subsets, image, preimage, pre-image, range, union, intersection, insert, singleton, complement, powerset

Set coercion to a type #

@[protected, instance]
def set.has_le {α : Type u_1} :
has_le (set α)
Equations
@[protected, instance]
def set.has_lt {α : Type u_1} :
has_lt (set α)
Equations
@[simp]
theorem set.top_eq_univ {α : Type u_1} :
@[simp]
theorem set.bot_eq_empty {α : Type u_1} :
@[simp]
theorem set.sup_eq_union {α : Type u_1} :
@[simp]
theorem set.inf_eq_inter {α : Type u_1} :
@[simp]
theorem set.le_eq_subset {α : Type u_1} :

set.lt_eq_ssubset is defined further down

@[simp]
theorem set.compl_eq_compl {α : Type u_1} :
@[protected, instance]
def set.has_coe_to_sort {α : Type u} :
has_coe_to_sort (set α) (Type u)

Coercion from a set to the corresponding subtype.

Equations
@[protected, instance]
def set.pi_set_coe.can_lift (ι : Type u) (α : ι → Type v) [ne : ∀ (i : ι), nonempty (α i)] (s : set ι) :
can_lift (Π (i : s), α i) (Π (i : ι), α i)
Equations
@[protected, instance]
def set.pi_set_coe.can_lift' (ι : Type u) (α : Type v) [ne : nonempty α] (s : set ι) :
can_lift (s → α) (ι → α)
Equations
@[protected, instance]
def set.set_coe.can_lift {α : Type u_1} (s : set α) :
Equations
theorem set.set_coe_eq_subtype {α : Type u} (s : set α) :
s = {x // x s}
@[simp]
theorem set_coe.forall {α : Type u} {s : set α} {p : s → Prop} :
(∀ (x : s), p x) ∀ (x : α) (h : x s), p x, h⟩
@[simp]
theorem set_coe.exists {α : Type u} {s : set α} {p : s → Prop} :
(∃ (x : s), p x) ∃ (x : α) (h : x s), p x, h⟩
theorem set_coe.exists' {α : Type u} {s : set α} {p : Π (x : α), x s → Prop} :
(∃ (x : α) (h : x s), p x h) ∃ (x : s), p x _
theorem set_coe.forall' {α : Type u} {s : set α} {p : Π (x : α), x s → Prop} :
(∀ (x : α) (h : x s), p x h) ∀ (x : s), p x _
@[simp]
theorem set_coe_cast {α : Type u} {s t : set α} (H' : s = t) (H : s = t) (x : s) :
cast H x = x.val, _⟩
theorem set_coe.ext {α : Type u} {s : set α} {a b : s} :
a = ba = b
theorem set_coe.ext_iff {α : Type u} {s : set α} {a b : s} :
a = b a = b
theorem subtype.mem {α : Type u_1} {s : set α} (p : s) :
p s

See also subtype.prop

theorem eq.subset {α : Type u_1} {s t : set α} :
s = ts t

Duplicate of eq.subset', which currently has elaboration problems.

@[protected, instance]
def set.inhabited {α : Type u} :
Equations
@[ext]
theorem set.ext {α : Type u} {a b : set α} (h : ∀ (x : α), x a x b) :
a = b
theorem set.ext_iff {α : Type u} {s t : set α} :
s = t ∀ (x : α), x s x t
theorem set.mem_of_mem_of_subset {α : Type u} {x : α} {s t : set α} (hx : x s) (h : s t) :
x t
theorem set.forall_in_swap {α : Type u} {β : Type v} {s : set α} {p : α → β → Prop} :
(∀ (a : α), a s∀ (b : β), p a b) ∀ (b : β) (a : α), a sp a b

Lemmas about mem and set_of #

@[simp]
theorem set.mem_set_of_eq {α : Type u} {a : α} {p : α → Prop} :
a {x : α | p x} = p a
theorem set.mem_set_of {α : Type u} {a : α} {p : α → Prop} :
a {x : α | p x} p a
theorem set.has_mem.mem.out {α : Type u} {p : α → Prop} {a : α} (h : a {x : α | p x}) :
p a

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.

theorem set.nmem_set_of_eq {α : Type u} {a : α} {p : α → Prop} :
a {x : α | p x} = ¬p a
@[simp]
theorem set.set_of_mem_eq {α : Type u} {s : set α} :
{x : α | x s} = s
theorem set.set_of_set {α : Type u} {s : set α} :
set_of s = s
theorem set.set_of_app_iff {α : Type u} {p : α → Prop} {x : α} :
{x : α | p x} x p x
theorem set.mem_def {α : Type u} {a : α} {s : set α} :
a s s a
@[simp]
theorem set.set_of_subset_set_of {α : Type u} {p q : α → Prop} :
{a : α | p a} {a : α | q a} ∀ (a : α), p aq a
@[simp]
theorem set.sep_set_of {α : Type u} {p q : α → Prop} :
{a ∈ {a : α | p a} | q a} = {a : α | p a q a}
theorem set.set_of_and {α : Type u} {p q : α → Prop} :
{a : α | p a q a} = {a : α | p a} {a : α | q a}
theorem set.set_of_or {α : Type u} {p q : α → Prop} :
{a : α | p a q a} = {a : α | p a} {a : α | q a}

Subset and strict subset relations #

@[protected, instance]
def set.has_ssubset {α : Type u} :
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem set.subset_def {α : Type u} {s t : set α} :
s t = ∀ (x : α), x sx t
theorem set.ssubset_def {α : Type u} {s t : set α} :
s t = (s t ¬t s)
theorem set.subset.refl {α : Type u} (a : set α) :
a a
theorem set.subset.rfl {α : Type u} {s : set α} :
s s
theorem set.subset.trans {α : Type u} {a b c : set α} (ab : a b) (bc : b c) :
a c
theorem set.mem_of_eq_of_mem {α : Type u} {x y : α} {s : set α} (hx : x = y) (h : y s) :
x s
theorem set.subset.antisymm {α : Type u} {a b : set α} (h₁ : a b) (h₂ : b a) :
a = b
theorem set.subset.antisymm_iff {α : Type u} {a b : set α} :
a = b a b b a
theorem set.eq_of_subset_of_subset {α : Type u} {a b : set α} :
a bb aa = b
theorem set.mem_of_subset_of_mem {α : Type u} {s₁ s₂ : set α} {a : α} (h : s₁ s₂) :
a s₁a s₂
theorem set.not_mem_subset {α : Type u} {a : α} {s t : set α} (h : s t) :
a ta s
theorem set.not_subset {α : Type u} {s t : set α} :
¬s t ∃ (a : α) (H : a s), a t
theorem set.nontrivial_mono {α : Type u_1} {s t : set α} (h₁ : s t) (h₂ : nontrivial s) :

Definition of strict subsets s ⊂ t and basic properties. #

@[simp]
@[protected]
theorem set.eq_or_ssubset_of_subset {α : Type u} {s t : set α} (h : s t) :
s = t s t
theorem set.exists_of_ssubset {α : Type u} {s t : set α} (h : s t) :
∃ (x : α) (H : x t), x s
@[protected]
theorem set.ssubset_iff_subset_ne {α : Type u} {s t : set α} :
s t s t s t
theorem set.ssubset_iff_of_subset {α : Type u} {s t : set α} (h : s t) :
s t ∃ (x : α) (H : x t), x s
@[protected]
theorem set.ssubset_of_ssubset_of_subset {α : Type u} {s₁ s₂ s₃ : set α} (hs₁s₂ : s₁ s₂) (hs₂s₃ : s₂ s₃) :
s₁ s₃
@[protected]
theorem set.ssubset_of_subset_of_ssubset {α : Type u} {s₁ s₂ s₃ : set α} (hs₁s₂ : s₁ s₂) (hs₂s₃ : s₂ s₃) :
s₁ s₃
theorem set.not_mem_empty {α : Type u} (x : α) :
@[simp]
theorem set.not_not_mem {α : Type u} {a : α} {s : set α} :
¬a s a s

Non-empty sets #

@[protected]
def set.nonempty {α : Type u} (s : set α) :
Prop

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.

Equations
@[simp]
theorem set.nonempty_coe_sort {α : Type u} (s : set α) :
theorem set.nonempty_def {α : Type u} {s : set α} :
s.nonempty ∃ (x : α), x s
theorem set.nonempty_of_mem {α : Type u} {s : set α} {x : α} (h : x s) :
theorem set.nonempty.not_subset_empty {α : Type u} {s : set α} :
theorem set.nonempty.ne_empty {α : Type u} {s : set α} :
s.nonemptys
@[simp]
theorem set.not_nonempty_empty {α : Type u} :
@[protected]
noncomputable def set.nonempty.some {α : Type u} {s : set α} (h : s.nonempty) :
α

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
@[protected]
theorem set.nonempty.some_mem {α : Type u} {s : set α} (h : s.nonempty) :
h.some s
theorem set.nonempty.mono {α : Type u} {s t : set α} (ht : s t) (hs : s.nonempty) :
theorem set.nonempty_of_not_subset {α : Type u} {s t : set α} (h : ¬s t) :
(s \ t).nonempty
theorem set.nonempty_of_ssubset {α : Type u} {s t : set α} (ht : s t) :
(t \ s).nonempty
theorem set.nonempty.of_diff {α : Type u} {s t : set α} (h : (s \ t).nonempty) :
theorem set.nonempty_of_ssubset' {α : Type u} {s t : set α} (ht : s t) :
theorem set.nonempty.inl {α : Type u} {s t : set α} (hs : s.nonempty) :
theorem set.nonempty.inr {α : Type u} {s t : set α} (ht : t.nonempty) :
@[simp]
theorem set.union_nonempty {α : Type u} {s t : set α} :
theorem set.nonempty.left {α : Type u} {s t : set α} (h : (s t).nonempty) :
theorem set.nonempty.right {α : Type u} {s t : set α} (h : (s t).nonempty) :
theorem set.nonempty_inter_iff_exists_right {α : Type u} {s t : set α} :
(s t).nonempty ∃ (x : t), x s
theorem set.nonempty_inter_iff_exists_left {α : Type u} {s t : set α} :
(s t).nonempty ∃ (x : s), x t
@[simp]
theorem set.univ_nonempty {α : Type u} [h : nonempty α] :
theorem set.nonempty.to_subtype {α : Type u} {s : set α} (h : s.nonempty) :
@[protected, instance]
def set.univ.nonempty {α : Type u} [nonempty α] :
@[simp]
theorem set.nonempty_insert {α : Type u} (a : α) (s : set α) :
theorem set.nonempty_of_nonempty_subtype {α : Type u} {s : set α} [nonempty s] :

Lemmas about the empty set #

theorem set.empty_def {α : Type u} :
= {x : α | false}
@[simp]
theorem set.mem_empty_eq {α : Type u} (x : α) :
@[simp]
theorem set.set_of_false {α : Type u} :
{a : α | false} =
@[simp]
theorem set.empty_subset {α : Type u} (s : set α) :
theorem set.subset_empty_iff {α : Type u} {s : set α} :
theorem set.eq_empty_iff_forall_not_mem {α : Type u} {s : set α} :
s = ∀ (x : α), x s
theorem set.eq_empty_of_forall_not_mem {α : Type u} {s : set α} (h : ∀ (x : α), x s) :
s =
theorem set.eq_empty_of_subset_empty {α : Type u} {s : set α} :
s s =
theorem set.eq_empty_of_is_empty {α : Type u} [is_empty α] (s : set α) :
s =
def set.unique_empty {α : Type u} [is_empty α] :
unique (set α)

There is exactly one set of a type that is empty.

Equations
theorem set.not_nonempty_iff_eq_empty {α : Type u} {s : set α} :
theorem set.empty_not_nonempty {α : Type u} :
theorem set.ne_empty_iff_nonempty {α : Type u} {s : set α} :
theorem set.eq_empty_or_nonempty {α : Type u} (s : set α) :
theorem set.subset_eq_empty {α : Type u} {s t : set α} (h : t s) (e : s = ) :
t =
theorem set.ball_empty_iff {α : Type u} {p : α → Prop} :
(∀ (x : α), x p x) true
@[protected, instance]
@[simp]
theorem set.empty_ssubset {α : Type u} {s : 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.

@[simp]
theorem set.set_of_true {α : Type u} :
{x : α | true} = set.univ
@[simp]
theorem set.mem_univ {α : Type u} (x : α) :
@[simp]
theorem set.univ_eq_empty_iff {α : Type u} :
theorem set.empty_ne_univ {α : Type u} [nonempty α] :
@[simp]
theorem set.subset_univ {α : Type u} (s : set α) :
theorem set.univ_subset_iff {α : Type u} {s : set α} :
theorem set.eq_univ_of_univ_subset {α : Type u} {s : set α} :
theorem set.eq_univ_iff_forall {α : Type u} {s : set α} :
s = set.univ ∀ (x : α), x s
theorem set.eq_univ_of_forall {α : Type u} {s : set α} :
(∀ (x : α), x s)s = set.univ
theorem set.eq_univ_of_subset {α : Type u} {s t : set α} (h : s t) (hs : s = set.univ) :
theorem set.exists_mem_of_nonempty (α : Type u_1) [nonempty α] :
∃ (x : α), x set.univ
theorem set.ne_univ_iff_exists_not_mem {α : Type u_1} (s : set α) :
s set.univ ∃ (a : α), a s
theorem set.not_subset_iff_exists_mem_not_mem {α : Type u_1} {s t : set α} :
¬s t ∃ (x : α), x s x t
theorem set.univ_unique {α : Type u} [unique α] :

Lemmas about union #

theorem set.union_def {α : Type u} {s₁ s₂ : set α} :
s₁ s₂ = {a : α | a s₁ a s₂}
theorem set.mem_union_left {α : Type u} {x : α} {a : set α} (b : set α) :
x ax a b
theorem set.mem_union_right {α : Type u} {x : α} {b : set α} (a : set α) :
x bx a b
theorem set.mem_or_mem_of_mem_union {α : Type u} {x : α} {a b : set α} (H : x a b) :
x a x b
theorem set.mem_union.elim {α : Type u} {x : α} {a b : set α} {P : Prop} (H₁ : x a b) (H₂ : x a → P) (H₃ : x b → P) :
P
theorem set.mem_union {α : Type u} (x : α) (a b : set α) :
x a b x a x b
@[simp]
theorem set.mem_union_eq {α : Type u} (x : α) (a b : set α) :
x a b = (x a x b)
@[simp]
theorem set.union_self {α : Type u} (a : set α) :
a a = a
@[simp]
theorem set.union_empty {α : Type u} (a : set α) :
a = a
@[simp]
theorem set.empty_union {α : Type u} (a : set α) :
a = a
theorem set.union_comm {α : Type u} (a b : set α) :
a b = b a
theorem set.union_assoc {α : Type u} (a b c : set α) :
a b c = a (b c)
@[protected, instance]
@[protected, instance]
theorem set.union_left_comm {α : Type u} (s₁ s₂ s₃ : set α) :
s₁ (s₂ s₃) = s₂ (s₁ s₃)
theorem set.union_right_comm {α : Type u} (s₁ s₂ s₃ : set α) :
s₁ s₂ s₃ = s₁ s₃ s₂
@[simp]
theorem set.union_eq_left_iff_subset {α : Type u} {s t : set α} :
s t = s t s
@[simp]
theorem set.union_eq_right_iff_subset {α : Type u} {s t : set α} :
s t = t s t
theorem set.union_eq_self_of_subset_left {α : Type u} {s t : set α} (h : s t) :
s t = t
theorem set.union_eq_self_of_subset_right {α : Type u} {s t : set α} (h : t s) :
s t = s
@[simp]
theorem set.subset_union_left {α : Type u} (s t : set α) :
s s t
@[simp]
theorem set.subset_union_right {α : Type u} (s t : set α) :
t s t
theorem set.union_subset {α : Type u} {s t r : set α} (sr : s r) (tr : t r) :
s t r
@[simp]
theorem set.union_subset_iff {α : Type u} {s t u : set α} :
s t u s u t u
theorem set.union_subset_union {α : Type u} {s₁ s₂ t₁ t₂ : set α} (h₁ : s₁ s₂) (h₂ : t₁ t₂) :
s₁ t₁ s₂ t₂
theorem set.union_subset_union_left {α : Type u} {s₁ s₂ : set α} (t : set α) (h : s₁ s₂) :
s₁ t s₂ t
theorem set.union_subset_union_right {α : Type u} (s : set α) {t₁ t₂ : set α} (h : t₁ t₂) :
s t₁ s t₂
theorem set.subset_union_of_subset_left {α : Type u} {s t : set α} (h : s t) (u : set α) :
s t u
theorem set.subset_union_of_subset_right {α : Type u} {s u : set α} (h : s u) (t : set α) :
s t u
@[simp]
theorem set.union_empty_iff {α : Type u} {s t : set α} :
s t = s = t =
@[simp]
theorem set.union_univ {α : Type u} {s : set α} :
@[simp]
theorem set.univ_union {α : Type u} {s : set α} :

Lemmas about intersection #

theorem set.inter_def {α : Type u} {s₁ s₂ : set α} :
s₁ s₂ = {a : α | a s₁ a s₂}
theorem set.mem_inter_iff {α : Type u} (x : α) (a b : set α) :
x a b x a x b
@[simp]
theorem set.mem_inter_eq {α : Type u} (x : α) (a b : set α) :
x a b = (x a x b)
theorem set.mem_inter {α : Type u} {x : α} {a b : set α} (ha : x a) (hb : x b) :
x a b
theorem set.mem_of_mem_inter_left {α : Type u} {x : α} {a b : set α} (h : x a b) :
x a
theorem set.mem_of_mem_inter_right {α : Type u} {x : α} {a b : set α} (h : x a b) :
x b
@[simp]
theorem set.inter_self {α : Type u} (a : set α) :
a a = a
@[simp]
theorem set.inter_empty {α : Type u} (a : set α) :
@[simp]
theorem set.empty_inter {α : Type u} (a : set α) :
theorem set.inter_comm {α : Type u} (a b : set α) :
a b = b a
theorem set.inter_assoc {α : Type u} (a b c : set α) :
a b c = a (b c)
@[protected, instance]
@[protected, instance]
theorem set.inter_left_comm {α : Type u} (s₁ s₂ s₃ : set α) :
s₁ (s₂ s₃) = s₂ (s₁ s₃)
theorem set.inter_right_comm {α : Type u} (s₁ s₂ s₃ : set α) :
s₁ s₂ s₃ = s₁ s₃ s₂
@[simp]
theorem set.inter_subset_left {α : Type u} (s t : set α) :
s t s
@[simp]
theorem set.inter_subset_right {α : Type u} (s t : set α) :
s t t
theorem set.subset_inter {α : Type u} {s t r : set α} (rs : r s) (rt : r t) :
r s t
@[simp]
theorem set.subset_inter_iff {α : Type u} {s t r : set α} :
r s t r s r t
@[simp]
theorem set.inter_eq_left_iff_subset {α : Type u} {s t : set α} :
s t = s s t
@[simp]
theorem set.inter_eq_right_iff_subset {α : Type u} {s t : set α} :
s t = t t s
theorem set.inter_eq_self_of_subset_left {α : Type u} {s t : set α} :
s ts t = s
theorem set.inter_eq_self_of_subset_right {α : Type u} {s t : set α} :
t ss t = t
@[simp]
theorem set.inter_univ {α : Type u} (a : set α) :
@[simp]
theorem set.univ_inter {α : Type u} (a : set α) :
theorem set.inter_subset_inter {α : Type u} {s₁ s₂ t₁ t₂ : set α} (h₁ : s₁ t₁) (h₂ : s₂ t₂) :
s₁ s₂ t₁ t₂
theorem set.inter_subset_inter_left {α : Type u} {s t : set α} (u : set α) (H : s t) :
s u t u
theorem set.inter_subset_inter_right {α : Type u} {s t : set α} (u : set α) (H : s t) :
u s u t
theorem set.union_inter_cancel_left {α : Type u} {s t : set α} :
(s t) s = s
theorem set.union_inter_cancel_right {α : Type u} {s t : set α} :
(s t) t = t

Distributivity laws #

theorem set.inter_distrib_left {α : Type u} (s t u : set α) :
s (t u) = s t s u
theorem set.inter_union_distrib_left {α : Type u} {s t u : set α} :
s (t u) = s t s u
theorem set.inter_distrib_right {α : Type u} (s t u : set α) :
(s t) u = s u t u
theorem set.union_inter_distrib_right {α : Type u} {s t u : set α} :
(s t) u = s u t u
theorem set.union_distrib_left {α : Type u} (s t u : set α) :
s t u = (s t) (s u)
theorem set.union_inter_distrib_left {α : Type u} {s t u : set α} :
s t u = (s t) (s u)
theorem set.union_distrib_right {α : Type u} (s t u : set α) :
s t u = (s u) (t u)
theorem set.inter_union_distrib_right {α : Type u} {s t u : set α} :
s t u = (s u) (t u)

Lemmas about insert #

insert α s is the set {α} ∪ s.

theorem set.insert_def {α : Type u} (x : α) (s : set α) :
insert x s = {y : α | y = x y s}
@[simp]
theorem set.subset_insert {α : Type u} (x : α) (s : set α) :
s insert x s
theorem set.mem_insert {α : Type u} (x : α) (s : set α) :
x insert x s
theorem set.mem_insert_of_mem {α : Type u} {x : α} {s : set α} (y : α) :
x sx insert y s
theorem set.eq_or_mem_of_mem_insert {α : Type u} {x a : α} {s : set α} :
x insert a sx = a x s
theorem set.mem_of_mem_insert_of_ne {α : Type u} {a b : α} {s : set α} :
b insert a sb ab s
theorem set.eq_of_not_mem_of_mem_insert {α : Type u} {a b : α} {s : set α} :
b insert a sb sb = a
@[simp]
theorem set.mem_insert_iff {α : Type u} {x a : α} {s : set α} :
x insert a s x = a x s
@[simp]
theorem set.insert_eq_of_mem {α : Type u} {a : α} {s : set α} (h : a s) :
insert a s = s
theorem set.ne_insert_of_not_mem {α : Type u} {s : set α} (t : set α) {a : α} :
a ss insert a t
theorem set.insert_subset {α : Type u} {a : α} {s t : set α} :
insert a s t a t s t
theorem set.insert_subset_insert {α : Type u} {a : α} {s t : set α} (h : s t) :
insert a s insert a t
theorem set.insert_subset_insert_iff {α : Type u} {a : α} {s t : set α} (ha : a s) :
insert a s insert a t s t
theorem set.ssubset_iff_insert {α : Type u} {s t : set α} :
s t ∃ (a : α) (H : a s), insert a s t
theorem set.ssubset_insert {α : Type u} {s : set α} {a : α} (h : a s) :
s insert a s
theorem set.insert_comm {α : Type u} (a b : α) (s : set α) :
insert a (insert b s) = insert b (insert a s)
theorem set.insert_union {α : Type u} {a : α} {s t : set α} :
insert a s t = insert a (s t)
@[simp]
theorem set.union_insert {α : Type u} {a : α} {s t : set α} :
s insert a t = insert a (s t)
theorem set.insert_nonempty {α : Type u} (a : α) (s : set α) :
@[protected, instance]
def set.has_insert.insert.nonempty {α : Type u} (a : α) (s : set α) :
theorem set.insert_inter_distrib {α : Type u} (a : α) (s t : set α) :
insert a (s t) = insert a s insert a t
theorem set.insert_union_distrib {α : Type u} (a : α) (s t : set α) :
insert a (s t) = insert a s insert a t
theorem set.insert_inj {α : Type u} {a b : α} {s : set α} (ha : a s) :
insert a s = insert b s a = b
theorem set.forall_of_forall_insert {α : Type u} {P : α → Prop} {a : α} {s : set α} (H : ∀ (x : α), x insert a sP x) (x : α) (h : x s) :
P x
theorem set.forall_insert_of_forall {α : Type u} {P : α → Prop} {a : α} {s : set α} (H : ∀ (x : α), x sP x) (ha : P a) (x : α) (h : x insert a s) :
P x
theorem set.bex_insert_iff {α : Type u} {P : α → Prop} {a : α} {s : set α} :
(∃ (x : α) (H : x insert a s), P x) P a ∃ (x : α) (H : x s), P x
theorem set.ball_insert_iff {α : Type u} {P : α → Prop} {a : α} {s : set α} :
(∀ (x : α), x insert a sP x) P a ∀ (x : α), x sP x

Lemmas about singletons #

theorem set.singleton_def {α : Type u} (a : α) :
{a} = {a}
@[simp]
theorem set.mem_singleton_iff {α : Type u} {a b : α} :
a {b} a = b
@[simp]
theorem set.set_of_eq_eq_singleton {α : Type u} {a : α} :
{n : α | n = a} = {a}
@[simp]
theorem set.set_of_eq_eq_singleton' {α : Type u} {a : α} :
{x : α | a = x} = {a}
@[simp]
theorem set.mem_singleton {α : Type u} (a : α) :
a {a}
theorem set.eq_of_mem_singleton {α : Type u} {x y : α} (h : x {y}) :
x = y
@[simp]
theorem set.singleton_eq_singleton_iff {α : Type u} {x y : α} :
{x} = {y} x = y
theorem set.mem_singleton_of_eq {α : Type u} {x y : α} (H : x = y) :
x {y}
theorem set.insert_eq {α : Type u} (x : α) (s : set α) :
insert x s = {x} s
@[simp]
theorem set.pair_eq_singleton {α : Type u} (a : α) :
{a, a} = {a}
theorem set.pair_comm {α : Type u} (a b : α) :
{a, b} = {b, a}
@[simp]
theorem set.singleton_nonempty {α : Type u} (a : α) :
@[simp]
theorem set.singleton_subset_iff {α : Type u} {a : α} {s : set α} :
{a} s a s
theorem set.set_compr_eq_eq_singleton {α : Type u} {a : α} :
{b : α | b = a} = {a}
@[simp]
theorem set.singleton_union {α : Type u} {a : α} {s : set α} :
{a} s = insert a s
@[simp]
theorem set.union_singleton {α : Type u} {a : α} {s : set α} :
s {a} = insert a s
@[simp]
theorem set.singleton_inter_nonempty {α : Type u} {a : α} {s : set α} :
({a} s).nonempty a s
@[simp]
theorem set.inter_singleton_nonempty {α : Type u} {a : α} {s : set α} :
(s {a}).nonempty a s
@[simp]
theorem set.singleton_inter_eq_empty {α : Type u} {a : α} {s : set α} :
{a} s = a s
@[simp]
theorem set.inter_singleton_eq_empty {α : Type u} {a : α} {s : set α} :
s {a} = a s
theorem set.nmem_singleton_empty {α : Type u} {s : set α} :
@[protected, instance]
def set.unique_singleton {α : Type u} (a : α) :
Equations
theorem set.eq_singleton_iff_unique_mem {α : Type u} {a : α} {s : set α} :
s = {a} a s ∀ (x : α), x sx = a
theorem set.eq_singleton_iff_nonempty_unique_mem {α : Type u} {a : α} {s : set α} :
s = {a} s.nonempty ∀ (x : α), x sx = a
@[simp]
theorem set.default_coe_singleton {α : Type u} (x : α) :
default = x, _⟩

Lemmas about sets defined as {x ∈ s | p x}. #

theorem set.mem_sep {α : Type u} {s : set α} {p : α → Prop} {x : α} (xs : x s) (px : p x) :
x {x ∈ s | p x}
@[simp]
theorem set.sep_mem_eq {α : Type u} {s t : set α} :
{x ∈ s | x t} = s t
@[simp]
theorem set.mem_sep_eq {α : Type u} {s : set α} {p : α → Prop} {x : α} :
x {x ∈ s | p x} = (x s p x)
theorem set.mem_sep_iff {α : Type u} {s : set α} {p : α → Prop} {x : α} :
x {x ∈ s | p x} x s p x
theorem set.eq_sep_of_subset {α : Type u} {s t : set α} (h : s t) :
s = {x ∈ t | x s}
@[simp]
theorem set.sep_subset {α : Type u} (s : set α) (p : α → Prop) :
{x ∈ s | p x} s
@[simp]
theorem set.sep_empty {α : Type u} (p : α → Prop) :
{x ∈ | p x} =
theorem set.forall_not_of_sep_empty {α : Type u} {s : set α} {p : α → Prop} (H : {x ∈ s | p x} = ) (x : α) :
x s¬p x
@[simp]
theorem set.sep_univ {α : Type u_1} {p : α → Prop} :
{a ∈ set.univ | p a} = {a : α | p a}
@[simp]
theorem set.sep_true {α : Type u} {s : set α} :
{a ∈ s | true} = s
@[simp]
theorem set.sep_false {α : Type u} {s : set α} :
{a ∈ s | false} =
theorem set.sep_inter_sep {α : Type u} {s : set α} {p q : α → Prop} :
{x ∈ s | p x} {x ∈ s | q x} = {x ∈ s | p x q x}
@[simp]
theorem set.subset_singleton_iff {α : Type u_1} {s : set α} {x : α} :
s {x} ∀ (y : α), y sy = x
theorem set.subset_singleton_iff_eq {α : Type u} {s : set α} {x : α} :
s {x} s = s = {x}
theorem set.ssubset_singleton_iff {α : Type u} {s : set α} {x : α} :
s {x} s =
theorem set.eq_empty_of_ssubset_singleton {α : Type u} {s : set α} {x : α} (hs : s {x}) :
s =

Lemmas about complement #

theorem set.mem_compl {α : Type u} {s : set α} {x : α} (h : x s) :
x s
theorem set.compl_set_of {α : Type u_1} (p : α → Prop) :
{a : α | p a} = {a : α | ¬p a}
theorem set.not_mem_of_mem_compl {α : Type u} {s : set α} {x : α} (h : x s) :
x s
@[simp]
theorem set.mem_compl_eq {α : Type u} (s : set α) (x : α) :
x s = (x s)
theorem set.mem_compl_iff {α : Type u} (s : set α) (x : α) :
x s x s
theorem set.not_mem_compl_iff {α : Type u} {s : set α} {x : α} :
x s x s
@[simp]
theorem set.inter_compl_self {α : Type u} (s : set α) :
@[simp]
theorem set.compl_inter_self {α : Type u} (s : set α) :
@[simp]
theorem set.compl_empty {α : Type u} :
@[simp]
theorem set.compl_union {α : Type u} (s t : set α) :
(s t) = s t
theorem set.compl_inter {α : Type u} (s t : set α) :
(s t) = s t
@[simp]
theorem set.compl_univ {α : Type u} :
@[simp]
theorem set.compl_empty_iff {α : Type u} {s : set α} :
@[simp]
theorem set.compl_univ_iff {α : Type u} {s : set α} :
theorem set.compl_ne_univ {α : Type u} {s : set α} :
theorem set.nonempty_compl {α : Type u} {s : set α} :
theorem set.mem_compl_singleton_iff {α : Type u} {a x : α} :
x {a} x a
theorem set.compl_singleton_eq {α : Type u} (a : α) :
{a} = {x : α | x a}
@[simp]
theorem set.compl_ne_eq_singleton {α : Type u} (a : α) :
{x : α | x a} = {a}
theorem set.union_eq_compl_compl_inter_compl {α : Type u} (s t : set α) :
s t = (s t)
theorem set.inter_eq_compl_compl_union_compl {α : Type u} (s t : set α) :
s t = (s t)
@[simp]
theorem set.union_compl_self {α : Type u} (s : set α) :
@[simp]
theorem set.compl_union_self {α : Type u} (s : set α) :
theorem set.compl_comp_compl {α : Type u} :
theorem set.compl_subset_comm {α : Type u} {s t : set α} :
s t t s
@[simp]
theorem set.compl_subset_compl {α : Type u} {s t : set α} :
s t t s
theorem set.subset_union_compl_iff_inter_subset {α : Type u} {s t u : set α} :
s t u s u t
theorem set.compl_subset_iff_union {α : Type u} {s t : set α} :
theorem set.subset_compl_comm {α : Type u} {s t : set α} :
s t t s
theorem set.subset_compl_iff_disjoint {α : Type u} {s t : set α} :
s t s t =
@[simp]
theorem set.subset_compl_singleton_iff {α : Type u} {a : α} {s : set α} :
s {a} a s
theorem set.inter_subset {α : Type u} (a b c : set α) :
a b c a b c
theorem set.inter_compl_nonempty_iff {α : Type u} {s t : set α} :

Lemmas about set difference #

theorem set.diff_eq {α : Type u} (s t : set α) :
s \ t = s t
@[simp]
theorem set.mem_diff {α : Type u} {s t : set α} (x : α) :
x s \ t x s x t
theorem set.mem_diff_of_mem {α : Type u} {s t : set α} {x : α} (h1 : x s) (h2 : x t) :
x s \ t
theorem set.mem_of_mem_diff {α : Type u} {s t : set α} {x : α} (h : x s \ t) :
x s
theorem set.not_mem_of_mem_diff {α : Type u} {s t : set α} {x : α} (h : x s \ t) :
x t
theorem set.diff_eq_compl_inter {α : Type u} {s t : set α} :
s \ t = t s
theorem set.nonempty_diff {α : Type u} {s t : set α} :
(s \ t).nonempty ¬s t
theorem set.diff_subset {α : Type u} (s t : set α) :
s \ t s
theorem set.union_diff_cancel' {α : Type u} {s t u : set α} (h₁ : s t) (h₂ : t u) :
t u \ s = u
theorem set.union_diff_cancel {α : Type u} {s t : set α} (h : s t) :
s t \ s = t
theorem set.union_diff_cancel_left {α : Type u} {s t : set α} (h : s t ) :
(s t) \ s = t
theorem set.union_diff_cancel_right {α : Type u} {s t : set α} (h : s t ) :
(s t) \ t = s
@[simp]
theorem set.union_diff_left {α : Type u} {s t : set α} :
(s t) \ s = t \ s
@[simp]
theorem set.union_diff_right {α : Type u} {s t : set α} :
(s t) \ t = s \ t
theorem set.union_diff_distrib {α : Type u} {s t u : set α} :
(s t) \ u = s \ u t \ u
theorem set.inter_diff_assoc {α : Type u} (a b c : set α) :
a b \ c = a (b \ c)
@[simp]
theorem set.inter_diff_self {α : Type u} (a b : set α) :
a (b \ a) =
@[simp]
theorem set.inter_union_diff {α : Type u} (s t : set α) :
s t s \ t = s
@[simp]
theorem set.diff_union_inter {α : Type u} (s t : set α) :
s \ t s t = s
@[simp]
theorem set.inter_union_compl {α : Type u} (s t : set α) :
s t s t = s
theorem set.diff_subset_diff {α : Type u} {s₁ s₂ t₁ t₂ : set α} :
s₁ s₂t₂ t₁s₁ \ t₁ s₂ \ t₂
theorem set.diff_subset_diff_left {α : Type u} {s₁ s₂ t : set α} (h : s₁ s₂) :
s₁ \ t s₂ \ t
theorem set.diff_subset_diff_right {α : Type u} {s t u : set α} (h : t u) :
s \ u s \ t
theorem set.compl_eq_univ_diff {α : Type u} (s : set α) :
@[simp]
theorem set.empty_diff {α : Type u} (s : set α) :
theorem set.diff_eq_empty {α : Type u} {s t : set α} :
s \ t = s t
@[simp]
theorem set.diff_empty {α : Type u} {s : set α} :
s \ = s
@[simp]
theorem set.diff_univ {α : Type u} (s : set α) :
theorem set.diff_diff {α : Type u} {s t u : set α} :
s \ t \ u = s \ (t u)
theorem set.diff_diff_comm {α : Type u} {s t u : set α} :
s \ t \ u = s \ u \ t
theorem set.diff_subset_iff {α : Type u} {s t u : set α} :
s \ t u s t u
theorem set.subset_diff_union {α : Type u} (s t : set α) :
s s \ t t
theorem set.diff_union_of_subset {α : Type u} {s t : set α} (h : t s) :
s \ t t = s
@[simp]
theorem set.diff_singleton_subset_iff {α : Type u} {x : α} {s t : set α} :
s \ {x} t s insert x t
theorem set.subset_diff_singleton {α : Type u} {x : α} {s t : set α} (h : s t) (hx : x s) :
s t \ {x}
theorem set.subset_insert_diff_singleton {α : Type u} (x : α) (s : set α) :
s insert x (s \ {x})
theorem set.diff_subset_comm {α : Type u} {s t u : set α} :
s \ t u s \ u t
theorem set.diff_inter {α : Type u} {s t u : set α} :
s \ (t u) = s \ t s \ u
theorem set.diff_inter_diff {α : Type u} {s t u : set α} :
s \ t (s \ u) = s \ (t u)
theorem set.diff_compl {α : Type u} {s t : set α} :
s \ t = s t
theorem set.diff_diff_right {α : Type u} {s t u : set α} :
s \ (t \ u) = s \ t s u
@[simp]
theorem set.insert_diff_of_mem {α : Type u} {a : α} {t : set α} (s : set α) (h : a t) :
insert a s \ t = s \ t
theorem set.insert_diff_of_not_mem {α : Type u} {a : α} {t : set α} (s : set α) (h : a t) :
insert a s \ t = insert a (s \ t)
theorem set.insert_diff_self_of_not_mem {α : Type u} {a : α} {s : set α} (h : a s) :
insert a s \ {a} = s
@[simp]
theorem set.insert_diff_eq_singleton {α : Type u} {a : α} {s : set α} (h : a s) :
insert a s \ s = {a}
theorem set.inter_insert_of_mem {α : Type u} {a : α} {s t : set α} (h : a s) :
s insert a t = insert a (s t)
theorem set.insert_inter_of_mem {α : Type u} {a : α} {s t : set α} (h : a t) :
insert a s t = insert a (s t)
theorem set.inter_insert_of_not_mem {α : Type u} {a : α} {s t : set α} (h : a s) :
s insert a t = s t
theorem set.insert_inter_of_not_mem {α : Type u} {a : α} {s t : set α} (h : a t) :
insert a s t = s t
@[simp]
theorem set.union_diff_self {α : Type u} {s t : set α} :
s t \ s = s t
@[simp]
theorem set.diff_union_self {α : Type u} {s t : set α} :
s \ t t = s t
@[simp]
theorem set.diff_inter_self {α : Type u} {a b : set α} :
b \ a a =
@[simp]
theorem set.diff_inter_self_eq_diff {α : Type u} {s t : set α} :
s \ (t s) = s \ t
@[simp]
theorem set.diff_self_inter {α : Type u} {s t : set α} :
s \ (s t) = s \ t
@[simp]
theorem set.diff_eq_self {α : Type u} {s t : set α} :
s \ t = s t s
@[simp]
theorem set.diff_singleton_eq_self {α : Type u} {a : α} {s : set α} (h : a s) :
s \ {a} = s
@[simp]
theorem set.insert_diff_singleton {α : Type u} {a : α} {s : set α} :
insert a (s \ {a}) = insert a s
@[simp]
theorem set.diff_self {α : Type u} {s : set α} :
s \ s =
theorem set.diff_diff_right_self {α : Type u} (s t : set α) :
s \ (s \ t) = s t
theorem set.diff_diff_cancel_left {α : Type u} {s t : set α} (h : s t) :
t \ (t \ s) = s
theorem set.mem_diff_singleton {α : Type u} {x y : α} {s : set α} :
x s \ {y} x s x y
theorem set.mem_diff_singleton_empty {α : Type u} {s : set α} {t : set (set α)} :
s t \ {} s t s.nonempty
theorem set.union_eq_diff_union_diff_union_inter {α : Type u} (s t : set α) :
s t = s \ t t \ s s t

Powerset #

theorem set.mem_powerset {α : Type u} {x s : set α} (h : x s) :
theorem set.subset_of_mem_powerset {α : Type u} {x s : set α} (h : x 𝒫s) :
x s
@[simp]
theorem set.mem_powerset_iff {α : Type u} (x s : set α) :
x 𝒫s x s
theorem set.powerset_inter {α : Type u} (s t : set α) :
@[simp]
theorem set.powerset_mono {α : Type u} {s t : set α} :
@[simp]
theorem set.powerset_nonempty {α : Type u} {s : set α} :
@[simp]
theorem set.powerset_empty {α : Type u} :
@[simp]
theorem set.powerset_univ {α : Type u} :

If-then-else for sets #

@[protected]
def set.ite {α : Type u} (t s s' : set α) :
set α

ite for sets: set.ite t s s' ∩ t = s ∩ t, set.ite t s s' ∩ tᶜ = s' ∩ tᶜ. Defined as s ∩ t ∪ s' \ t.

Equations
@[simp]
theorem set.ite_inter_self {α : Type u} (t s s' : set α) :
t.ite s s' t = s t
@[simp]
theorem set.ite_compl {α : Type u} (t s s' : set α) :
t.ite s s' = t.ite s' s
@[simp]
theorem set.ite_inter_compl_self {α : Type u} (t s s' : set α) :
t.ite s s' t = s' t
@[simp]
theorem set.ite_diff_self {α : Type u} (t s s' : set α) :
t.ite s s' \ t = s' \ t
@[simp]
theorem set.ite_same {α : Type u} (t s : set α) :
t.ite s s = s
@[simp]
theorem set.ite_left {α : Type u} (s t : set α) :
s.ite s t = s t
@[simp]
theorem set.ite_right {α : Type u} (s t : set α) :
s.ite t s = t s
@[simp]
theorem set.ite_empty {α : Type u} (s s' : set α) :
.ite s s' = s'
@[simp]
theorem set.ite_univ {α : Type u} (s s' : set α) :
set.univ.ite s s' = s
@[simp]
theorem set.ite_empty_left {α : Type u} (t s : set α) :
t.ite s = s \ t
@[simp]
theorem set.ite_empty_right {α : Type u} (t s : set α) :
t.ite s = s t
theorem set.ite_mono {α : Type u} (t : set α) {s₁ s₁' s₂ s₂' : set α} (h : s₁ s₂) (h' : s₁' s₂') :
t.ite s₁ s₁' t.ite s₂ s₂'
theorem set.ite_subset_union {α : Type u} (t s s' : set α) :
t.ite s s' s s'
theorem set.inter_subset_ite {α : Type u} (t s s' : set α) :
s s' t.ite s s'
theorem set.ite_inter_inter {α : Type u} (t s₁ s₂ s₁' s₂' : set α) :
t.ite (s₁ s₂) (s₁' s₂') = t.ite s₁ s₁' t.ite s₂ s₂'
theorem set.ite_inter {α : Type u} (t s₁ s₂ s : set α) :
t.ite (s₁ s) (s₂ s) = t.ite s₁ s₂ s
theorem set.ite_inter_of_inter_eq {α : Type u} (t : set α) {s₁ s₂ s : set α} (h : s₁ s = s₂ s) :
t.ite s₁ s₂ s = s₁ s
theorem set.subset_ite {α : Type u} {t s s' u : set α} :
u t.ite s s' u t s u \ t s'

Inverse image #

def set.preimage {α : Type u} {β : Type v} (f : α → β) (s : set β) :
set α

The preimage of s : set β by f : α → β, written f ⁻¹' s, is the set of x : α such that f x ∈ s.

Equations
@[simp]
theorem set.preimage_empty {α : Type u} {β : Type v} {f : α → β} :
@[simp]
theorem set.mem_preimage {α : Type u} {β : Type v} {f : α → β} {s : set β} {a : α} :
a f ⁻¹' s f a s
theorem set.preimage_congr {α : Type u} {β : Type v} {f g : α → β} {s : set β} (h : ∀ (x : α), f x = g x) :
f ⁻¹' s = g ⁻¹' s
theorem set.preimage_mono {α : Type u} {β : Type v} {f : α → β} {s t : set β} (h : s t) :
f ⁻¹' s f ⁻¹' t
@[simp]
theorem set.preimage_univ {α : Type u} {β : Type v} {f : α → β} :
theorem set.subset_preimage_univ {α : Type u} {β : Type v} {f : α → β} {s : set α} :
@[simp]
theorem set.preimage_inter {α : Type u} {β : Type v} {f : α → β} {s t : set β} :
f ⁻¹' (s t) = f ⁻¹' s f ⁻¹' t
@[simp]
theorem set.preimage_union {α : Type u} {β : Type v} {f : α → β} {s t : set β} :
f ⁻¹' (s t) = f ⁻¹' s f ⁻¹' t
@[simp]
theorem set.preimage_compl {α : Type u} {β : Type v} {f : α → β} {s : set β} :
@[simp]
theorem set.preimage_diff {α : Type u} {β : Type v} (f : α → β) (s t : set β) :
f ⁻¹' (s \ t) = f ⁻¹' s \ f ⁻¹' t
@[simp]
theorem set.preimage_ite {α : Type u} {β : Type v} (f : α → β) (s t₁ t₂ : set β) :
f ⁻¹' s.ite t₁ t₂ = (f ⁻¹' s).ite (f ⁻¹' t₁) (f ⁻¹' t₂)
@[simp]
theorem set.preimage_set_of_eq {α : Type u} {β : Type v} {p : α → Prop} {f : β → α} :
f ⁻¹' {a : α | p a} = {a : β | p (f a)}
@[simp]
theorem set.preimage_id {α : Type u} {s : set α} :
id ⁻¹' s = s
@[simp]
theorem set.preimage_id' {α : Type u} {s : set α} :
(λ (x : α), x) ⁻¹' s = s
@[simp]
theorem set.preimage_const_of_mem {α : Type u} {β : Type v} {b : β} {s : set β} (h : b s) :
(λ (x : α), b) ⁻¹' s = set.univ
@[simp]
theorem set.preimage_const_of_not_mem {α : Type u} {β : Type v} {b : β} {s : set β} (h : b s) :
(λ (x : α), b) ⁻¹' s =
theorem set.preimage_const {α : Type u} {β : Type v} (b : β) (s : set β) [decidable (b s)] :
(λ (x : α), b) ⁻¹' s = ite (b s) set.univ
theorem set.preimage_comp {α : Type u} {β : Type v} {γ : Type w} {f : α → β} {g : β → γ} {s : set γ} :
g f ⁻¹' s = f ⁻¹' (g ⁻¹' s)
theorem set.preimage_preimage {α : Type u} {β : Type v} {γ : Type w} {g : β → γ} {f : α → β} {s : set γ} :
f ⁻¹' (g ⁻¹' s) = (λ (x : α), g (f x)) ⁻¹' s
theorem set.eq_preimage_subtype_val_iff {α : Type u} {p : α → Prop} {s : set (subtype p)} {t : set α} :
s = subtype.val ⁻¹' t ∀ (x : α) (h : p x), x, h⟩ s x t
theorem set.nonempty_of_nonempty_preimage {α : Type u} {β : Type v} {s : set β} {f : α → β} (hf : (f ⁻¹' s).nonempty) :

Image of a set under a function #

theorem set.mem_image_iff_bex {α : Type u} {β : Type v} {f : α → β} {s : set α} {y : β} :
y f '' s ∃ (x : α) (_x : x s), f x = y
theorem set.mem_image_eq {α : Type u} {β : Type v} (f : α → β) (s : set α) (y : β) :
y f '' s = ∃ (x : α), x s f x = y
@[simp]
theorem set.mem_image {α : Type u} {β : Type v} (f : α → β) (s : set α) (y : β) :
y f '' s ∃ (x : α), x s f x = y
theorem set.image_eta {α : Type u} {β : Type v} {s : set α} (f : α → β) :
f '' s = (λ (x : α), f x) '' s
theorem set.mem_image_of_mem {α : Type u} {β : Type v} (f : α → β) {x : α} {a : set α} (h : x a) :
f x f '' a
theorem function.injective.mem_set_image {α : Type u} {β : Type v} {f : α → β} (hf : function.injective f) {s : set α} {a : α} :
f a f '' s a s
theorem set.ball_image_iff {α : Type u} {β : Type v} {f : α → β} {s : set α} {p : β → Prop} :
(∀ (y : β), y f '' sp y) ∀ (x : α), x sp (f x)
theorem set.ball_image_of_ball {α : Type u} {β : Type v} {f : α → β} {s : set α} {p : β → Prop} (h : ∀ (x : α), x sp (f x)) (y : β) (H : y f '' s) :
p y
theorem set.bex_image_iff {α : Type u} {β : Type v} {f : α → β} {s : set α} {p : β → Prop} :
(∃ (y : β) (H : y f '' s), p y) ∃ (x : α) (H : x s), p (f x)
theorem set.mem_image_elim {α : Type u} {β : Type v} {f : α → β} {s : set α} {C : β → Prop} (h : ∀ (x : α), x sC (f x)) {y : β} :
y f '' sC y
theorem set.mem_image_elim_on {α : Type u} {β : Type v} {f : α → β} {s : set α} {C : β → Prop} {y : β} (h_y : y f '' s) (h : ∀ (x : α), x sC (f x)) :
C y
theorem set.image_congr {α : Type u} {β : Type v} {f g : α → β} {s : set α} (h : ∀ (a : α), a sf a = g a) :
f '' s = g '' s
theorem set.image_congr' {α : Type u} {β : Type v} {f g : α → β} {s : set α} (h : ∀ (x : α), f x = g x) :
f '' s = g '' s

A common special case of image_congr

theorem set.image_comp {α : Type u} {β : Type v} {γ : Type w} (f : β → γ) (g : α → β) (a : set α) :
f g '' a = f '' (g '' a)
theorem set.image_image {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : α → β) (s : set α) :
g '' (f '' s) = (λ (x : α), g (f x)) '' s

A variant of image_comp, useful for rewriting

theorem set.image_comm {α : Type u} {β : Type v} {γ : Type w} {s : set α} {β' : Type u_1} {f : β → γ} {g : α → β} {f' : α → β'} {g' : β' → γ} (h_comm : ∀ (a : α), f (g a) = g' (f' a)) :
f '' (g '' s) = g' '' (f' '' s)
theorem set.image_subset {α : Type u} {β : Type v} {a b : set α} (f : α → β) (h : a b) :
f '' a f '' b

Image is monotone with respect to . See set.monotone_image for the statement in terms of .

theorem set.image_union {α : Type u} {β : Type v} (f : α → β) (s t : set α) :
f '' (s t) = f '' s f '' t
@[simp]
theorem set.image_empty {α : Type u} {β : Type v} (f : α → β) :
theorem set.image_inter_subset {α : Type u} {β : Type v} (f : α → β) (s t : set α) :
f '' (s t) f '' s f '' t
theorem set.image_inter_on {α : Type u} {β : Type v} {f : α → β} {s t : set α} (h : ∀ (x : α), x t∀ (y : α), y sf x = f yx = y) :
f '' s f '' t = f '' (s t)
theorem set.image_inter {α : Type u} {β : Type v} {f : α → β} {s t : set α} (H : function.injective f) :
f '' s f '' t = f '' (s t)
theorem set.image_univ_of_surjective {β : Type v} {ι : Type u_1} {f : ι → β} (H : function.surjective f) :
@[simp]
theorem set.image_singleton {α : Type u} {β : Type v} {f : α → β} {a : α} :
f '' {a} = {f a}
@[simp]
theorem set.nonempty.image_const {α : Type u} {β : Type v} {s : set α} (hs : s.nonempty) (a : β) :
(λ (_x : α), a) '' s = {a}
@[simp]
theorem set.image_eq_empty {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} :
f '' s = s =
theorem set.mem_compl_image {α : Type u} (t : set α) (S : set (set α)) :
@[simp]
theorem set.image_id' {α : Type u} (s : set α) :
(λ (x : α), x) '' s = s

A variant of image_id

theorem set.image_id {α : Type u} (s : set α) :
id '' s = s
theorem set.compl_compl_image {α : Type u} (S : set (set α)) :
compl '' (compl '' S) = S
theorem set.image_insert_eq {α : Type u} {β : Type v} {f : α → β} {a : α} {s : set α} :
f '' insert a s = insert (f a) (f '' s)
theorem set.image_pair {α : Type u} {β : Type v} (f : α → β) (a b : α) :
f '' {a, b} = {f a, f b}
theorem set.image_subset_preimage_of_inverse {α : Type u} {β : Type v} {f : α → β} {g : β → α} (I : function.left_inverse g f) (s : set α) :
f '' s g ⁻¹' s
theorem set.preimage_subset_image_of_inverse {α : Type u} {β : Type v} {f : α → β} {g : β → α} (I : function.left_inverse g f) (s : set β) :
f ⁻¹' s g '' s
theorem set.image_eq_preimage_of_inverse {α : Type u} {β : Type v} {f : α → β} {g : β → α} (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) :
theorem set.mem_image_iff_of_inverse {α : Type u} {β : Type v} {f : α → β} {g : β → α} {b : β} {s : set α} (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) :
b f '' s g b s
theorem set.image_compl_subset {α : Type u} {β : Type v} {f : α → β} {s : set α} (H : function.injective f) :
f '' s (f '' s)
theorem set.subset_image_compl {α : Type u} {β : Type v} {f : α → β} {s : set α} (H : function.surjective f) :
(f '' s) f '' s
theorem set.image_compl_eq {α : Type u} {β : Type v} {f : α → β} {s : set α} (H : function.bijective f) :
f '' s = (f '' s)
theorem set.subset_image_diff {α : Type u} {β : Type v} (f : α → β) (s t : set α) :
f '' s \ f '' t f '' (s \ t)
theorem set.image_diff {α : Type u} {β : Type v} {f : α → β} (hf : function.injective f) (s t : set α) :
f '' (s \ t) = f '' s \ f '' t
theorem set.nonempty.image {α : Type u} {β : Type v} (f : α → β) {s : set α} :
s.nonempty(f '' s).nonempty
theorem set.nonempty.of_image {α : Type u} {β : Type v} {f : α → β} {s : set α} :
(f '' s).nonempty → s.nonempty
@[simp]
theorem set.nonempty_image_iff {α : Type u} {β : Type v} {f : α → β} {s : set α} :
theorem set.nonempty.preimage {α : Type u} {β : Type v} {s : set β} (hs : s.nonempty) {f : α → β} (hf : function.surjective f) :
@[protected, instance]
def set.image.nonempty {α : Type u} {β : Type v} (f : α → β) (s : set α) [nonempty s] :
@[simp]
theorem set.image_subset_iff {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} :
f '' s t s f ⁻¹' t

image and preimage are a Galois connection

theorem set.image_preimage_subset {α : Type u} {β : Type v} (f : α → β) (s : set β) :
f '' (f ⁻¹' s) s
theorem set.subset_preimage_image {α : Type u} {β : Type v} (f : α → β) (s : set α) :
s f ⁻¹' (f '' s)
theorem set.preimage_image_eq {α : Type u} {β : Type v} {f : α → β} (s : set α) (h : function.injective f) :
f ⁻¹' (f '' s) = s
theorem set.image_preimage_eq {α : Type u} {β : Type v} {f : α → β} (s : set β) (h : function.surjective f) :
f '' (f ⁻¹' s) = s
theorem set.preimage_eq_preimage {α : Type u} {β : Type v} {s t : set α} {f : β → α} (hf : function.surjective f) :
f ⁻¹' s = f ⁻¹' t s = t
theorem set.image_inter_preimage {α : Type u} {β : Type v} (f : α → β) (s : set α) (t : set β) :
f '' (s f ⁻¹' t) = f '' s t
theorem set.image_preimage_inter {α : Type u} {β : Type v} (f : α → β) (s : set α) (t : set β) :
f '' (f ⁻¹' t s) = t f '' s
@[simp]
theorem set.image_inter_nonempty_iff {α : Type u} {β : Type v} {f : α → β} {s : set α} {t : set β} :
(f '' s t).nonempty (s f ⁻¹' t).nonempty
theorem set.image_diff_preimage {α : Type u} {β : Type v} {f : α → β} {s : set α} {t : set β} :
f '' (s \ f ⁻¹' t) = f '' s \ t
theorem set.compl_image_set_of {α : Type u} {p : set α → Prop} :
compl '' {s : set α | p s} = {s : set α | p s}
theorem set.inter_preimage_subset {α : Type u} {β : Type v} (s : set α) (t : set β) (f : α → β) :
s f ⁻¹' t f ⁻¹' (f '' s t)
theorem set.union_preimage_subset {α : Type u} {β : Type v} (s : set α) (t : set β) (f : α → β) :
s f ⁻¹' t f ⁻¹' (f '' s t)
theorem set.subset_image_union {α : Type u} {β : Type v} (f : α → β) (s : set α) (t : set β) :
f '' (s f ⁻¹' t) f '' s t
theorem set.preimage_subset_iff {α : Type u} {β : Type v} {A : set α} {B : set β} {f : α → β} :
f ⁻¹' B A ∀ (a : α), f a Ba A
theorem set.image_eq_image {α : Type u} {β : Type v} {s t : set α} {f : α → β} (hf : function.injective f) :
f '' s = f '' t s = t
theorem set.image_subset_image_iff {α : Type u} {β : Type v} {s t : set α} {f : α → β} (hf : function.injective f) :
f '' s f '' t s t
theorem set.prod_quotient_preimage_eq_image {α : Type u} {β : Type v} [s : setoid α] (g : quotient s → β) {h : α → β} (Hh : h = g quotient.mk) (r : set × β)) :
{x : quotient s × quotient s | (g x.fst, g x.snd) r} = (λ (a : α × α), (a.fst, a.snd)) '' ((λ (a : α × α), (h a.fst, h a.snd)) ⁻¹' r)
theorem set.exists_image_iff {α : Type u} {β : Type v} (f : α → β) (x : set α) (P : β → Prop) :
(∃ (a : (f '' x)), P a) ∃ (a : x), P (f a)
def set.image_factorization {α : Type u} {β : Type v} (f : α → β) (s : set α) :
s → (f '' s)

Restriction of f to s factors through s.image_factorization f : s → f '' s.

Equations
theorem set.image_factorization_eq {α : Type u} {β : Type v} {f : α → β} {s : set α} :
theorem set.surjective_onto_image {α : Type u} {β : Type v} {f : α → β} {s : set α} :
theorem set.image_perm {α : Type u} {s : set α} {σ : equiv.perm α} (hs : {a : α | σ a a} s) :
σ '' s = s

If the only elements outside s are those left fixed by σ, then mapping by σ has no effect.

Subsingleton #

@[protected]
def set.subsingleton {α : Type u} (s : set α) :
Prop

A set s is a subsingleton, if it has at most one element.

Equations
theorem set.subsingleton.mono {α : Type u} {s t : set α} (ht : t.subsingleton) (hst : s t) :
theorem set.subsingleton.image {α : Type u} {β : Type v} {s : set α} (hs : s.subsingleton) (f : α → β) :
theorem set.subsingleton.eq_singleton_of_mem {α : Type u} {s : set α} (hs : s.subsingleton) {x : α} (hx : x s) :
s = {x}
@[simp]
theorem set.subsingleton_empty {α : Type u} :
@[simp]
theorem set.subsingleton_singleton {α : Type u} {a : α} :
theorem set.subsingleton_of_subset_singleton {α : Type u} {a : α} {s : set α} (h : s {a}) :
theorem set.subsingleton_of_forall_eq {α : Type u} {s : set α} (a : α) (h : ∀ (b : α), b sb = a) :
theorem set.subsingleton_iff_singleton {α : Type u} {s : set α} {x : α} (hx : x s) :
theorem set.subsingleton.eq_empty_or_singleton {α : Type u} {s : set α} (hs : s.subsingleton) :
s = ∃ (x : α), s = {x}
theorem set.subsingleton.induction_on {α : Type u} {s : set α} {p : set α → Prop} (hs : s.subsingleton) (he : p ) (h₁ : ∀ (x : α), p {x}) :
p s
theorem set.subsingleton_of_subsingleton {α : Type u} [subsingleton α] {s : set α} :
theorem set.subsingleton_is_top (α : Type u_1) [partial_order α] :
{x : α | is_top x}.subsingleton
theorem set.subsingleton_is_bot (α : Type u_1) [partial_order α] :
{x : α | is_bot x}.subsingleton
theorem set.exists_eq_singleton_iff_nonempty_subsingleton {α : Type u} {s : set α} :
(∃ (a : α), s = {a}) s.nonempty s.subsingleton
@[simp, norm_cast]
theorem set.subsingleton_coe {α : Type u} (s : set α) :

s, coerced to a type, is a subsingleton type if and only if s is a subsingleton set.

@[protected, instance]

The coe_sort of a set s in a subsingleton type is a subsingleton. For the corresponding result for subtype, see subtype.subsingleton.

theorem set.subsingleton.preimage {α : Type u} {β : Type v} {s : set β} (hs : s.subsingleton) {f : α → β} (hf : function.injective f) :

The preimage of a subsingleton under an injective map is a subsingleton.

theorem set.subsingleton_of_image {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.injective f) (s : set α) (hs : (f '' s).subsingleton) :

s is a subsingleton, if its image of an injective function is.

Lemmas about range of a function. #

def set.range {α : Type u} {ι : Sort x} (f : ι → α) :
set α

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.

Equations
@[simp]
theorem set.mem_range {α : Type u} {ι : Sort x} {f : ι → α} {x : α} :
x set.range f ∃ (y : ι), f y = x
@[simp]
theorem set.mem_range_self {α : Type u} {ι : Sort x} {f : ι → α} (i : ι) :
theorem set.forall_range_iff {α : Type u} {ι : Sort x} {f : ι → α} {p : α → Prop} :
(∀ (a : α), a set.range fp a) ∀ (i : ι), p (f i)
theorem set.forall_subtype_range_iff {α : Type u} {ι : Sort x} {f : ι → α} {p : (set.range f) → Prop} :
(∀ (a : (set.range f)), p a) ∀ (i : ι), p f i, _⟩
theorem set.exists_range_iff {α : Type u} {ι : Sort x} {f : ι → α} {p : α → Prop} :
(∃ (a : α) (H : a set.range f), p a) ∃ (i : ι), p (f i)
theorem set.exists_range_iff' {α : Type u} {ι : Sort x} {f : ι → α} {p : α → Prop} :
(∃ (a : α), a set.range f p a) ∃ (i : ι), p (f i)
theorem set.exists_subtype_range_iff {α : Type u} {ι : Sort x} {f : ι → α} {p : (set.range f) → Prop} :
(∃ (a : (set.range f)), p a) ∃ (i : ι), p f i, _⟩
theorem set.range_iff_surjective {α : Type u} {ι : Sort x} {f : ι → α} :
theorem function.surjective.range_eq {α : Type u} {ι : Sort x} {f : ι → α} :

Alias of range_iff_surjective.

@[simp]
theorem set.range_id {α : Type u} :
@[simp]
theorem set.range_id' {α : Type u} :
set.range (λ (x : α), x) = set.univ
@[simp]
theorem prod.range_fst {α : Type u} {β : Type v} [nonempty β] :
@[simp]
theorem prod.range_snd {α : Type u} {β : Type v} [nonempty α] :
@[simp]
theorem set.range_eval {ι : Type u_1} {α : ι → Type u_2} [∀ (i : ι), nonempty (α i)] (i : ι) :
@[simp]
@[simp]
theorem set.range_inl_inter_range_inr {α : Type u} {β : Type v} :
@[simp]
@[simp]
theorem set.range_inr_inter_range_inl {α : Type u} {β : Type v} :
@[simp]
theorem set.preimage_inl_range_inr {α : Type u} {β : Type v} :
@[simp]
theorem set.preimage_inr_range_inl {α : Type u} {β : Type v} :
@[simp]
theorem set.compl_range_inl {α : Type u} {β : Type v} :
@[simp]
theorem set.compl_range_inr {α : Type u} {β : Type v} :
@[simp]
theorem set.range_quot_mk {α : Type u} (r : α → α → Prop) :
set.range (quot.mk r) = set.univ
@[simp]
theorem set.image_univ {α : Type u} {β : Type v} {f : α → β} :
theorem set.image_subset_range {α : Type u} {β : Type v} (f : α → β) (s : set α) :
theorem set.mem_range_of_mem_image {α : Type u} {β : Type v} (f : α → β) (s : set α) {x : β} (h : x f '' s) :
theorem set.nonempty.preimage' {α : Type u} {β : Type v} {s : set β} (hs : s.nonempty) {f : α → β} (hf : s set.range f) :
theorem set.range_comp {α : Type u} {β : Type v} {ι : Sort x} (g : α → β) (f : ι → α) :
theorem set.range_subset_iff {α : Type u} {ι : Sort x} {s : set α} {f : ι → α} :
set.range f s ∀ (y : ι), f y s
theorem set.range_eq_iff {α : Type u} {β : Type v} (f : α → β) (s : set β) :
set.range f = s (∀ (a : α), f a s) ∀ (b : β), b s(∃ (a : α), f a = b)
theorem set.range_comp_subset_range {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : β → γ) :
theorem set.range_nonempty_iff_nonempty {α : Type u} {ι : Sort x} {f : ι → α} :
theorem set.range_nonempty {α : Type u} {ι : Sort x} [h : nonempty ι] (f : ι → α) :
@[simp]
theorem set.range_eq_empty_iff {α : Type u} {ι : Sort x} {f : ι → α} :
theorem set.range_eq_empty {α : Type u} {ι : Sort x} [is_empty ι] (f : ι → α) :
@[protected, instance]
def set.range.nonempty {α : Type u} {ι : Sort x} [nonempty ι] (f : ι → α) :
@[simp]
theorem set.image_union_image_compl_eq_range {α : Type u} {β : Type v} {s : set α} (f : α → β) :
f '' s f '' s = set.range f
theorem set.image_preimage_eq_inter_range {α : Type u} {β : Type v} {f : α → β} {t : set β} :
f '' (f ⁻¹' t) = t set.range f
theorem set.image_preimage_eq_of_subset {α : Type u} {β : Type v} {f : α → β} {s : set β} (hs : s set.range f) :
f '' (f ⁻¹' s) = s
@[protected, instance]
def set.set.can_lift {α : Type u} {β : Type v} [can_lift α β] :
can_lift (set α) (set β)
Equations
theorem set.image_preimage_eq_iff {α : Type u} {β : Type v} {f : α → β} {s : set β} :
f '' (f ⁻¹' s) = s s set.range f
theorem set.preimage_subset_preimage_iff {α : Type u} {β : Type v} {s t : set α} {f : β → α} (hs : s set.range f) :
f ⁻¹' s f ⁻¹' t s t
theorem set.preimage_eq_preimage' {α : Type u} {β : Type v} {s t : set α} {f : β → α} (hs : s set.range f) (ht : t set.range f) :
f ⁻¹' s = f ⁻¹' t s = t
@[simp]
theorem set.preimage_inter_range {α : Type u} {β : Type v} {f : α → β} {s : set β} :
@[simp]
theorem set.preimage_range_inter {α : Type u} {β : Type v} {f : α → β} {s : set β} :
theorem set.preimage_image_preimage {α : Type u} {β : Type v} {f : α → β} {s : set β} :
f ⁻¹' (f '' (f ⁻¹' s)) = f ⁻¹' s
@[simp]
theorem set.quot_mk_range_eq {α : Type u} [setoid α] :
set.range (λ (x : α), x) = set.univ
theorem set.range_const_subset {α : Type u} {ι : Sort x} {c : α} :
set.range (λ (x : ι), c) {c}
@[simp]
theorem set.range_const {α : Type u} {ι : Sort x} [nonempty ι] {c : α} :
set.range (λ (x : ι), c) = {c}
theorem set.preimage_singleton_nonempty {α : Type u} {β : Type v} {f : α → β} {y : β} :
theorem set.preimage_singleton_eq_empty {α : Type u} {β : Type v} {f : α → β} {y : β} :
theorem set.range_subset_singleton {α : Type u} {ι : Sort x} {f : ι → α} {x : α} :
theorem set.image_compl_preimage {α : Type u} {β : Type v} {f : α → β} {s : set β} :
f '' (f ⁻¹' s) = set.range f \ s
@[simp]
theorem set.range_sigma_mk {α : Type u} {β : α → Type u_1} (a : α) :
def set.range_factorization {β : Type v} {ι : Sort x} (f : ι → β) :
ι → (set.range f)

Any map f : ι → β factors through a map range_factorization f : ι → range f.

Equations
theorem set.range_factorization_eq {β : Type v} {ι : Sort x} {f : ι → β} :
@[simp]
theorem set.range_factorization_coe {β : Type v} {ι : Sort x} (f : ι → β) (a : ι) :
@[simp]
theorem set.coe_comp_range_factorization {β : Type v} {ι : Sort x} (f : ι → β) :
theorem set.surjective_onto_range {α : Type u} {ι : Sort x} {f : ι → α} :
theorem set.image_eq_range {α : Type u} {β : Type v} (f : α → β) (s : set α) :
f '' s = set.range (λ (x : s), f x)
@[simp]
theorem set.sum.elim_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → γ) (g : β → γ) :
theorem set.range_ite_subset' {α : Type u} {β : Type v} {p : Prop} [decidable p] {f g : α → β} :
theorem set.range_ite_subset {α : Type u} {β : Type v} {p : α → Prop} [decidable_pred p] {f g : α → β} :
set.range (λ (x : α), ite (p x) (f x) (g x)) set.range f set.range g
@[simp]
theorem set.preimage_range {α : Type u} {β : Type v} (f : α → β) :
theorem set.range_unique {α : Type u} {ι : Sort x} {f : ι → α} [h : unique ι] :

The range of a function from a unique type contains just the function applied to its single value.

theorem set.range_diff_image_subset {α : Type u} {β : Type v} (f : α → β) (s : set α) :
set.range f \ f '' s f '' s
theorem set.range_diff_image {α : Type u} {β : Type v} {f : α → β} (H : function.injective f) (s : set α) :
set.range f \ f '' s = f '' s
noncomputable def set.range_splitting {α : Type u} {β : Type v} (f : α → β) :
(set.range f) → α

We can use the axiom of choice to pick a preimage for every element of range f.

Equations
theorem set.apply_range_splitting {α : Type u} {β : Type v} (f : α → β) (x : (set.range f)) :
@[simp]
theorem set.comp_range_splitting {α : Type u} {β : Type v} (f : α → β) :
theorem set.left_inverse_range_splitting {α : Type u} {β : Type v} (f : α → β) :
theorem set.range_splitting_injective {α : Type u} {β : Type v} (f : α → β) :
theorem set.preimage_range_splitting {α : Type u} {β : Type v} {f : α → β} (hf : function.injective f) :
@[simp]
theorem set.compl_range_some (α : Type u_1) :
@[simp]
theorem set.range_some_inter_none (α : Type u_1) :
@[simp]
theorem set.range_some_union_none (α : Type u_1) :
@[simp]
theorem function.surjective.preimage_injective {α : Type u_2} {β : Type u_3} {f : α → β} (hf : function.surjective f) :
theorem function.injective.preimage_image {α : Type u_2} {β : Type u_3} {f : α → β} (hf : function.injective f) (s : set α) :
f ⁻¹' (f '' s) = s
theorem function.injective.preimage_surjective {α : Type u_2} {β : Type u_3} {f : α → β} (hf : function.injective f) :
theorem function.injective.subsingleton_image_iff {α : Type u_2} {β : Type u_3} {f : α → β} (hf : function.injective f) {s : set α} :
theorem function.surjective.image_preimage {α : Type u_2} {β : Type u_3} {f : α → β} (hf : function.surjective f) (s : set β) :
f '' (f ⁻¹' s) = s
theorem function.surjective.image_surjective {α : Type u_2} {β : Type u_3} {f : α → β} (hf : function.surjective f) :
theorem function.surjective.nonempty_preimage {α : Type u_2} {β : Type u_3} {f : α → β} (hf : function.surjective f) {s : set β} :
theorem function.injective.image_injective {α : Type u_2} {β : Type u_3} {f : α → β} (hf : function.injective f) :
theorem function.surjective.preimage_subset_preimage_iff {α : Type u_2} {β : Type u_3} {f : α → β} {s t : set β} (hf : function.surjective f) :
f ⁻¹' s f ⁻¹' t s t
theorem function.surjective.range_comp {ι : Sort u_1} {α : Type u_2} {ι' : Sort u_3} {f : ι → ι'} (hf : function.surjective f) (g : ι' → α) :
theorem function.injective.nonempty_apply_iff {α : Type u_2} {β : Type u_3} {f : set αset β} (hf : function.injective f) (h2 : f = ) {s : set α} :
theorem function.injective.mem_range_iff_exists_unique {α : Type u_2} {β : Type u_3} {f : α → β} (hf : function.injective f) {b : β} :
b set.range f ∃! (a : α), f a = b
theorem function.injective.exists_unique_of_mem_range {α : Type u_2} {β : Type u_3} {f : α → β} (hf : function.injective f) {b : β} (hb : b set.range f) :
∃! (a : α), f a = b
theorem function.injective.compl_image_eq {α : Type u_2} {β : Type u_3} {f : α → β} (hf : function.injective f) (s : set α) :
(f '' s) = f '' s (set.range f)
theorem function.left_inverse.image_image {α : Type u_2} {β : Type u_3} {f : α → β} {g : β → α} (h : function.left_inverse g f) (s : set α) :
g '' (f '' s) = s
theorem function.left_inverse.preimage_preimage {α : Type u_2} {β : Type u_3} {f : α → β} {g : β → α} (h : function.left_inverse g f) (s : set α) :
f ⁻¹' (g ⁻¹' s) = s
theorem option.injective_iff {α : Type u_1} {β : Type u_2} {f : option α → β} :

Image and preimage on subtypes #

theorem subtype.coe_image {α : Type u_1} {p : α → Prop} {s : set (subtype p)} :
coe '' s = {x : α | ∃ (h : p x), x, h⟩ s}
@[simp]
theorem subtype.coe_image_of_subset {α : Type u_1} {s t : set α} (h : t s) :
coe '' {x : s | x t} = t
theorem subtype.range_coe {α : Type u_1} {s : set α} :
theorem subtype.range_val {α : Type u_1} {s : set α} :

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.

@[simp]
theorem subtype.range_coe_subtype {α : Type u_1} {p : α → Prop} :
set.range coe = {x : α | p x}

We make this the simp lemma instead of range_coe. The reason is that if we write for s : set α the function coe : s → α, then the inferred implicit arguments of coe are coe α (λ x, x ∈ s).

@[simp]
theorem subtype.coe_preimage_self {α : Type u_1} (s : set α) :
theorem subtype.range_val_subtype {α : Type u_1} {p : α → Prop} :
set.range subtype.val = {x : α | p x}
theorem subtype.coe_image_subset {α : Type u_1} (s : set α) (t : set s) :
coe '' t s
theorem subtype.coe_image_univ {α : Type u_1} (s : set α) :
@[simp]
theorem subtype.image_preimage_coe {α : Type u_1} (s t : set α) :
coe '' (coe ⁻¹' t) = t s
theorem subtype.image_preimage_val {α : Type u_1} (s t : set α) :
theorem subtype.preimage_coe_eq_preimage_coe_iff {α : Type u_1} {s t u : set α} :
coe ⁻¹' t = coe ⁻¹' u t s = u s
theorem subtype.preimage_val_eq_preimage_val_iff {α : Type u_1} (s t u : set α) :
theorem subtype.exists_set_subtype {α : Type u_1} {t : set α} (p : set α → Prop) :
(∃ (s : set t), p (coe '' s)) ∃ (s : set α), s t p s
theorem subtype.preimage_coe_nonempty {α : Type u_1} {s t : set α} :
theorem subtype.preimage_coe_eq_empty {α : Type u_1} {s t : set α} :
@[simp]
theorem subtype.preimage_coe_compl {α : Type u_1} (s : set α) :
@[simp]
theorem subtype.preimage_coe_compl' {α : Type u_1} (s : set α) :

Lemmas about inclusion, the injection of subtypes induced by #

def set.inclusion {α : Type u_1} {s t : set α} (h : s t) :
s → t

inclusion is the "identity" function between two subsets s and t, where s ⊆ t

Equations
@[simp]
theorem set.inclusion_self {α : Type u_1} {s : set α} (x : s) :
@[simp]
theorem set.inclusion_right {α : Type u_1} {s t : set α} (h : s t) (x : t) (m : x s) :
@[simp]
theorem set.inclusion_inclusion {α : Type u_1} {s t u : set α} (hst : s t) (htu : t u) (x : s) :
@[simp]
theorem set.coe_inclusion {α : Type u_1} {s t : set α} (h : s t) (x : s) :
theorem set.inclusion_injective {α : Type u_1} {s t : set α} (h : s t) :
@[simp]
theorem set.range_inclusion {α : Type u_1} {s t : set α} (h : s t) :
theorem set.eq_of_inclusion_surjective {α : Type u_1} {s t : set α} {h : s t} (h_surj : function.surjective (set.inclusion h)) :
s = t

Injectivity and surjectivity lemmas for image and preimage #

@[simp]
theorem set.preimage_injective {α : Type u} {β : Type v} {f : α → β} :
@[simp]
theorem set.preimage_surjective {α : Type u} {β : Type v} {f : α → β} :
@[simp]
theorem set.image_surjective {α : Type u} {β : Type v} {f : α → β} :
@[simp]
theorem set.image_injective {α : Type u} {β : Type v} {f : α → β} :
theorem set.preimage_eq_iff_eq_image {α : Type u} {β : Type v} {f : α → β} (hf : function.bijective f) {s : set β} {t : set α} :
f ⁻¹' s = t s = f '' t
theorem set.eq_preimage_iff_image_eq {α : Type u} {β : Type v} {f : α → β} (hf : function.bijective f) {s : set α} {t : set β} :
s = f ⁻¹' t f '' s = t

Images of binary and ternary functions #

This section is very similar to order.filter.n_ary. Please keep them in sync.

def set.image2 {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α → β → γ) (s : set α) (t : set β) :
set γ

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 α × β → γ.

Equations
theorem set.mem_image2_eq {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : set α} {t : set β} {c : γ} :
c set.image2 f s t = ∃ (a : α) (b : β), a s b t f a b = c
@[simp]
theorem set.mem_image2 {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : set α} {t : set β} {c : γ} :
c set.image2 f s t ∃ (a : α) (b : β), a s b t f a b = c
theorem set.mem_image2_of_mem {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : set α} {t : set β} {a : α} {b : β} (h1 : a s) (h2 : b t) :
f a b set.image2 f s t
theorem set.mem_image2_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : set α} {t : set β} {a : α} {b : β} (hf : function.injective2 f) :
f a b set.image2 f s t a s b t
theorem set.image2_subset {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : set α} {t t' : set β} (hs : s s') (ht : t t') :
set.image2 f s t set.image2 f s' t'

image2 is monotone with respect to .

theorem set.image2_subset_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : set α} {t t' : set β} (ht : t t') :
theorem set.image2_subset_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : set α} {t : set β} (hs : s s') :
theorem set.image_subset_image2_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : set α} {t : set β} {b : β} (hb : b t) :
(λ (a : α), f a b) '' s set.image2 f s t
theorem set.image_subset_image2_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : set α} {t : set β} {a : α} (ha : a s) :
f a '' t set.image2 f s t
theorem set.forall_image2_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : set α} {t : set β} {p : γ → Prop} :
(∀ (z : γ), z set.image2 f s tp z) ∀ (x : α), x s∀ (y : β), y tp (f x y)
@[simp]
theorem set.image2_subset_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : set α} {t : set β} {u : set γ} :
set.image2 f s t u ∀ (x : α), x s∀ (y : β), y tf x y u
theorem set.image2_union_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {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_3} {γ : Type u_5} {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_3} {γ : Type u_5} {f : α → β → γ} {t : set β} :
@[simp]
theorem set.image2_empty_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : set α} :
theorem set.nonempty.image2 {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : set α} {t : set β} :
s.nonemptyt.nonempty(set.image2 f s t).nonempty
@[simp]
theorem set.image2_nonempty_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : set α} {t : set β} :
@[simp]
theorem set.image2_eq_empty_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : set α} {t : set β} :
theorem set.image2_inter_subset_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {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_3} {γ : Type u_5} {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_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {t : set β} {a : α} :
set.image2 f {a} t = f a '' t
@[simp]
theorem set.image2_singleton_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : set α} {b : β} :
set.image2 f s {b} = (λ (a : α), f a b) '' s
theorem set.image2_singleton {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {a : α} {b : β} :
set.image2 f {a} {b} = {f a b}
theorem set.image2_congr {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f f' : α → β → γ} {s : set α} {t : set β} (h : ∀ (a : α), a s∀ (b : β), b tf a b = f' a b) :
set.image2 f s t = set.image2 f' s t
theorem set.image2_congr' {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f f' : α → β → γ} {s : set α} {t : set β} (h : ∀ (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

def set.image3 {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} (g : α → β → γ → δ) (s : set α) (t : set β) (u : set γ) :
set δ

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 α × β × γ → δ.

Equations
@[simp]
theorem set.mem_image3 {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {g : α → β → γ → δ} {s : set α} {t : set β} {u : set γ} {d : δ} :
d set.image3 g s t u ∃ (a : α) (b : β) (c : γ), a s b t c u g a b c = d
theorem set.image3_mono {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {g : α → β → γ → δ} {s s' : set α} {t t' : set β} {u u' : set γ} (hs : s s') (ht : t t') (hu : u u') :
set.image3 g s t u set.image3 g s' t' u'
theorem set.image3_congr {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {g g' : α → β → γ → δ} {s : set α} {t : set β} {u : set γ} (h : ∀ (a : α), a s∀ (b : β), b t∀ (c : γ), c ug 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_3} {γ : Type u_5} {δ : Type u_7} {g g' : α → β → γ → δ} {s : set α} {t : set β} {u : set γ} (h : ∀ (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_3} {γ : Type u_5} {δ : Type u_7} {ε : Type u_9} {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_3} {γ : Type u_5} {δ : Type u_7} {ε : Type u_9} {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_3} {γ : Type u_5} {δ : Type u_7} {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_3} {γ : Type u_5} {δ : Type u_7} {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_3} {γ : Type u_5} {δ : Type u_7} {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_3} {γ : Type u_5} (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_3} {s : set α} {t : set β} (h : t.nonempty) :
set.image2 (λ (x : α) (y : β), x) s t = s
@[simp]
theorem set.image2_right {α : Type u_1} {β : Type u_3} {s : set α} {t : set β} (h : s.nonempty) :
set.image2 (λ (x : α) (y : β), y) s t = t
theorem set.image2_assoc {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {ε : Type u_9} {ε' : Type u_10} {s : set α} {t : set β} {u : set γ} {f : δ → γ → ε} {g : α → β → δ} {f' : α → ε' → ε} {g' : β → γ → ε'} (h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)) :
set.image2 f (set.image2 g s t) u = set.image2 f' s (set.image2 g' t u)
theorem set.image2_comm {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : set α} {t : set β} {g : β → α → γ} (h_comm : ∀ (a : α) (b : β), f a b = g b a) :
set.image2 f s t = set.image2 g t s
theorem set.image2_left_comm {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {δ' : Type u_8} {ε : Type u_9} {s : set α} {t : set β} {u : set γ} {f : α → δ → ε} {g : β → γ → δ} {f' : α → γ → δ'} {g' : β → δ' → ε} (h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)) :
set.image2 f s (set.image2 g t u) = set.image2 g' t (set.image2 f' s u)
theorem set.image2_right_comm {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {δ' : Type u_8} {ε : Type u_9} {s : set α} {t : set β} {u : set γ} {f : δ → γ → ε} {g : α → β → δ} {f' : α → γ → δ'} {g' : δ' → β → ε} (h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b) :
set.image2 f (set.image2 g s t) u = set.image2 g' (set.image2 f' s u) t
theorem set.image_image2_distrib {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {f : α → β → γ} {s : set α} {t : set β} {g : γ → δ} {f' : α' → β' → δ} {g₁ : α → α'} {g₂ : β → β'} (h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)) :
g '' set.image2 f s t = set.image2 f' (g₁ '' s) (g₂ '' t)
theorem set.image_image2_distrib_left {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {f : α → β → γ} {s : set α} {t : set β} {g : γ → δ} {f' : α' → β → δ} {g' : α → α'} (h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b) :
g '' set.image2 f s t = set.image2 f' (g' '' s) t

Symmetric of set.image2_image_left_comm.

theorem set.image_image2_distrib_right {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {f : α → β → γ} {s : set α} {t : set β} {g : γ → δ} {f' : α → β' → δ} {g' : β → β'} (h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)) :
g '' set.image2 f s t = set.image2 f' s (g' '' t)

Symmetric of set.image_image2_right_comm.

theorem set.image2_image_left_comm {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {s : set α} {t : set β} {f : α' → β → γ} {g : α → α'} {f' : α → β → δ} {g' : δ → γ} (h_left_comm : ∀ (a : α) (b : β), f (g a) b = g' (f' a b)) :
set.image2 f (g '' s) t = g' '' set.image2 f' s t

Symmetric of set.image_image2_distrib_left.

theorem set.image_image2_right_comm {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {s : set α} {t : set β} {f : α → β' → γ} {g : β → β'} {f' : α → β → δ} {g' : δ → γ} (h_right_comm : ∀ (a : α) (b : β), f a (g b) = g' (f' a b)) :
set.image2 f s (g '' t) = g' '' set.image2 f' s t

Symmetric of set.image_image2_distrib_right.

theorem set.image_image2_antidistrib {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {f : α → β → γ} {s : set α} {t : set β} {g : γ → δ} {f' : β' → α' → δ} {g₁ : β → β'} {g₂ : α → α'} (h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)) :
g '' set.image2 f s t = set.image2 f' (g₁ '' t) (g₂ '' s)
theorem set.image_image2_antidistrib_left {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {f : α → β → γ} {s : set α} {t : set β} {g : γ → δ} {f' : β' → α → δ} {g' : β → β'} (h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a) :
g '' set.image2 f s t = set.image2 f' (g' '' t) s

Symmetric of set.image2_image_left_anticomm.

theorem set.image_image2_antidistrib_right {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {f : α → β → γ} {s : set α} {t : set β} {g : γ → δ} {f' : β → α' → δ} {g' : α → α'} (h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)) :
g '' set.image2 f s t = set.image2 f' t (g' '' s)

Symmetric of set.image_image2_right_anticomm.

theorem set.image2_image_left_anticomm {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {s : set α} {t : set β} {f : α' → β → γ} {g : α → α'} {f' : β → α → δ} {g' : δ → γ} (h_left_anticomm : ∀ (a : α) (b : β), f (g a) b = g' (f' b a)) :
set.image2 f (g '' s) t = g' '' set.image2 f' t s

Symmetric of set.image_image2_antidistrib_left.

theorem set.image_image2_right_anticomm {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {s : set α} {t : set β} {f : α → β' → γ} {g : β → β'} {f' : β → α → δ} {g' : δ → γ} (h_right_anticomm : ∀ (a : α) (b : β), f a (g b) = g' (f' b a)) :
set.image2 f s (g '' t) = g' '' set.image2 f' t s

Symmetric of set.image_image2_antidistrib_right.

theorem subsingleton.eq_univ_of_nonempty {α : Type u_1} [subsingleton α] {s : set α} :
theorem subsingleton.set_cases {α : Type u_1} [subsingleton α] {p : set α → Prop} (h0 : p ) (h1 : p set.univ) (s : set α) :
p s
theorem subsingleton.mem_iff_nonempty {α : Type u_1} [subsingleton α] {s : set α} {x : α} :

Decidability instances for sets #

@[protected, instance]
def set.decidable_sdiff {α : Type u} (s t : set α) (a : α) [decidable (a s)] [decidable (a t)] :
decidable (a s \ t)
Equations
@[protected, instance]
def set.decidable_inter {α : Type u} (s t : set α) (a : α) [decidable (a s)] [decidable (a t)] :
decidable (a s t)
Equations
@[protected, instance]
def set.decidable_union {α : Type u} (s t : set α) (a : α) [decidable (a s)] [decidable (a t)] :
decidable (a s t)
Equations
@[protected, instance]
def set.decidable_compl {α : Type u} (s : set α) (a : α) [decidable (a s)] :
Equations
@[protected, instance]
def set.decidable_emptyset {α : Type u} :
decidable_pred (λ (_x : α), _x )
Equations
@[protected, instance]
def set.decidable_univ {α : Type u} :
decidable_pred (λ (_x : α), _x set.univ)
Equations
@[protected, instance]
def set.decidable_set_of {α : Type u} (a : α) (p : α → Prop) [decidable (p a)] :
decidable (a {a : α | p a})
Equations