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 #

source
theorem has_subset.subset.trans {α : Type u_1} [has_subset α] [is_trans α has_subset.subset] {a b c : α} (h : a ⊆ b) (h' : b ⊆ c) :
a ⊆ c
source
theorem has_subset.subset.antisymm {α : Type u_1} [has_subset α] [is_antisymm α has_subset.subset] {a b : α} (h : a ⊆ b) (h' : b ⊆ a) :
a = b
source
theorem has_ssubset.ssubset.trans {α : Type u_1} [has_ssubset α] [is_trans α has_ssubset.ssubset] {a b c : α} (h : a ⊂ b) (h' : b ⊂ c) :
a ⊂ c
source
theorem has_ssubset.ssubset.asymm {α : Type u_1} [has_ssubset α] [is_asymm α has_ssubset.ssubset] {a b : α} (h : a ⊂ b) :
¬b ⊂ a
source
@[protected, instance]
def set.has_le {α : Type u_1} :
has_le (set α)
Equations
source
@[protected, instance]
def set.has_lt {α : Type u_1} :
has_lt (set α)
Equations
source
@[protected, instance]
def set.boolean_algebra {α : Type u_1} :
boolean_algebra (set α)
Equations
source
@[simp]
theorem set.top_eq_univ {α : Type u_1} :
⊤ = set.univ
source
@[simp]
theorem set.bot_eq_empty {α : Type u_1} :
⊥ = ∅
source
@[simp]
theorem set.sup_eq_union {α : Type u_1} :
has_sup.sup = has_union.union
source
@[simp]
theorem set.inf_eq_inter {α : Type u_1} :
has_inf.inf = has_inter.inter
source
@[simp]
theorem set.le_eq_subset {α : Type u_1} :
has_le.le = has_subset.subset

set.lt_eq_ssubset is defined further down

source
@[simp]
theorem set.compl_eq_compl {α : Type u_1} :
set.compl = compl
source
@[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
source
@[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
source
@[protected, instance]
def set.pi_set_coe.can_lift' (ι : Type u) (α : Type v) [ne : nonempty α] (s : set ι) :
can_lift (↥s → α) (ι → α)
Equations
source
@[protected, instance]
def set.set_coe.can_lift {α : Type u_1} (s : set α) :
can_lift α ↥s
Equations
source
theorem set.set_coe_eq_subtype {α : Type u} (s : set α) :
↥s = {x // x ∈ s}
source
@[simp]
theorem set_coe.forall {α : Type u} {s : set α} {p : ↥s → Prop} :
(∀ (x : ↥s), p x) ↔ ∀ (x : α) (h : x ∈ s), p ⟨x, h⟩
source
@[simp]
theorem set_coe.exists {α : Type u} {s : set α} {p : ↥s → Prop} :
(∃ (x : ↥s), p x) ↔ ∃ (x : α) (h : x ∈ s), p ⟨x, h⟩
source
theorem set_coe.exists' {α : Type u} {s : set α} {p : Π (x : α), x ∈ s → Prop} :
(∃ (x : α) (h : x ∈ s), p x h) ↔ ∃ (x : ↥s), p ↑x _
source
theorem set_coe.forall' {α : Type u} {s : set α} {p : Π (x : α), x ∈ s → Prop} :
(∀ (x : α) (h : x ∈ s), p x h) ↔ ∀ (x : ↥s), p ↑x _
source
@[simp]
theorem set_coe_cast {α : Type u} {s t : set α} (H' : s = t) (H : ↥s = ↥t) (x : ↥s) :
cast H x = ⟨x.val, _⟩
source
theorem set_coe.ext {α : Type u} {s : set α} {a b : ↥s} :
↑a = ↑b → a = b
source
theorem set_coe.ext_iff {α : Type u} {s : set α} {a b : ↥s} :
↑a = ↑b ↔ a = b
source
theorem subtype.mem {α : Type u_1} {s : set α} (p : ↥s) :
↑p ∈ s

See also subtype.prop

source
theorem eq.subset {α : Type u_1} {s t : set α} :
s = t → s ⊆ t
source
@[protected, instance]
def set.inhabited {α : Type u} :
inhabited (set α)
Equations
source
@[ext]
theorem set.ext {α : Type u} {a b : set α} (h : ∀ (x : α), x ∈ a ↔ x ∈ b) :
a = b
source
theorem set.ext_iff {α : Type u} {s t : set α} :
s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ t
source
theorem set.mem_of_mem_of_subset {α : Type u} {x : α} {s t : set α} (hx : x ∈ s) (h : s ⊆ t) :
x ∈ t

Lemmas about mem and set_of #

source
@[simp]
theorem set.mem_set_of_eq {α : Type u} {a : α} {p : α → Prop} :
a ∈ {a : α | p a} = p a
source
theorem set.nmem_set_of_eq {α : Type u} {a : α} {P : α → Prop} :
a ∉ {a : α | P a} = ¬P a
source
@[simp]
theorem set.set_of_mem_eq {α : Type u} {s : set α} :
{x : α | x ∈ s} = s
source
theorem set.set_of_set {α : Type u} {s : set α} :
set_of s = s
source
theorem set.set_of_app_iff {α : Type u} {p : α → Prop} {x : α} :
{x : α | p x} x ↔ p x
source
theorem set.mem_def {α : Type u} {a : α} {s : set α} :
a ∈ s ↔ s a
source
@[protected, instance]
def set.decidable_set_of {α : Type u} (p : α → Prop) [H : decidable_pred p] :
decidable_pred (λ (_x : α), _x ∈ {a : α | p a})
Equations
source
@[simp]
theorem set.set_of_subset_set_of {α : Type u} {p q : α → Prop} :
{a : α | p a} ⊆ {a : α | q a} ↔ ∀ (a : α), p a → q a
source
@[simp]
theorem set.sep_set_of {α : Type u} {p q : α → Prop} :
{a ∈ {a : α | p a} | q a} = {a : α | p a ∧ q a}
source
theorem set.set_of_and {α : Type u} {p q : α → Prop} :
{a : α | p a ∧ q a} = {a : α | p a} ∩ {a : α | q a}
source
theorem set.set_of_or {α : Type u} {p q : α → Prop} :
{a : α | p a ∨ q a} = {a : α | p a} ∪ {a : α | q a}

Lemmas about subsets #

source
theorem set.subset_def {α : Type u} {s t : set α} :
s ⊆ t = ∀ (x : α), x ∈ s → x ∈ t
source
theorem set.subset.refl {α : Type u} (a : set α) :
a ⊆ a
source
theorem set.subset.rfl {α : Type u} {s : set α} :
s ⊆ s
source
theorem set.subset.trans {α : Type u} {a b c : set α} (ab : a ⊆ b) (bc : b ⊆ c) :
a ⊆ c
source
theorem set.mem_of_eq_of_mem {α : Type u} {x y : α} {s : set α} (hx : x = y) (h : y ∈ s) :
x ∈ s
source
theorem set.subset.antisymm {α : Type u} {a b : set α} (h₁ : a ⊆ b) (h₂ : b ⊆ a) :
a = b
source
theorem set.subset.antisymm_iff {α : Type u} {a b : set α} :
a = b ↔ a ⊆ b ∧ b ⊆ a
source
theorem set.eq_of_subset_of_subset {α : Type u} {a b : set α} :
a ⊆ b → b ⊆ a → a = b
source
theorem set.mem_of_subset_of_mem {α : Type u} {s₁ s₂ : set α} {a : α} (h : s₁ ⊆ s₂) :
a ∈ s₁ → a ∈ s₂
source
theorem set.not_mem_subset {α : Type u} {a : α} {s t : set α} (h : s ⊆ t) :
a ∉ t → a ∉ s
source
theorem set.not_subset {α : Type u} {s t : set α} :
¬s ⊆ t ↔ ∃ (a : α) (H : a ∈ s), a ∉ t

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

source
@[protected, instance]
def set.has_ssubset {α : Type u} :
has_ssubset (set α)
Equations
source
@[simp]
theorem set.lt_eq_ssubset {α : Type u} :
has_lt.lt = has_ssubset.ssubset
source
theorem set.ssubset_def {α : Type u} {s t : set α} :
s ⊂ t = (s ⊆ t ∧ ¬t ⊆ s)
source
theorem set.eq_or_ssubset_of_subset {α : Type u} {s t : set α} (h : s ⊆ t) :
s = t ∨ s ⊂ t
source
theorem set.exists_of_ssubset {α : Type u} {s t : set α} (h : s ⊂ t) :
∃ (x : α) (H : x ∈ t), x ∉ s
source
theorem set.ssubset_iff_subset_ne {α : Type u} {s t : set α} :
s ⊂ t ↔ s ⊆ t ∧ s ≠ t
source
theorem set.ssubset_iff_of_subset {α : Type u} {s t : set α} (h : s ⊆ t) :
s ⊂ t ↔ ∃ (x : α) (H : x ∈ t), x ∉ s
source
theorem set.ssubset_of_ssubset_of_subset {α : Type u} {s₁ s₂ s₃ : set α} (hs₁s₂ : s₁ ⊂ s₂) (hs₂s₃ : s₂ ⊆ s₃) :
s₁ ⊂ s₃
source
theorem set.ssubset_of_subset_of_ssubset {α : Type u} {s₁ s₂ s₃ : set α} (hs₁s₂ : s₁ ⊆ s₂) (hs₂s₃ : s₂ ⊂ s₃) :
s₁ ⊂ s₃
source
theorem set.not_mem_empty {α : Type u} (x : α) :
x ∉ ∅
source
@[simp]
theorem set.not_not_mem {α : Type u} {a : α} {s : set α} :
¬a ∉ s ↔ a ∈ s

Non-empty sets #

source
@[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
source
@[simp]
theorem set.nonempty_coe_sort {α : Type u} (s : set α) :
nonempty ↥s ↔ s.nonempty
source
theorem set.nonempty_def {α : Type u} {s : set α} :
s.nonempty ↔ ∃ (x : α), x ∈ s
source
theorem set.nonempty_of_mem {α : Type u} {s : set α} {x : α} (h : x ∈ s) :
s.nonempty
source
theorem set.nonempty.not_subset_empty {α : Type u} {s : set α} :
s.nonempty → ¬s ⊆ ∅
source
theorem set.nonempty.ne_empty {α : Type u} {s : set α} :
s.nonempty → s ≠ ∅
source
@[simp]
theorem set.not_nonempty_empty {α : Type u} :
¬∅.nonempty
source
@[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
source
@[protected]
theorem set.nonempty.some_mem {α : Type u} {s : set α} (h : s.nonempty) :
h.some ∈ s
source
theorem set.nonempty.mono {α : Type u} {s t : set α} (ht : s ⊆ t) (hs : s.nonempty) :
t.nonempty
source
theorem set.nonempty_of_not_subset {α : Type u} {s t : set α} (h : ¬s ⊆ t) :
(s \ t).nonempty
source
theorem set.nonempty_of_ssubset {α : Type u} {s t : set α} (ht : s ⊂ t) :
(t \ s).nonempty
source
theorem set.nonempty.of_diff {α : Type u} {s t : set α} (h : (s \ t).nonempty) :
s.nonempty
source
theorem set.nonempty_of_ssubset' {α : Type u} {s t : set α} (ht : s ⊂ t) :
t.nonempty
source
theorem set.nonempty.inl {α : Type u} {s t : set α} (hs : s.nonempty) :
(s ∪ t).nonempty
source
theorem set.nonempty.inr {α : Type u} {s t : set α} (ht : t.nonempty) :
(s ∪ t).nonempty
source
@[simp]
theorem set.union_nonempty {α : Type u} {s t : set α} :
(s ∪ t).nonempty ↔ s.nonempty ∨ t.nonempty
source
theorem set.nonempty.left {α : Type u} {s t : set α} (h : (s ∩ t).nonempty) :
s.nonempty
source
theorem set.nonempty.right {α : Type u} {s t : set α} (h : (s ∩ t).nonempty) :
t.nonempty
source
theorem set.nonempty_inter_iff_exists_right {α : Type u} {s t : set α} :
(s ∩ t).nonempty ↔ ∃ (x : ↥t), ↑x ∈ s
source
theorem set.nonempty_inter_iff_exists_left {α : Type u} {s t : set α} :
(s ∩ t).nonempty ↔ ∃ (x : ↥s), ↑x ∈ t
source
theorem set.nonempty_iff_univ_nonempty {α : Type u} :
nonempty α ↔ set.univ.nonempty
source
@[simp]
theorem set.univ_nonempty {α : Type u} [h : nonempty α] :
set.univ.nonempty
source
theorem set.nonempty.to_subtype {α : Type u} {s : set α} (h : s.nonempty) :
nonempty ↥s
source
@[protected, instance]
def set.univ.nonempty {α : Type u} [nonempty α] :
nonempty ↥set.univ
source
@[simp]
theorem set.nonempty_insert {α : Type u} (a : α) (s : set α) :
(insert a s).nonempty
source
theorem set.nonempty_of_nonempty_subtype {α : Type u} {s : set α} [nonempty ↥s] :
s.nonempty

Lemmas about the empty set #

source
theorem set.empty_def {α : Type u} :
∅ = {x : α | false}
source
@[simp]
theorem set.mem_empty_eq {α : Type u} (x : α) :
x ∈ ∅ = false
source
@[simp]
theorem set.set_of_false {α : Type u} :
{a : α | false} = ∅
source
@[simp]
theorem set.empty_subset {α : Type u} (s : set α) :
∅ ⊆ s
source
theorem set.subset_empty_iff {α : Type u} {s : set α} :
s ⊆ ∅ ↔ s = ∅
source
theorem set.eq_empty_iff_forall_not_mem {α : Type u} {s : set α} :
s = ∅ ↔ ∀ (x : α), x ∉ s
source
theorem set.eq_empty_of_subset_empty {α : Type u} {s : set α} :
s ⊆ ∅ → s = ∅
source
theorem set.eq_empty_of_is_empty {α : Type u} [is_empty α] (s : set α) :
s = ∅
source
def set.unique_empty {α : Type u} [is_empty α] :
unique (set α)

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

Equations
source
theorem set.not_nonempty_iff_eq_empty {α : Type u} {s : set α} :
¬s.nonempty ↔ s = ∅
source
theorem set.empty_not_nonempty {α : Type u} :
¬∅.nonempty
source
theorem set.ne_empty_iff_nonempty {α : Type u} {s : set α} :
s ≠ ∅ ↔ s.nonempty
source
theorem set.eq_empty_or_nonempty {α : Type u} (s : set α) :
s = ∅ ∨ s.nonempty
source
theorem set.subset_eq_empty {α : Type u} {s t : set α} (h : t ⊆ s) (e : s = ∅) :
t = ∅
source
theorem set.ball_empty_iff {α : Type u} {p : α → Prop} :
(∀ (x : α), x ∈ ∅ → p x) ↔ true
source
@[protected, instance]
def set.has_emptyc.emptyc.is_empty (α : Type u) :
is_empty ↥∅

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.

source
@[simp]
theorem set.set_of_true {α : Type u} :
{x : α | true} = set.univ
source
@[simp]
theorem set.mem_univ {α : Type u} (x : α) :
x ∈ set.univ
source
@[simp]
theorem set.univ_eq_empty_iff {α : Type u} :
set.univ = ∅ ↔ is_empty α
source
theorem set.empty_ne_univ {α : Type u} [nonempty α] :
∅ ≠ set.univ
source
@[simp]
theorem set.subset_univ {α : Type u} (s : set α) :
s ⊆ set.univ
source
theorem set.univ_subset_iff {α : Type u} {s : set α} :
set.univ ⊆ s ↔ s = set.univ
source
theorem set.eq_univ_of_univ_subset {α : Type u} {s : set α} :
set.univ ⊆ s → s = set.univ
source
theorem set.eq_univ_iff_forall {α : Type u} {s : set α} :
s = set.univ ↔ ∀ (x : α), x ∈ s
source
theorem set.eq_univ_of_forall {α : Type u} {s : set α} :
(∀ (x : α), x ∈ s) → s = set.univ
source
theorem set.eq_univ_of_subset {α : Type u} {s t : set α} (h : s ⊆ t) (hs : s = set.univ) :
t = set.univ
source
theorem set.exists_mem_of_nonempty (α : Type u_1) [nonempty α] :
∃ (x : α), x ∈ set.univ
source
@[protected, instance]
def set.univ_decidable {α : Type u} :
decidable_pred (λ (_x : α), _x ∈ set.univ)
Equations
source
theorem set.ne_univ_iff_exists_not_mem {α : Type u_1} (s : set α) :
s ≠ set.univ ↔ ∃ (a : α), a ∉ s
source
theorem set.not_subset_iff_exists_mem_not_mem {α : Type u_1} {s t : set α} :
¬s ⊆ t ↔ ∃ (x : α), x ∈ s ∧ x ∉ t
source
theorem set.univ_unique {α : Type u} [unique α] :
set.univ = {default α}

Lemmas about union #

source
theorem set.union_def {α : Type u} {s₁ s₂ : set α} :
s₁ ∪ s₂ = {a : α | a ∈ s₁ ∨ a ∈ s₂}
source
theorem set.mem_union_left {α : Type u} {x : α} {a : set α} (b : set α) :
x ∈ a → x ∈ a ∪ b
source
theorem set.mem_union_right {α : Type u} {x : α} {b : set α} (a : set α) :
x ∈ b → x ∈ a ∪ b
source
theorem set.mem_or_mem_of_mem_union {α : Type u} {x : α} {a b : set α} (H : x ∈ a ∪ b) :
x ∈ a ∨ x ∈ b
source
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
source
theorem set.mem_union {α : Type u} (x : α) (a b : set α) :
x ∈ a ∪ b ↔ x ∈ a ∨ x ∈ b
source
@[simp]
theorem set.mem_union_eq {α : Type u} (x : α) (a b : set α) :
x ∈ a ∪ b = (x ∈ a ∨ x ∈ b)
source
@[simp]
theorem set.union_self {α : Type u} (a : set α) :
a ∪ a = a
source
@[simp]
theorem set.union_empty {α : Type u} (a : set α) :
a ∪ ∅ = a
source
@[simp]
theorem set.empty_union {α : Type u} (a : set α) :
∅ ∪ a = a
source
theorem set.union_comm {α : Type u} (a b : set α) :
a ∪ b = b ∪ a
source
theorem set.union_assoc {α : Type u} (a b c : set α) :
a ∪ b ∪ c = a ∪ (b ∪ c)
source
@[protected, instance]
def set.union_is_assoc {α : Type u} :
is_associative (set α) has_union.union
source
@[protected, instance]
def set.union_is_comm {α : Type u} :
is_commutative (set α) has_union.union
source
theorem set.union_left_comm {α : Type u} (s₁ s₂ s₃ : set α) :
s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃)
source
theorem set.union_right_comm {α : Type u} (s₁ s₂ s₃ : set α) :
s₁ ∪ s₂ ∪ s₃ = s₁ ∪ s₃ ∪ s₂
source
@[simp]
theorem set.union_eq_left_iff_subset {α : Type u} {s t : set α} :
s ∪ t = s ↔ t ⊆ s
source
@[simp]
theorem set.union_eq_right_iff_subset {α : Type u} {s t : set α} :
s ∪ t = t ↔ s ⊆ t
source
theorem set.union_eq_self_of_subset_left {α : Type u} {s t : set α} (h : s ⊆ t) :
s ∪ t = t
source
theorem set.union_eq_self_of_subset_right {α : Type u} {s t : set α} (h : t ⊆ s) :
s ∪ t = s
source
@[simp]
theorem set.subset_union_left {α : Type u} (s t : set α) :
s ⊆ s ∪ t
source
@[simp]
theorem set.subset_union_right {α : Type u} (s t : set α) :
t ⊆ s ∪ t
source
theorem set.union_subset {α : Type u} {s t r : set α} (sr : s ⊆ r) (tr : t ⊆ r) :
s ∪ t ⊆ r
source
@[simp]
theorem set.union_subset_iff {α : Type u} {s t u : set α} :
s ∪ t ⊆ u ↔ s ⊆ u ∧ t ⊆ u
source
theorem set.union_subset_union {α : Type u} {s₁ s₂ t₁ t₂ : set α} (h₁ : s₁ ⊆ s₂) (h₂ : t₁ ⊆ t₂) :
s₁ ∪ t₁ ⊆ s₂ ∪ t₂
source
theorem set.union_subset_union_left {α : Type u} {s₁ s₂ : set α} (t : set α) (h : s₁ ⊆ s₂) :
s₁ ∪ t ⊆ s₂ ∪ t
source
theorem set.union_subset_union_right {α : Type u} (s : set α) {t₁ t₂ : set α} (h : t₁ ⊆ t₂) :
s ∪ t₁ ⊆ s ∪ t₂
source
theorem set.subset_union_of_subset_left {α : Type u} {s t : set α} (h : s ⊆ t) (u : set α) :
s ⊆ t ∪ u
source
theorem set.subset_union_of_subset_right {α : Type u} {s u : set α} (h : s ⊆ u) (t : set α) :
s ⊆ t ∪ u
source
@[simp]
theorem set.union_empty_iff {α : Type u} {s t : set α} :
s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅
source
@[simp]
theorem set.union_univ {α : Type u} {s : set α} :
s ∪ set.univ = set.univ
source
@[simp]
theorem set.univ_union {α : Type u} {s : set α} :
set.univ ∪ s = set.univ

Lemmas about intersection #

source
theorem set.inter_def {α : Type u} {s₁ s₂ : set α} :
s₁ ∩ s₂ = {a : α | a ∈ s₁ ∧ a ∈ s₂}
source
theorem set.mem_inter_iff {α : Type u} (x : α) (a b : set α) :
x ∈ a ∩ b ↔ x ∈ a ∧ x ∈ b
source
@[simp]
theorem set.mem_inter_eq {α : Type u} (x : α) (a b : set α) :
x ∈ a ∩ b = (x ∈ a ∧ x ∈ b)
source
theorem set.mem_inter {α : Type u} {x : α} {a b : set α} (ha : x ∈ a) (hb : x ∈ b) :
x ∈ a ∩ b
source
theorem set.mem_of_mem_inter_left {α : Type u} {x : α} {a b : set α} (h : x ∈ a ∩ b) :
x ∈ a
source
theorem set.mem_of_mem_inter_right {α : Type u} {x : α} {a b : set α} (h : x ∈ a ∩ b) :
x ∈ b
source
@[simp]
theorem set.inter_self {α : Type u} (a : set α) :
a ∩ a = a
source
@[simp]
theorem set.inter_empty {α : Type u} (a : set α) :
a ∩ ∅ = ∅
source
@[simp]
theorem set.empty_inter {α : Type u} (a : set α) :
∅ ∩ a = ∅
source
theorem set.inter_comm {α : Type u} (a b : set α) :
a ∩ b = b ∩ a
source
theorem set.inter_assoc {α : Type u} (a b c : set α) :
a ∩ b ∩ c = a ∩ (b ∩ c)
source
@[protected, instance]
def set.inter_is_assoc {α : Type u} :
is_associative (set α) has_inter.inter
source
@[protected, instance]
def set.inter_is_comm {α : Type u} :
is_commutative (set α) has_inter.inter
source
theorem set.inter_left_comm {α : Type u} (s₁ s₂ s₃ : set α) :
s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃)
source
theorem set.inter_right_comm {α : Type u} (s₁ s₂ s₃ : set α) :
s₁ ∩ s₂ ∩ s₃ = s₁ ∩ s₃ ∩ s₂
source
@[simp]
theorem set.inter_subset_left {α : Type u} (s t : set α) :
s ∩ t ⊆ s
source
@[simp]
theorem set.inter_subset_right {α : Type u} (s t : set α) :
s ∩ t ⊆ t
source
theorem set.subset_inter {α : Type u} {s t r : set α} (rs : r ⊆ s) (rt : r ⊆ t) :
r ⊆ s ∩ t
source
@[simp]
theorem set.subset_inter_iff {α : Type u} {s t r : set α} :
r ⊆ s ∩ t ↔ r ⊆ s ∧ r ⊆ t
source
@[simp]
theorem set.inter_eq_left_iff_subset {α : Type u} {s t : set α} :
s ∩ t = s ↔ s ⊆ t
source
@[simp]
theorem set.inter_eq_right_iff_subset {α : Type u} {s t : set α} :
s ∩ t = t ↔ t ⊆ s
source
theorem set.inter_eq_self_of_subset_left {α : Type u} {s t : set α} :
s ⊆ t → s ∩ t = s
source
theorem set.inter_eq_self_of_subset_right {α : Type u} {s t : set α} :
t ⊆ s → s ∩ t = t
source
@[simp]
theorem set.inter_univ {α : Type u} (a : set α) :
a ∩ set.univ = a
source
@[simp]
theorem set.univ_inter {α : Type u} (a : set α) :
set.univ ∩ a = a
source
theorem set.inter_subset_inter {α : Type u} {s₁ s₂ t₁ t₂ : set α} (h₁ : s₁ ⊆ t₁) (h₂ : s₂ ⊆ t₂) :
s₁ ∩ s₂ ⊆ t₁ ∩ t₂
source
theorem set.inter_subset_inter_left {α : Type u} {s t : set α} (u : set α) (H : s ⊆ t) :
s ∩ u ⊆ t ∩ u
source
theorem set.inter_subset_inter_right {α : Type u} {s t : set α} (u : set α) (H : s ⊆ t) :
u ∩ s ⊆ u ∩ t
source
theorem set.union_inter_cancel_left {α : Type u} {s t : set α} :
(s ∪ t) ∩ s = s
source
theorem set.union_inter_cancel_right {α : Type u} {s t : set α} :
(s ∪ t) ∩ t = t

Distributivity laws #

source
theorem set.inter_distrib_left {α : Type u} (s t u : set α) :
s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u
source
theorem set.inter_union_distrib_left {α : Type u} {s t u : set α} :
s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u
source
theorem set.inter_distrib_right {α : Type u} (s t u : set α) :
(s ∪ t) ∩ u = s ∩ u ∪ t ∩ u
source
theorem set.union_inter_distrib_right {α : Type u} {s t u : set α} :
(s ∪ t) ∩ u = s ∩ u ∪ t ∩ u
source
theorem set.union_distrib_left {α : Type u} (s t u : set α) :
s ∪ t ∩ u = (s ∪ t) ∩ (s ∪ u)
source
theorem set.union_inter_distrib_left {α : Type u} {s t u : set α} :
s ∪ t ∩ u = (s ∪ t) ∩ (s ∪ u)
source
theorem set.union_distrib_right {α : Type u} (s t u : set α) :
s ∩ t ∪ u = (s ∪ u) ∩ (t ∪ u)
source
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.

source
theorem set.insert_def {α : Type u} (x : α) (s : set α) :
insert x s = {y : α | y = x ∨ y ∈ s}
source
@[simp]
theorem set.subset_insert {α : Type u} (x : α) (s : set α) :
s ⊆ insert x s
source
theorem set.mem_insert {α : Type u} (x : α) (s : set α) :
x ∈ insert x s
source
theorem set.mem_insert_of_mem {α : Type u} {x : α} {s : set α} (y : α) :
x ∈ s → x ∈ insert y s
source
theorem set.eq_or_mem_of_mem_insert {α : Type u} {x a : α} {s : set α} :
x ∈ insert a s → x = a ∨ x ∈ s
source
theorem set.mem_of_mem_insert_of_ne {α : Type u} {x a : α} {s : set α} :
x ∈ insert a s → x ≠ a → x ∈ s
source
@[simp]
theorem set.mem_insert_iff {α : Type u} {x a : α} {s : set α} :
x ∈ insert a s ↔ x = a ∨ x ∈ s
source
@[simp]
theorem set.insert_eq_of_mem {α : Type u} {a : α} {s : set α} (h : a ∈ s) :
insert a s = s
source
theorem set.ne_insert_of_not_mem {α : Type u} {s : set α} (t : set α) {a : α} :
a ∉ s → s ≠ insert a t
source
theorem set.insert_subset {α : Type u} {a : α} {s t : set α} :
insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t
source
theorem set.insert_subset_insert {α : Type u} {a : α} {s t : set α} (h : s ⊆ t) :
insert a s ⊆ insert a t
source
theorem set.insert_subset_insert_iff {α : Type u} {a : α} {s t : set α} (ha : a ∉ s) :
insert a s ⊆ insert a t ↔ s ⊆ t
source
theorem set.ssubset_iff_insert {α : Type u} {s t : set α} :
s ⊂ t ↔ ∃ (a : α) (H : a ∉ s), insert a s ⊆ t
source
theorem set.ssubset_insert {α : Type u} {s : set α} {a : α} (h : a ∉ s) :
s ⊂ insert a s
source
theorem set.insert_comm {α : Type u} (a b : α) (s : set α) :
insert a (insert b s) = insert b (insert a s)
source
theorem set.insert_union {α : Type u} {a : α} {s t : set α} :
insert a s ∪ t = insert a (s ∪ t)
source
@[simp]
theorem set.union_insert {α : Type u} {a : α} {s t : set α} :
s ∪ insert a t = insert a (s ∪ t)
source
theorem set.insert_nonempty {α : Type u} (a : α) (s : set α) :
(insert a s).nonempty
source
@[protected, instance]
def set.has_insert.insert.nonempty {α : Type u} (a : α) (s : set α) :
nonempty ↥(insert a s)
source
theorem set.insert_inter {α : Type u} (x : α) (s t : set α) :
insert x (s ∩ t) = insert x s ∩ insert x t
source
theorem set.forall_of_forall_insert {α : Type u} {P : α → Prop} {a : α} {s : set α} (H : ∀ (x : α), x ∈ insert a s → P x) (x : α) (h : x ∈ s) :
P x
source
theorem set.forall_insert_of_forall {α : Type u} {P : α → Prop} {a : α} {s : set α} (H : ∀ (x : α), x ∈ s → P x) (ha : P a) (x : α) (h : x ∈ insert a s) :
P x
source
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
source
theorem set.ball_insert_iff {α : Type u} {P : α → Prop} {a : α} {s : set α} :
(∀ (x : α), x ∈ insert a s → P x) ↔ P a ∧ ∀ (x : α), x ∈ s → P x

Lemmas about singletons #

source
theorem set.singleton_def {α : Type u} (a : α) :
{a} = {a}
source
@[simp]
theorem set.mem_singleton_iff {α : Type u} {a b : α} :
a ∈ {b} ↔ a = b
source
@[simp]
theorem set.set_of_eq_eq_singleton {α : Type u} {a : α} :
{n : α | n = a} = {a}
source
@[simp]
theorem set.set_of_eq_eq_singleton' {α : Type u} {a : α} :
{x : α | a = x} = {a}
source
@[simp]
theorem set.mem_singleton {α : Type u} (a : α) :
a ∈ {a}
source
theorem set.eq_of_mem_singleton {α : Type u} {x y : α} (h : x ∈ {y}) :
x = y
source
@[simp]
theorem set.singleton_eq_singleton_iff {α : Type u} {x y : α} :
{x} = {y} ↔ x = y
source
theorem set.mem_singleton_of_eq {α : Type u} {x y : α} (H : x = y) :
x ∈ {y}
source
theorem set.insert_eq {α : Type u} (x : α) (s : set α) :
insert x s = {x} ∪ s
source
@[simp]
theorem set.pair_eq_singleton {α : Type u} (a : α) :
{a, a} = {a}
source
theorem set.pair_comm {α : Type u} (a b : α) :
{a, b} = {b, a}
source
@[simp]
theorem set.singleton_nonempty {α : Type u} (a : α) :
{a}.nonempty
source
@[simp]
theorem set.singleton_subset_iff {α : Type u} {a : α} {s : set α} :
{a} ⊆ s ↔ a ∈ s
source
theorem set.set_compr_eq_eq_singleton {α : Type u} {a : α} :
{b : α | b = a} = {a}
source
@[simp]
theorem set.singleton_union {α : Type u} {a : α} {s : set α} :
{a} ∪ s = insert a s
source
@[simp]
theorem set.union_singleton {α : Type u} {a : α} {s : set α} :
s ∪ {a} = insert a s
source
@[simp]
theorem set.singleton_inter_nonempty {α : Type u} {a : α} {s : set α} :
({a} ∩ s).nonempty ↔ a ∈ s
source
@[simp]
theorem set.inter_singleton_nonempty {α : Type u} {a : α} {s : set α} :
(s ∩ {a}).nonempty ↔ a ∈ s
source
@[simp]
theorem set.singleton_inter_eq_empty {α : Type u} {a : α} {s : set α} :
{a} ∩ s = ∅ ↔ a ∉ s
source
@[simp]
theorem set.inter_singleton_eq_empty {α : Type u} {a : α} {s : set α} :
s ∩ {a} = ∅ ↔ a ∉ s
source
theorem set.nmem_singleton_empty {α : Type u} {s : set α} :
s ∉ {∅} ↔ s.nonempty
source
@[protected, instance]
def set.unique_singleton {α : Type u} (a : α) :
unique ↥{a}
Equations
source
theorem set.eq_singleton_iff_unique_mem {α : Type u} {a : α} {s : set α} :
s = {a} ↔ a ∈ s ∧ ∀ (x : α), x ∈ s → x = a
source
theorem set.eq_singleton_iff_nonempty_unique_mem {α : Type u} {a : α} {s : set α} :
s = {a} ↔ s.nonempty ∧ ∀ (x : α), x ∈ s → x = a
source
theorem set.exists_eq_singleton_iff_nonempty_unique_mem {α : Type u} {s : set α} :
(∃ (a : α), s = {a}) ↔ s.nonempty ∧ ∀ (a b : α), a ∈ s → b ∈ s → a = b
source
@[simp]
theorem set.default_coe_singleton {α : Type u} (x : α) :
default ↥{x} = ⟨x, _⟩

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

source
theorem set.mem_sep {α : Type u} {s : set α} {p : α → Prop} {x : α} (xs : x ∈ s) (px : p x) :
x ∈ {x ∈ s | p x}
source
@[simp]
theorem set.sep_mem_eq {α : Type u} {s t : set α} :
{x ∈ s | x ∈ t} = s ∩ t
source
@[simp]
theorem set.mem_sep_eq {α : Type u} {s : set α} {p : α → Prop} {x : α} :
x ∈ {x ∈ s | p x} = (x ∈ s ∧ p x)
source
theorem set.mem_sep_iff {α : Type u} {s : set α} {p : α → Prop} {x : α} :
x ∈ {x ∈ s | p x} ↔ x ∈ s ∧ p x
source
theorem set.eq_sep_of_subset {α : Type u} {s t : set α} (h : s ⊆ t) :
s = {x ∈ t | x ∈ s}
source
@[simp]
theorem set.sep_subset {α : Type u} (s : set α) (p : α → Prop) :
{x ∈ s | p x} ⊆ s
source
theorem set.forall_not_of_sep_empty {α : Type u} {s : set α} {p : α → Prop} (H : {x ∈ s | p x} = ∅) (x : α) :
x ∈ s → ¬p x
source
@[simp]
theorem set.sep_univ {α : Type u_1} {p : α → Prop} :
{a ∈ set.univ | p a} = {a : α | p a}
source
@[simp]
theorem set.sep_true {α : Type u} {s : set α} :
{a ∈ s | true} = s
source
@[simp]
theorem set.sep_false {α : Type u} {s : set α} :
{a ∈ s | false} = ∅
source
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}
source
@[simp]
theorem set.subset_singleton_iff {α : Type u_1} {s : set α} {x : α} :
s ⊆ {x} ↔ ∀ (y : α), y ∈ s → y = x
source
theorem set.subset_singleton_iff_eq {α : Type u} {s : set α} {x : α} :
s ⊆ {x} ↔ s = ∅ ∨ s = {x}
source
theorem set.ssubset_singleton_iff {α : Type u} {s : set α} {x : α} :
s ⊂ {x} ↔ s = ∅
source
theorem set.eq_empty_of_ssubset_singleton {α : Type u} {s : set α} {x : α} (hs : s ⊂ {x}) :
s = ∅

Lemmas about complement #

source
theorem set.mem_compl {α : Type u} {s : set α} {x : α} (h : x ∉ s) :
x ∈ sᶜ
source
theorem set.compl_set_of {α : Type u_1} (p : α → Prop) :
{a : α | p a}ᶜ = {a : α | ¬p a}
source
theorem set.not_mem_of_mem_compl {α : Type u} {s : set α} {x : α} (h : x ∈ sᶜ) :
x ∉ s
source
@[simp]
theorem set.mem_compl_eq {α : Type u} (s : set α) (x : α) :
x ∈ sᶜ = (x ∉ s)
source
theorem set.mem_compl_iff {α : Type u} (s : set α) (x : α) :
x ∈ sᶜ ↔ x ∉ s
source
@[simp]
theorem set.inter_compl_self {α : Type u} (s : set α) :
s ∩ sᶜ = ∅
source
@[simp]
theorem set.compl_inter_self {α : Type u} (s : set α) :
sᶜ ∩ s = ∅
source
@[simp]
theorem set.compl_empty {α : Type u} :
∅ᶜ = set.univ
source
@[simp]
theorem set.compl_union {α : Type u} (s t : set α) :
(s ∪ t)ᶜ = sᶜ ∩ tᶜ
source
theorem set.compl_inter {α : Type u} (s t : set α) :
(s ∩ t)ᶜ = sᶜ ∪ tᶜ
source
@[simp]
theorem set.compl_univ {α : Type u} :
set.univᶜ = ∅
source
@[simp]
theorem set.compl_empty_iff {α : Type u} {s : set α} :
sᶜ = ∅ ↔ s = set.univ
source
@[simp]
theorem set.compl_univ_iff {α : Type u} {s : set α} :
sᶜ = set.univ ↔ s = ∅
source
theorem set.nonempty_compl {α : Type u} {s : set α} :
sᶜ.nonempty ↔ s ≠ set.univ
source
theorem set.mem_compl_singleton_iff {α : Type u} {a x : α} :
x ∈ {a}ᶜ ↔ x ≠ a
source
theorem set.compl_singleton_eq {α : Type u} (a : α) :
{a}ᶜ = {x : α | x ≠ a}
source
@[simp]
theorem set.compl_ne_eq_singleton {α : Type u} (a : α) :
{x : α | x ≠ a}ᶜ = {a}
source
theorem set.union_eq_compl_compl_inter_compl {α : Type u} (s t : set α) :
s ∪ t = (sᶜ ∩ tᶜ)ᶜ
source
theorem set.inter_eq_compl_compl_union_compl {α : Type u} (s t : set α) :
s ∩ t = (sᶜ ∪ tᶜ)ᶜ
source
@[simp]
theorem set.union_compl_self {α : Type u} (s : set α) :
s ∪ sᶜ = set.univ
source
@[simp]
theorem set.compl_union_self {α : Type u} (s : set α) :
sᶜ ∪ s = set.univ
source
theorem set.compl_comp_compl {α : Type u} :
compl ∘ compl = id
source
theorem set.compl_subset_comm {α : Type u} {s t : set α} :
sᶜ ⊆ t ↔ tᶜ ⊆ s
source
@[simp]
theorem set.compl_subset_compl {α : Type u} {s t : set α} :
sᶜ ⊆ tᶜ ↔ t ⊆ s
source
theorem set.subset_union_compl_iff_inter_subset {α : Type u} {s t u : set α} :
s ⊆ t ∪ uᶜ ↔ s ∩ u ⊆ t
source
theorem set.compl_subset_iff_union {α : Type u} {s t : set α} :
sᶜ ⊆ t ↔ s ∪ t = set.univ
source
theorem set.subset_compl_comm {α : Type u} {s t : set α} :
s ⊆ tᶜ ↔ t ⊆ sᶜ
source
theorem set.subset_compl_iff_disjoint {α : Type u} {s t : set α} :
s ⊆ tᶜ ↔ s ∩ t = ∅
source
theorem set.subset_compl_singleton_iff {α : Type u} {a : α} {s : set α} :
s ⊆ {a}ᶜ ↔ a ∉ s
source
theorem set.inter_subset {α : Type u} (a b c : set α) :
a ∩ b ⊆ c ↔ a ⊆ bᶜ ∪ c
source
theorem set.inter_compl_nonempty_iff {α : Type u} {s t : set α} :
(s ∩ tᶜ).nonempty ↔ ¬s ⊆ t

Lemmas about set difference #

source
theorem set.diff_eq {α : Type u} (s t : set α) :
s \ t = s ∩ tᶜ
source
@[simp]
theorem set.mem_diff {α : Type u} {s t : set α} (x : α) :
x ∈ s \ t ↔ x ∈ s ∧ x ∉ t
source
theorem set.mem_diff_of_mem {α : Type u} {s t : set α} {x : α} (h1 : x ∈ s) (h2 : x ∉ t) :
x ∈ s \ t
source
theorem set.mem_of_mem_diff {α : Type u} {s t : set α} {x : α} (h : x ∈ s \ t) :
x ∈ s
source
theorem set.not_mem_of_mem_diff {α : Type u} {s t : set α} {x : α} (h : x ∈ s \ t) :
x ∉ t
source
theorem set.diff_eq_compl_inter {α : Type u} {s t : set α} :
s \ t = tᶜ ∩ s
source
theorem set.nonempty_diff {α : Type u} {s t : set α} :
(s \ t).nonempty ↔ ¬s ⊆ t
source
theorem set.diff_subset {α : Type u} (s t : set α) :
s \ t ⊆ s
source
theorem set.union_diff_cancel' {α : Type u} {s t u : set α} (h₁ : s ⊆ t) (h₂ : t ⊆ u) :
t ∪ u \ s = u
source
theorem set.union_diff_cancel {α : Type u} {s t : set α} (h : s ⊆ t) :
s ∪ t \ s = t
source
theorem set.union_diff_cancel_left {α : Type u} {s t : set α} (h : s ∩ t ⊆ ∅) :
(s ∪ t) \ s = t
source
theorem set.union_diff_cancel_right {α : Type u} {s t : set α} (h : s ∩ t ⊆ ∅) :
(s ∪ t) \ t = s
source
@[simp]
theorem set.union_diff_left {α : Type u} {s t : set α} :
(s ∪ t) \ s = t \ s
source
@[simp]
theorem set.union_diff_right {α : Type u} {s t : set α} :
(s ∪ t) \ t = s \ t
source
theorem set.union_diff_distrib {α : Type u} {s t u : set α} :
(s ∪ t) \ u = s \ u ∪ t \ u
source
theorem set.inter_diff_assoc {α : Type u} (a b c : set α) :
a ∩ b \ c = a ∩ (b \ c)
source
@[simp]
theorem set.inter_diff_self {α : Type u} (a b : set α) :
a ∩ (b \ a) = ∅
source
@[simp]
theorem set.inter_union_diff {α : Type u} (s t : set α) :
s ∩ t ∪ s \ t = s
source
@[simp]
theorem set.diff_union_inter {α : Type u} (s t : set α) :
s \ t ∪ s ∩ t = s
source
@[simp]
theorem set.inter_union_compl {α : Type u} (s t : set α) :
s ∩ t ∪ s ∩ tᶜ = s
source
theorem set.diff_subset_diff {α : Type u} {s₁ s₂ t₁ t₂ : set α} :
s₁ ⊆ s₂ → t₂ ⊆ t₁ → s₁ \ t₁ ⊆ s₂ \ t₂
source
theorem set.diff_subset_diff_left {α : Type u} {s₁ s₂ t : set α} (h : s₁ ⊆ s₂) :
s₁ \ t ⊆ s₂ \ t
source
theorem set.diff_subset_diff_right {α : Type u} {s t u : set α} (h : t ⊆ u) :
s \ u ⊆ s \ t
source
theorem set.compl_eq_univ_diff {α : Type u} (s : set α) :
sᶜ = set.univ \ s
source
@[simp]
theorem set.empty_diff {α : Type u} (s : set α) :
∅ \ s = ∅
source
theorem set.diff_eq_empty {α : Type u} {s t : set α} :
s \ t = ∅ ↔ s ⊆ t
source
@[simp]
theorem set.diff_empty {α : Type u} {s : set α} :
s \ ∅ = s
source
@[simp]
theorem set.diff_univ {α : Type u} (s : set α) :
s \ set.univ = ∅
source
theorem set.diff_diff {α : Type u} {s t u : set α} :
s \ t \ u = s \ (t ∪ u)
source
theorem set.diff_diff_comm {α : Type u} {s t u : set α} :
s \ t \ u = s \ u \ t
source
theorem set.diff_subset_iff {α : Type u} {s t u : set α} :
s \ t ⊆ u ↔ s ⊆ t ∪ u
source
theorem set.subset_diff_union {α : Type u} (s t : set α) :
s ⊆ s \ t ∪ t
source
theorem set.diff_union_of_subset {α : Type u} {s t : set α} (h : t ⊆ s) :
s \ t ∪ t = s
source
@[simp]
theorem set.diff_singleton_subset_iff {α : Type u} {x : α} {s t : set α} :
s \ {x} ⊆ t ↔ s ⊆ insert x t
source
theorem set.subset_diff_singleton {α : Type u} {x : α} {s t : set α} (h : s ⊆ t) (hx : x ∉ s) :
s ⊆ t \ {x}
source
theorem set.subset_insert_diff_singleton {α : Type u} (x : α) (s : set α) :
s ⊆ insert x (s \ {x})
source
theorem set.diff_subset_comm {α : Type u} {s t u : set α} :
s \ t ⊆ u ↔ s \ u ⊆ t
source
theorem set.diff_inter {α : Type u} {s t u : set α} :
s \ (t ∩ u) = s \ t ∪ s \ u
source
theorem set.diff_inter_diff {α : Type u} {s t u : set α} :
s \ t ∩ (s \ u) = s \ (t ∪ u)
source
theorem set.diff_compl {α : Type u} {s t : set α} :
s \ tᶜ = s ∩ t
source
theorem set.diff_diff_right {α : Type u} {s t u : set α} :
s \ (t \ u) = s \ t ∪ s ∩ u
source
@[simp]
theorem set.insert_diff_of_mem {α : Type u} {a : α} {t : set α} (s : set α) (h : a ∈ t) :
insert a s \ t = s \ t
source
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)
source
theorem set.insert_diff_self_of_not_mem {α : Type u} {a : α} {s : set α} (h : a ∉ s) :
insert a s \ {a} = s
source
theorem set.insert_inter_of_mem {α : Type u} {s₁ s₂ : set α} {a : α} (h : a ∈ s₂) :
insert a s₁ ∩ s₂ = insert a (s₁ ∩ s₂)
source
theorem set.insert_inter_of_not_mem {α : Type u} {s₁ s₂ : set α} {a : α} (h : a ∉ s₂) :
insert a s₁ ∩ s₂ = s₁ ∩ s₂
source
@[simp]
theorem set.union_diff_self {α : Type u} {s t : set α} :
s ∪ t \ s = s ∪ t
source
@[simp]
theorem set.diff_union_self {α : Type u} {s t : set α} :
s \ t ∪ t = s ∪ t
source
@[simp]
theorem set.diff_inter_self {α : Type u} {a b : set α} :
b \ a ∩ a = ∅
source
@[simp]
theorem set.diff_inter_self_eq_diff {α : Type u} {s t : set α} :
s \ (t ∩ s) = s \ t
source
@[simp]
theorem set.diff_self_inter {α : Type u} {s t : set α} :
s \ (s ∩ t) = s \ t
source
@[simp]
theorem set.diff_eq_self {α : Type u} {s t : set α} :
s \ t = s ↔ t ∩ s ⊆ ∅
source
@[simp]
theorem set.diff_singleton_eq_self {α : Type u} {a : α} {s : set α} (h : a ∉ s) :
s \ {a} = s
source
@[simp]
theorem set.insert_diff_singleton {α : Type u} {a : α} {s : set α} :
insert a (s \ {a}) = insert a s
source
@[simp]
theorem set.diff_self {α : Type u} {s : set α} :
s \ s = ∅
source
theorem set.diff_diff_cancel_left {α : Type u} {s t : set α} (h : s ⊆ t) :
t \ (t \ s) = s
source
theorem set.mem_diff_singleton {α : Type u} {x y : α} {s : set α} :
x ∈ s \ {y} ↔ x ∈ s ∧ x ≠ y
source
theorem set.mem_diff_singleton_empty {α : Type u} {s : set α} {t : set (set α)} :
s ∈ t \ {∅} ↔ s ∈ t ∧ s.nonempty
source
theorem set.union_eq_diff_union_diff_union_inter {α : Type u} (s t : set α) :
s ∪ t = s \ t ∪ t \ s ∪ s ∩ t

Powerset #

source
theorem set.mem_powerset {α : Type u} {x s : set α} (h : x ⊆ s) :
x ∈ 𝒫s
source
theorem set.subset_of_mem_powerset {α : Type u} {x s : set α} (h : x ∈ 𝒫s) :
x ⊆ s
source
@[simp]
theorem set.mem_powerset_iff {α : Type u} (x s : set α) :
x ∈ 𝒫s ↔ x ⊆ s
source
theorem set.powerset_inter {α : Type u} (s t : set α) :
𝒫(s ∩ t) = 𝒫s ∩ 𝒫t
source
@[simp]
theorem set.powerset_mono {α : Type u} {s t : set α} :
𝒫s ⊆ 𝒫t ↔ s ⊆ t
source
theorem set.monotone_powerset {α : Type u} :
monotone set.powerset
source
@[simp]
theorem set.powerset_nonempty {α : Type u} {s : set α} :
(𝒫s).nonempty
source
@[simp]
theorem set.powerset_empty {α : Type u} :
𝒫∅ = {∅}
source
@[simp]
theorem set.powerset_univ {α : Type u} :
𝒫set.univ = set.univ

If-then-else for sets #

source
@[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
source
@[simp]
theorem set.ite_inter_self {α : Type u} (t s s' : set α) :
t.ite s s' ∩ t = s ∩ t
source
@[simp]
theorem set.ite_compl {α : Type u} (t s s' : set α) :
tᶜ.ite s s' = t.ite s' s
source
@[simp]
theorem set.ite_inter_compl_self {α : Type u} (t s s' : set α) :
t.ite s s' ∩ tᶜ = s' ∩ tᶜ
source
@[simp]
theorem set.ite_diff_self {α : Type u} (t s s' : set α) :
t.ite s s' \ t = s' \ t
source
@[simp]
theorem set.ite_same {α : Type u} (t s : set α) :
t.ite s s = s
source
@[simp]
theorem set.ite_left {α : Type u} (s t : set α) :
s.ite s t = s ∪ t
source
@[simp]
theorem set.ite_right {α : Type u} (s t : set α) :
s.ite t s = t ∩ s
source
@[simp]
theorem set.ite_empty {α : Type u} (s s' : set α) :
∅.ite s s' = s'
source
@[simp]
theorem set.ite_univ {α : Type u} (s s' : set α) :
set.univ.ite s s' = s
source
@[simp]
theorem set.ite_empty_left {α : Type u} (t s : set α) :
t.ite ∅ s = s \ t
source
@[simp]
theorem set.ite_empty_right {α : Type u} (t s : set α) :
t.ite s ∅ = s ∩ t
source
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₂'
source
theorem set.ite_subset_union {α : Type u} (t s s' : set α) :
t.ite s s' ⊆ s ∪ s'
source
theorem set.inter_subset_ite {α : Type u} (t s s' : set α) :
s ∩ s' ⊆ t.ite s s'
source
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₂'
source
theorem set.ite_inter {α : Type u} (t s₁ s₂ s : set α) :
t.ite (s₁ ∩ s) (s₂ ∩ s) = t.ite s₁ s₂ ∩ s
source
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
source
theorem set.subset_ite {α : Type u} {t s s' u : set α} :
u ⊆ t.ite s s' ↔ u ∩ t ⊆ s ∧ u \ t ⊆ s'

Inverse image #

source
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
source
@[simp]
theorem set.preimage_empty {α : Type u} {β : Type v} {f : α → β} :
f ⁻¹' ∅ = ∅
source
@[simp]
theorem set.mem_preimage {α : Type u} {β : Type v} {f : α → β} {s : set β} {a : α} :
a ∈ f ⁻¹' s ↔ f a ∈ s
source
theorem set.preimage_congr {α : Type u} {β : Type v} {f g : α → β} {s : set β} (h : ∀ (x : α), f x = g x) :
f ⁻¹' s = g ⁻¹' s
source
theorem set.preimage_mono {α : Type u} {β : Type v} {f : α → β} {s t : set β} (h : s ⊆ t) :
f ⁻¹' s ⊆ f ⁻¹' t
source
@[simp]
theorem set.preimage_univ {α : Type u} {β : Type v} {f : α → β} :
f ⁻¹' set.univ = set.univ
source
theorem set.subset_preimage_univ {α : Type u} {β : Type v} {f : α → β} {s : set α} :
s ⊆ f ⁻¹' set.univ
source
@[simp]
theorem set.preimage_inter {α : Type u} {β : Type v} {f : α → β} {s t : set β} :
f ⁻¹' (s ∩ t) = f ⁻¹' s ∩ f ⁻¹' t
source
@[simp]
theorem set.preimage_union {α : Type u} {β : Type v} {f : α → β} {s t : set β} :
f ⁻¹' (s ∪ t) = f ⁻¹' s ∪ f ⁻¹' t
source
@[simp]
theorem set.preimage_compl {α : Type u} {β : Type v} {f : α → β} {s : set β} :
f ⁻¹' sᶜ = (f ⁻¹' s)ᶜ
source
@[simp]
theorem set.preimage_diff {α : Type u} {β : Type v} (f : α → β) (s t : set β) :
f ⁻¹' (s \ t) = f ⁻¹' s \ f ⁻¹' t
source
@[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₂)
source
@[simp]
theorem set.preimage_set_of_eq {α : Type u} {β : Type v} {p : α → Prop} {f : β → α} :
f ⁻¹' {a : α | p a} = {a : β | p (f a)}
source
@[simp]
theorem set.preimage_id {α : Type u} {s : set α} :
id ⁻¹' s = s
source
@[simp]
theorem set.preimage_id' {α : Type u} {s : set α} :
(λ (x : α), x) ⁻¹' s = s
source
@[simp]
theorem set.preimage_const_of_mem {α : Type u} {β : Type v} {b : β} {s : set β} (h : b ∈ s) :
(λ (x : α), b) ⁻¹' s = set.univ
source
@[simp]
theorem set.preimage_const_of_not_mem {α : Type u} {β : Type v} {b : β} {s : set β} (h : b ∉ s) :
(λ (x : α), b) ⁻¹' s = ∅
source
theorem set.preimage_const {α : Type u} {β : Type v} (b : β) (s : set β) [decidable (b ∈ s)] :
(λ (x : α), b) ⁻¹' s = ite (b ∈ s) set.univ ∅
source
theorem set.preimage_comp {α : Type u} {β : Type v} {γ : Type w} {f : α → β} {g : β → γ} {s : set γ} :
g ∘ f ⁻¹' s = f ⁻¹' (g ⁻¹' s)
source
theorem set.preimage_preimage {α : Type u} {β : Type v} {γ : Type w} {g : β → γ} {f : α → β} {s : set γ} :
f ⁻¹' (g ⁻¹' s) = (λ (x : α), g (f x)) ⁻¹' s
source
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
source
theorem set.nonempty_of_nonempty_preimage {α : Type u} {β : Type v} {s : set β} {f : α → β} (hf : (f ⁻¹' s).nonempty) :
s.nonempty

Image of a set under a function #

source
theorem set.mem_image_iff_bex {α : Type u} {β : Type v} {f : α → β} {s : set α} {y : β} :
y ∈ f '' s ↔ ∃ (x : α) (_x : x ∈ s), f x = y
source
theorem set.mem_image_eq {α : Type u} {β : Type v} (f : α → β) (s : set α) (y : β) :
y ∈ f '' s = ∃ (x : α), x ∈ s ∧ f x = y
source
@[simp]
theorem set.mem_image {α : Type u} {β : Type v} (f : α → β) (s : set α) (y : β) :
y ∈ f '' s ↔ ∃ (x : α), x ∈ s ∧ f x = y
source
theorem set.image_eta {α : Type u} {β : Type v} {s : set α} (f : α → β) :
f '' s = (λ (x : α), f x) '' s
source
theorem set.mem_image_of_mem {α : Type u} {β : Type v} (f : α → β) {x : α} {a : set α} (h : x ∈ a) :
f x ∈ f '' a
source
theorem function.injective.mem_set_image {α : Type u} {β : Type v} {f : α → β} (hf : function.injective f) {s : set α} {a : α} :
f a ∈ f '' s ↔ a ∈ s
source
theorem set.ball_image_iff {α : Type u} {β : Type v} {f : α → β} {s : set α} {p : β → Prop} :
(∀ (y : β), y ∈ f '' s → p y) ↔ ∀ (x : α), x ∈ s → p (f x)
source
theorem set.ball_image_of_ball {α : Type u} {β : Type v} {f : α → β} {s : set α} {p : β → Prop} (h : ∀ (x : α), x ∈ s → p (f x)) (y : β) (H : y ∈ f '' s) :
p y
source
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)
source
theorem set.mem_image_elim {α : Type u} {β : Type v} {f : α → β} {s : set α} {C : β → Prop} (h : ∀ (x : α), x ∈ s → C (f x)) {y : β} :
y ∈ f '' s → C y
source
theorem set.mem_image_elim_on {α : Type u} {β : Type v} {f : α → β} {s : set α} {C : β → Prop} {y : β} (h_y : y ∈ f '' s) (h : ∀ (x : α), x ∈ s → C (f x)) :
C y
source
theorem set.image_congr {α : Type u} {β : Type v} {f g : α → β} {s : set α} (h : ∀ (a : α), a ∈ s → f a = g a) :
f '' s = g '' s
source
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

source
theorem set.image_comp {α : Type u} {β : Type v} {γ : Type w} (f : β → γ) (g : α → β) (a : set α) :
f ∘ g '' a = f '' (g '' a)
source
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

source
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 ≤.

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

A variant of image_id

source
theorem set.image_id {α : Type u} (s : set α) :
id '' s = s
source
theorem set.compl_compl_image {α : Type u} (S : set (set α)) :
compl '' (compl '' S) = S
source
theorem set.image_insert_eq {α : Type u} {β : Type v} {f : α → β} {a : α} {s : set α} :
f '' insert a s = insert (f a) (f '' s)
source
theorem set.image_pair {α : Type u} {β : Type v} (f : α → β) (a b : α) :
f '' {a, b} = {f a, f b}
source
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
source
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
source
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) :
set.image f = set.preimage g
source
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
source
theorem set.image_compl_subset {α : Type u} {β : Type v} {f : α → β} {s : set α} (H : function.injective f) :
f '' sᶜ ⊆ (f '' s)ᶜ
source
theorem set.subset_image_compl {α : Type u} {β : Type v} {f : α → β} {s : set α} (H : function.surjective f) :
(f '' s)ᶜ ⊆ f '' sᶜ
source
theorem set.image_compl_eq {α : Type u} {β : Type v} {f : α → β} {s : set α} (H : function.bijective f) :
f '' sᶜ = (f '' s)ᶜ
source
theorem set.subset_image_diff {α : Type u} {β : Type v} (f : α → β) (s t : set α) :
f '' s \ f '' t ⊆ f '' (s \ t)
source
theorem set.image_diff {α : Type u} {β : Type v} {f : α → β} (hf : function.injective f) (s t : set α) :
f '' (s \ t) = f '' s \ f '' t
source
theorem set.nonempty.image {α : Type u} {β : Type v} (f : α → β) {s : set α} :
s.nonempty → (f '' s).nonempty
source
theorem set.nonempty.of_image {α : Type u} {β : Type v} {f : α → β} {s : set α} :
(f '' s).nonempty → s.nonempty
source
@[simp]
theorem set.nonempty_image_iff {α : Type u} {β : Type v} {f : α → β} {s : set α} :
(f '' s).nonempty ↔ s.nonempty
source
theorem set.nonempty.preimage {α : Type u} {β : Type v} {s : set β} (hs : s.nonempty) {f : α → β} (hf : function.surjective f) :
(f ⁻¹' s).nonempty
source
@[protected, instance]
def set.image.nonempty {α : Type u} {β : Type v} (f : α → β) (s : set α) [nonempty ↥s] :
nonempty ↥(f '' s)
source
@[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

source
theorem set.image_preimage_subset {α : Type u} {β : Type v} (f : α → β) (s : set β) :
f '' (f ⁻¹' s) ⊆ s
source
theorem set.subset_preimage_image {α : Type u} {β : Type v} (f : α → β) (s : set α) :
s ⊆ f ⁻¹' (f '' s)
source
theorem set.preimage_image_eq {α : Type u} {β : Type v} {f : α → β} (s : set α) (h : function.injective f) :
f ⁻¹' (f '' s) = s
source
theorem set.image_preimage_eq {α : Type u} {β : Type v} {f : α → β} (s : set β) (h : function.surjective f) :
f '' (f ⁻¹' s) = s
source
theorem set.preimage_eq_preimage {α : Type u} {β : Type v} {s t : set α} {f : β → α} (hf : function.surjective f) :
f ⁻¹' s = f ⁻¹' t ↔ s = t
source
theorem set.image_inter_preimage {α : Type u} {β : Type v} (f : α → β) (s : set α) (t : set β) :
f '' (s ∩ f ⁻¹' t) = f '' s ∩ t
source
theorem set.image_preimage_inter {α : Type u} {β : Type v} (f : α → β) (s : set α) (t : set β) :
f '' (f ⁻¹' t ∩ s) = t ∩ f '' s
source
@[simp]
theorem set.image_inter_nonempty_iff {α : Type u} {β : Type v} {f : α → β} {s : set α} {t : set β} :
(f '' s ∩ t).nonempty ↔ (s ∩ f ⁻¹' t).nonempty
source
theorem set.image_diff_preimage {α : Type u} {β : Type v} {f : α → β} {s : set α} {t : set β} :
f '' (s \ f ⁻¹' t) = f '' s \ t
source
theorem set.compl_image {α : Type u} :
set.image compl = set.preimage compl
source
theorem set.compl_image_set_of {α : Type u} {p : set α → Prop} :
compl '' {s : set α | p s} = {s : set α | p sᶜ}
source
theorem set.inter_preimage_subset {α : Type u} {β : Type v} (s : set α) (t : set β) (f : α → β) :
s ∩ f ⁻¹' t ⊆ f ⁻¹' (f '' s ∩ t)
source
theorem set.union_preimage_subset {α : Type u} {β : Type v} (s : set α) (t : set β) (f : α → β) :
s ∪ f ⁻¹' t ⊆ f ⁻¹' (f '' s ∪ t)
source
theorem set.subset_image_union {α : Type u} {β : Type v} (f : α → β) (s : set α) (t : set β) :
f '' (s ∪ f ⁻¹' t) ⊆ f '' s ∪ t
source
theorem set.preimage_subset_iff {α : Type u} {β : Type v} {A : set α} {B : set β} {f : α → β} :
f ⁻¹' B ⊆ A ↔ ∀ (a : α), f a ∈ B → a ∈ A
source
theorem set.image_eq_image {α : Type u} {β : Type v} {s t : set α} {f : α → β} (hf : function.injective f) :
f '' s = f '' t ↔ s = t
source
theorem set.image_subset_image_iff {α : Type u} {β : Type v} {s t : set α} {f : α → β} (hf : function.injective f) :
f '' s ⊆ f '' t ↔ s ⊆ t
source
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)
source
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
source
theorem set.image_factorization_eq {α : Type u} {β : Type v} {f : α → β} {s : set α} :
subtype.val ∘ set.image_factorization f s = f ∘ subtype.val
source
theorem set.surjective_onto_image {α : Type u} {β : Type v} {f : α → β} {s : set α} :
function.surjective (set.image_factorization f s)

Subsingleton #

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

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

Equations
source
theorem set.subsingleton.mono {α : Type u} {s t : set α} (ht : t.subsingleton) (hst : s ⊆ t) :
s.subsingleton
source
theorem set.subsingleton.image {α : Type u} {β : Type v} {s : set α} (hs : s.subsingleton) (f : α → β) :
(f '' s).subsingleton
source
theorem set.subsingleton.eq_singleton_of_mem {α : Type u} {s : set α} (hs : s.subsingleton) {x : α} (hx : x ∈ s) :
s = {x}
source
@[simp]
theorem set.subsingleton_empty {α : Type u} :
∅.subsingleton
source
@[simp]
theorem set.subsingleton_singleton {α : Type u} {a : α} :
{a}.subsingleton
source
theorem set.subsingleton_iff_singleton {α : Type u} {s : set α} {x : α} (hx : x ∈ s) :
s.subsingleton ↔ s = {x}
source
theorem set.subsingleton.eq_empty_or_singleton {α : Type u} {s : set α} (hs : s.subsingleton) :
s = ∅ ∨ ∃ (x : α), s = {x}
source
theorem set.subsingleton.induction_on {α : Type u} {s : set α} {p : set α → Prop} (hs : s.subsingleton) (he : p ∅) (h₁ : ∀ (x : α), p {x}) :
p s
source
theorem set.subsingleton_univ {α : Type u} [subsingleton α] :
set.univ.subsingleton
source
theorem set.subsingleton_of_univ_subsingleton {α : Type u} (h : set.univ.subsingleton) :
subsingleton α
source
@[simp]
theorem set.subsingleton_univ_iff {α : Type u} :
set.univ.subsingleton ↔ subsingleton α
source
theorem set.subsingleton_of_subsingleton {α : Type u} [subsingleton α] {s : set α} :
s.subsingleton
source
theorem set.subsingleton_is_top (α : Type u_1) [partial_order α] :
{x : α | is_top x}.subsingleton
source
theorem set.subsingleton_is_bot (α : Type u_1) [partial_order α] :
{x : α | is_bot x}.subsingleton
source
@[simp, norm_cast]
theorem set.subsingleton_coe {α : Type u} (s : set α) :
subsingleton ↥s ↔ s.subsingleton

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

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

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

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

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

source
theorem set.univ_eq_true_false  :
set.univ = {true, false}

Lemmas about range of a function. #

source
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
source
@[simp]
theorem set.mem_range {α : Type u} {ι : Sort x} {f : ι → α} {x : α} :
x ∈ set.range f ↔ ∃ (y : ι), f y = x
source
@[simp]
theorem set.mem_range_self {α : Type u} {ι : Sort x} {f : ι → α} (i : ι) :
f i ∈ set.range f
source
theorem set.forall_range_iff {α : Type u} {ι : Sort x} {f : ι → α} {p : α → Prop} :
(∀ (a : α), a ∈ set.range f → p a) ↔ ∀ (i : ι), p (f i)
source
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, _⟩
source
theorem set.exists_range_iff {α : Type u} {ι : Sort x} {f : ι → α} {p : α → Prop} :
(∃ (a : α) (H : a ∈ set.range f), p a) ↔ ∃ (i : ι), p (f i)
source
theorem set.exists_range_iff' {α : Type u} {ι : Sort x} {f : ι → α} {p : α → Prop} :
(∃ (a : α), a ∈ set.range f ∧ p a) ↔ ∃ (i : ι), p (f i)
source
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, _⟩
source
theorem set.range_iff_surjective {α : Type u} {ι : Sort x} {f : ι → α} :
set.range f = set.univ ↔ function.surjective f
source
theorem function.surjective.range_eq {α : Type u} {ι : Sort x} {f : ι → α} :
function.surjective f → set.range f = set.univ

Alias of range_iff_surjective.

source
@[simp]
theorem set.range_id {α : Type u} :
set.range id = set.univ
source
@[simp]
theorem set.range_id' {α : Type u} :
set.range (λ (x : α), x) = set.univ
source
@[simp]
theorem prod.range_fst {α : Type u} {β : Type v} [nonempty β] :
set.range prod.fst = set.univ
source
@[simp]
theorem prod.range_snd {α : Type u} {β : Type v} [nonempty α] :
set.range prod.snd = set.univ
source
@[simp]
theorem set.range_eval {ι : Type u_1} {α : ι → Type u_2} [∀ (i : ι), nonempty (α i)] (i : ι) :
set.range (function.eval i) = set.univ
source
theorem set.is_compl_range_inl_range_inr {α : Type u} {β : Type v} :
is_compl (set.range sum.inl) (set.range sum.inr)
source
@[simp]
theorem set.range_inl_union_range_inr {α : Type u} {β : Type v} :
set.range sum.inl ∪ set.range sum.inr = set.univ
source
@[simp]
theorem set.range_inl_inter_range_inr {α : Type u} {β : Type v} :
set.range sum.inl ∩ set.range sum.inr = ∅
source
@[simp]
theorem set.range_inr_union_range_inl {α : Type u} {β : Type v} :
set.range sum.inr ∪ set.range sum.inl = set.univ
source
@[simp]
theorem set.range_inr_inter_range_inl {α : Type u} {β : Type v} :
set.range sum.inr ∩ set.range sum.inl = ∅
source
@[simp]
theorem set.preimage_inl_range_inr {α : Type u} {β : Type v} :
sum.inl ⁻¹' set.range sum.inr = ∅
source
@[simp]
theorem set.preimage_inr_range_inl {α : Type u} {β : Type v} :
sum.inr ⁻¹' set.range sum.inl = ∅
source
@[simp]
theorem set.range_quot_mk {α : Type u} (r : α → α → Prop) :
set.range (quot.mk r) = set.univ
source
@[simp]
theorem set.image_univ {α : Type u} {β : Type v} {f : α → β} :
f '' set.univ = set.range f
source
theorem set.image_subset_range {α : Type u} {β : Type v} (f : α → β) (s : set α) :
f '' s ⊆ set.range f
source
theorem set.mem_range_of_mem_image {α : Type u} {β : Type v} (f : α → β) (s : set α) {x : β} (h : x ∈ f '' s) :
x ∈ set.range f
source
theorem set.nonempty.preimage' {α : Type u} {β : Type v} {s : set β} (hs : s.nonempty) {f : α → β} (hf : s ⊆ set.range f) :
(f ⁻¹' s).nonempty
source
theorem set.range_comp {α : Type u} {β : Type v} {ι : Sort x} (g : α → β) (f : ι → α) :
set.range (g ∘ f) = g '' set.range f
source
theorem set.range_subset_iff {α : Type u} {ι : Sort x} {s : set α} {f : ι → α} :
set.range f ⊆ s ↔ ∀ (y : ι), f y ∈ s
source
theorem set.range_comp_subset_range {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : β → γ) :
set.range (g ∘ f) ⊆ set.range g
source
theorem set.range_nonempty_iff_nonempty {α : Type u} {ι : Sort x} {f : ι → α} :
(set.range f).nonempty ↔ nonempty ι
source
theorem set.range_nonempty {α : Type u} {ι : Sort x} [h : nonempty ι] (f : ι → α) :
(set.range f).nonempty
source
@[simp]
theorem set.range_eq_empty_iff {α : Type u} {ι : Sort x} {f : ι → α} :
set.range f = ∅ ↔ is_empty ι
source
theorem set.range_eq_empty {α : Type u} {ι : Sort x} [is_empty ι] (f : ι → α) :
set.range f = ∅
source
@[protected, instance]
def set.range.nonempty {α : Type u} {ι : Sort x} [nonempty ι] (f : ι → α) :
nonempty ↥(set.range f)
source
@[simp]
theorem set.image_union_image_compl_eq_range {α : Type u} {β : Type v} {s : set α} (f : α → β) :
f '' s ∪ f '' sᶜ = set.range f
source
theorem set.image_preimage_eq_inter_range {α : Type u} {β : Type v} {f : α → β} {t : set β} :
f '' (f ⁻¹' t) = t ∩ set.range f
source
theorem set.image_preimage_eq_of_subset {α : Type u} {β : Type v} {f : α → β} {s : set β} (hs : s ⊆ set.range f) :
f '' (f ⁻¹' s) = s
source
@[protected, instance]
def set.set.can_lift {α : Type u} {β : Type v} [can_lift α β] :
can_lift (set α) (set β)
Equations
source
theorem set.image_preimage_eq_iff {α : Type u} {β : Type v} {f : α → β} {s : set β} :
f '' (f ⁻¹' s) = s ↔ s ⊆ set.range f
source
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
source
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
source
@[simp]
theorem set.preimage_inter_range {α : Type u} {β : Type v} {f : α → β} {s : set β} :
f ⁻¹' (s ∩ set.range f) = f ⁻¹' s
source
@[simp]
theorem set.preimage_range_inter {α : Type u} {β : Type v} {f : α → β} {s : set β} :
f ⁻¹' (set.range f ∩ s) = f ⁻¹' s
source
theorem set.preimage_image_preimage {α : Type u} {β : Type v} {f : α → β} {s : set β} :
f ⁻¹' (f '' (f ⁻¹' s)) = f ⁻¹' s
source
@[simp]
theorem set.quot_mk_range_eq {α : Type u} [setoid α] :
set.range (λ (x : α), ⟦x⟧) = set.univ
source
theorem set.range_const_subset {α : Type u} {ι : Sort x} {c : α} :
set.range (λ (x : ι), c) ⊆ {c}
source
@[simp]
theorem set.range_const {α : Type u} {ι : Sort x} [nonempty ι] {c : α} :
set.range (λ (x : ι), c) = {c}
source
theorem set.image_swap_eq_preimage_swap {α : Type u} {β : Type v} :
set.image prod.swap = set.preimage prod.swap
source
theorem set.preimage_singleton_nonempty {α : Type u} {β : Type v} {f : α → β} {y : β} :
(f ⁻¹' {y}).nonempty ↔ y ∈ set.range f
source
theorem set.preimage_singleton_eq_empty {α : Type u} {β : Type v} {f : α → β} {y : β} :
f ⁻¹' {y} = ∅ ↔ y ∉ set.range f
source
theorem set.range_subset_singleton {α : Type u} {ι : Sort x} {f : ι → α} {x : α} :
set.range f ⊆ {x} ↔ f = function.const ι x
source
theorem set.image_compl_preimage {α : Type u} {β : Type v} {f : α → β} {s : set β} :
f '' (f ⁻¹' s)ᶜ = set.range f \ s
source
@[simp]
theorem set.range_sigma_mk {α : Type u} {β : α → Type u_1} (a : α) :
set.range (sigma.mk a) = sigma.fst ⁻¹' {a}
source
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
source
theorem set.range_factorization_eq {β : Type v} {ι : Sort x} {f : ι → β} :
subtype.val ∘ set.range_factorization f = f
source
@[simp]
theorem set.range_factorization_coe {β : Type v} {ι : Sort x} (f : ι → β) (a : ι) :
↑(set.range_factorization f a) = f a
source
@[simp]
theorem set.coe_comp_range_factorization {β : Type v} {ι : Sort x} (f : ι → β) :
coe ∘ set.range_factorization f = f
source
theorem set.surjective_onto_range {α : Type u} {ι : Sort x} {f : ι → α} :
function.surjective (set.range_factorization f)
source
theorem set.image_eq_range {α : Type u} {β : Type v} (f : α → β) (s : set α) :
f '' s = set.range (λ (x : ↥s), f ↑x)
source
@[simp]
theorem set.sum.elim_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → γ) (g : β → γ) :
set.range (sum.elim f g) = set.range f ∪ set.range g
source
theorem set.range_ite_subset' {α : Type u} {β : Type v} {p : Prop} [decidable p] {f g : α → β} :
set.range (ite p f g) ⊆ set.range f ∪ set.range g
source
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
source
@[simp]
theorem set.preimage_range {α : Type u} {β : Type v} (f : α → β) :
f ⁻¹' set.range f = set.univ
source
theorem set.range_unique {α : Type u} {ι : Sort x} {f : ι → α} [h : unique ι] :
set.range f = {f (default ι)}

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

source
theorem set.range_diff_image_subset {α : Type u} {β : Type v} (f : α → β) (s : set α) :
set.range f \ f '' s ⊆ f '' sᶜ
source
theorem set.range_diff_image {α : Type u} {β : Type v} {f : α → β} (H : function.injective f) (s : set α) :
set.range f \ f '' s = f '' sᶜ
source
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
source
theorem set.apply_range_splitting {α : Type u} {β : Type v} (f : α → β) (x : ↥(set.range f)) :
f (set.range_splitting f x) = ↑x
source
@[simp]
theorem set.comp_range_splitting {α : Type u} {β : Type v} (f : α → β) :
f ∘ set.range_splitting f = coe
source
theorem set.left_inverse_range_splitting {α : Type u} {β : Type v} (f : α → β) :
function.left_inverse (set.range_factorization f) (set.range_splitting f)
source
theorem set.range_splitting_injective {α : Type u} {β : Type v} (f : α → β) :
function.injective (set.range_splitting f)
source
theorem set.right_inverse_range_splitting {α : Type u} {β : Type v} {f : α → β} (h : function.injective f) :
function.right_inverse (set.range_factorization f) (set.range_splitting f)
source
theorem set.preimage_range_splitting {α : Type u} {β : Type v} {f : α → β} (hf : function.injective f) :
set.preimage (set.range_splitting f) = set.image (set.range_factorization f)
source
theorem set.is_compl_range_some_none (α : Type u_1) :
is_compl (set.range some) {none}
source
@[simp]
theorem set.compl_range_some (α : Type u_1) :
(set.range some)ᶜ = {none}
source
@[simp]
theorem set.range_some_inter_none (α : Type u_1) :
set.range some ∩ {none} = ∅
source
@[simp]
theorem set.range_some_union_none (α : Type u_1) :
set.range some ∪ {none} = set.univ
source
theorem function.surjective.preimage_injective {α : Type u_2} {β : Type u_3} {f : α → β} (hf : function.surjective f) :
function.injective (set.preimage f)
source
theorem function.injective.preimage_image {α : Type u_2} {β : Type u_3} {f : α → β} (hf : function.injective f) (s : set α) :
f ⁻¹' (f '' s) = s
source
theorem function.injective.preimage_surjective {α : Type u_2} {β : Type u_3} {f : α → β} (hf : function.injective f) :
function.surjective (set.preimage f)
source
theorem function.injective.subsingleton_image_iff {α : Type u_2} {β : Type u_3} {f : α → β} (hf : function.injective f) {s : set α} :
(f '' s).subsingleton ↔ s.subsingleton
source
theorem function.surjective.image_preimage {α : Type u_2} {β : Type u_3} {f : α → β} (hf : function.surjective f) (s : set β) :
f '' (f ⁻¹' s) = s
source
theorem function.surjective.image_surjective {α : Type u_2} {β : Type u_3} {f : α → β} (hf : function.surjective f) :
function.surjective (set.image f)
source
theorem function.surjective.nonempty_preimage {α : Type u_2} {β : Type u_3} {f : α → β} (hf : function.surjective f) {s : set β} :
(f ⁻¹' s).nonempty ↔ s.nonempty
source
theorem function.injective.image_injective {α : Type u_2} {β : Type u_3} {f : α → β} (hf : function.injective f) :
function.injective (set.image f)
source
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
source
theorem function.surjective.range_comp {ι : Sort u_1} {α : Type u_2} {ι' : Sort u_3} {f : ι → ι'} (hf : function.surjective f) (g : ι' → α) :
set.range (g ∘ f) = set.range g
source
theorem function.injective.nonempty_apply_iff {α : Type u_2} {β : Type u_3} {f : set α → set β} (hf : function.injective f) (h2 : f ∅ = ∅) {s : set α} :
(f s).nonempty ↔ s.nonempty
source
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
source
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
source
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)ᶜ
source
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
source
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
source
theorem option.injective_iff {α : Type u_1} {β : Type u_2} {f : option α → β} :
function.injective f ↔ function.injective (f ∘ some) ∧ f none ∉ set.range (f ∘ some)

Image and preimage on subtypes #

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

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.

source
@[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).

source
@[simp]
theorem subtype.coe_preimage_self {α : Type u_1} (s : set α) :
coe ⁻¹' s = set.univ
source
theorem subtype.range_val_subtype {α : Type u_1} {p : α → Prop} :
set.range subtype.val = {x : α | p x}
source
theorem subtype.coe_image_subset {α : Type u_1} (s : set α) (t : set ↥s) :
coe '' t ⊆ s
source
theorem subtype.coe_image_univ {α : Type u_1} (s : set α) :
coe '' set.univ = s
source
@[simp]
theorem subtype.image_preimage_coe {α : Type u_1} (s t : set α) :
coe '' (coe ⁻¹' t) = t ∩ s
source
theorem subtype.image_preimage_val {α : Type u_1} (s t : set α) :
subtype.val '' (subtype.val ⁻¹' t) = t ∩ s
source
theorem subtype.preimage_coe_eq_preimage_coe_iff {α : Type u_1} {s t u : set α} :
coe ⁻¹' t = coe ⁻¹' u ↔ t ∩ s = u ∩ s
source
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
source
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
source
theorem subtype.preimage_coe_nonempty {α : Type u_1} {s t : set α} :
(coe ⁻¹' t).nonempty ↔ (s ∩ t).nonempty
source
theorem subtype.preimage_coe_eq_empty {α : Type u_1} {s t : set α} :
coe ⁻¹' t = ∅ ↔ s ∩ t = ∅
source
@[simp]
theorem subtype.preimage_coe_compl {α : Type u_1} (s : set α) :
coe ⁻¹' sᶜ = ∅
source
@[simp]
theorem subtype.preimage_coe_compl' {α : Type u_1} (s : set α) :
coe ⁻¹' s = ∅

Lemmas about inclusion, the injection of subtypes induced by ⊆ #

source
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
source
@[simp]
theorem set.inclusion_self {α : Type u_1} {s : set α} (x : ↥s) :
set.inclusion set.subset.rfl x = x
source
@[simp]
theorem set.inclusion_right {α : Type u_1} {s t : set α} (h : s ⊆ t) (x : ↥t) (m : ↑x ∈ s) :
set.inclusion h ⟨↑x, m⟩ = x
source
@[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
source
@[simp]
theorem set.coe_inclusion {α : Type u_1} {s t : set α} (h : s ⊆ t) (x : ↥s) :
↑(set.inclusion h x) = ↑x
source
theorem set.inclusion_injective {α : Type u_1} {s t : set α} (h : s ⊆ t) :
function.injective (set.inclusion h)
source
@[simp]
theorem set.range_inclusion {α : Type u_1} {s t : set α} (h : s ⊆ t) :
set.range (set.inclusion h) = {x : ↥t | ↑x ∈ s}
source
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 #

source
@[simp]
theorem set.preimage_injective {α : Type u} {β : Type v} {f : α → β} :
function.injective (set.preimage f) ↔ function.surjective f
source
@[simp]
theorem set.preimage_surjective {α : Type u} {β : Type v} {f : α → β} :
function.surjective (set.preimage f) ↔ function.injective f
source
@[simp]
theorem set.image_surjective {α : Type u} {β : Type v} {f : α → β} :
function.surjective (set.image f) ↔ function.surjective f
source
@[simp]
theorem set.image_injective {α : Type u} {β : Type v} {f : α → β} :
function.injective (set.image f) ↔ function.injective f
source
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
source
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

Lemmas about images of binary and ternary functions #

source
def set.image2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (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
source
theorem set.mem_image2_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : set α} {t : set β} {c : γ} :
c ∈ set.image2 f s t = ∃ (a : α) (b : β), a ∈ s ∧ b ∈ t ∧ f a b = c
source
@[simp]
theorem set.mem_image2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : set α} {t : set β} {c : γ} :
c ∈ set.image2 f s t ↔ ∃ (a : α) (b : β), a ∈ s ∧ b ∈ t ∧ f a b = c
source
theorem set.mem_image2_of_mem {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : set α} {t : set β} {a : α} {b : β} (h1 : a ∈ s) (h2 : b ∈ t) :
f a b ∈ set.image2 f s t
source
theorem set.mem_image2_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : set α} {t : set β} {a : α} {b : β} (hf : function.injective2 f) :
f a b ∈ set.image2 f s t ↔ a ∈ s ∧ b ∈ t
source
theorem set.image2_subset {α : Type u_1} {β : Type u_2} {γ : Type u_3} {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 ⊆.

source
theorem set.image2_subset_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : set α} {t t' : set β} (ht : t ⊆ t') :
set.image2 f s t ⊆ set.image2 f s t'
source
theorem set.image2_subset_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s s' : set α} {t : set β} (hs : s ⊆ s') :
set.image2 f s t ⊆ set.image2 f s' t
source
theorem set.forall_image2_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : set α} {t : set β} {p : γ → Prop} :
(∀ (z : γ), z ∈ set.image2 f s t → p z) ↔ ∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → p (f x y)
source
@[simp]
theorem set.image2_subset_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : set α} {t : set β} {u : set γ} :
set.image2 f s t ⊆ u ↔ ∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u
source
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
source
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'
source
@[simp]
theorem set.image2_empty_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {t : set β} :
set.image2 f ∅ t = ∅
source
@[simp]
theorem set.image2_empty_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : set α} :
set.image2 f s ∅ = ∅
source
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
source
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'
source
@[simp]
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
source
@[simp]
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
source
theorem set.image2_singleton {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {a : α} {b : β} :
set.image2 f {a} {b} = {f a b}
source
theorem set.image2_congr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f f' : α → β → γ} {s : set α} {t : set β} (h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → f a b = f' a b) :
set.image2 f s t = set.image2 f' s t
source
theorem set.image2_congr' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {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

source
def set.image3 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (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
source
@[simp]
theorem set.mem_image3 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {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
source
theorem set.image3_congr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {g g' : α → β → γ → δ} {s : set α} {t : set β} {u : set γ} (h : ∀ (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
source
theorem set.image3_congr' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {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

source
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
source
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
source
theorem set.image2_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {s : set α} {t : set β} {u : set γ} {ε' : Type u_6} {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)
source
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
source
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
source
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
source
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
source
@[simp]
theorem set.image2_left {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} (h : t.nonempty) :
set.image2 (λ (x : α) (y : β), x) s t = s
source
@[simp]
theorem set.image2_right {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} (h : s.nonempty) :
set.image2 (λ (x : α) (y : β), y) s t = t
source
theorem set.nonempty.image2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : set α} {t : set β} (hs : s.nonempty) (ht : t.nonempty) :
(set.image2 f s t).nonempty
source
theorem subsingleton.eq_univ_of_nonempty {α : Type u_1} [subsingleton α] {s : set α} :
s.nonempty → s = set.univ
source
theorem subsingleton.set_cases {α : Type u_1} [subsingleton α] {p : set α → Prop} (h0 : p ∅) (h1 : p set.univ) (s : set α) :
p s
source
theorem subsingleton.mem_iff_nonempty {α : Type u_1} [subsingleton α] {s : set α} {x : α} :
x ∈ s ↔ s.nonempty