Basic properties of sets #
Sets in Lean are homogeneous; all their elements have the same type. Sets whose elements
have type X are thus defined as set X := X → Prop. Note that this function need not
be decidable. The definition is in the core library.
This file provides some basic definitions related to sets and functions not present in the core library, as well as extra lemmas for functions in the core library (empty set, univ, union, intersection, insert, singleton, set-theoretic difference, complement, and powerset).
Note that a set is a term, not a type. There is a coercion from set α to Type* sending
s to the corresponding subtype ↥s.
See also the file set_theory/zfc.lean, which contains an encoding of ZFC set theory in Lean.
Main definitions #
Notation used here:
Definitions in the file:
-
nonempty s : Prop: the predicates ≠ ∅. Note that this is the preferred way to express the fact thatshas an element (see the Implementation Notes). -
preimage f t : set α: the preimage f⁻¹(t) (writtenf ⁻¹' tin Lean) of a subset of β. -
subsingleton s : Prop: the predicate saying thatshas at most one element. -
range f : set β: the image ofunivunderf. Also works for{p : Prop} (f : p → α)(unlikeimage) -
inclusion s₁ s₂ : ↥s₁ → ↥s₂: the map↥s₁ → ↥s₂induced by an inclusions₁ ⊆ s₂.
Notation #
-
f ⁻¹' tforpreimage f t -
f '' sforimage f s -
sᶜfor the complement ofs
Implementation notes #
-
s.nonemptyis to be preferred tos ≠ ∅or∃ x, x ∈ s. It has the advantage that thes.nonemptydot notation can be used. -
For
s : set α, do not usesubtype s. Instead use↥sor(s : Type*)ors.
Tags #
set, sets, subset, subsets, image, preimage, pre-image, range, union, intersection, insert, singleton, complement, powerset
Set coercion to a type #
@[protected, instance]
Equations
@[protected, instance]
Equations
- set.boolean_algebra = {sup := has_union.union set.has_union, le := has_le.le set.has_le, lt := has_lt.lt set.has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inter.inter set.has_inter, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, sdiff := sdiff set.has_sdiff, bot := ∅, sup_inf_sdiff := _, inf_inf_sdiff := _, compl := set.compl α, top := set.univ α, inf_compl_le_bot := _, top_le_sup_compl := _, le_top := _, bot_le := _, sdiff_eq := _}
set.lt_eq_ssubset is defined further down
@[protected, instance]
Coercion from a set to the corresponding subtype.
@[protected, instance]
def
set.pi_set_coe.can_lift
(ι : Type u)
(α : ι → Type v)
[ne : ∀ (i : ι), nonempty (α i)]
(s : set ι) :
Equations
- set.pi_set_coe.can_lift ι α s = {coe := λ (f : Π (i : ι), α i) (i : ↥s), f ↑i, cond := can_lift.cond (Π (i : ι), α i) (pi_subtype.can_lift ι α s), prf := _}
@[protected, instance]
Equations
- set.pi_set_coe.can_lift' ι α s = set.pi_set_coe.can_lift ι (λ (_x : ι), α) s
@[protected, instance]
Equations
- set.set_coe.can_lift s = {coe := coe coe_to_lift, cond := λ (a : α), a ∈ s, prf := _}
@[protected, instance]
Equations
- set.inhabited = {default := ∅}
@[simp]
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.
@[simp]
@[simp]
Subset and strict subset relations #
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Definition of strict subsets s ⊂ t and basic properties. #
Non-empty sets #
@[protected]
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.
@[protected]
Extract a witness from s.nonempty. This function might be used instead of case analysis
on the argument. Note that it makes a proof depend on the classical.choice axiom.
Equations
- h.some = classical.some h
Lemmas about the empty set #
There is exactly one set of a type that is empty.
Equations
- set.unique_empty = {to_inhabited := {default := ∅}, uniq := _}
Universal set. #
In Lean @univ α (or univ : set α) is the set that contains all elements of type α.
Mathematically it is the same as α but it has a different type.
Lemmas about union #
@[protected, instance]
@[protected, instance]
Lemmas about intersection #
@[protected, instance]
@[protected, instance]
Distributivity laws #
Lemmas about insert #
insert α s is the set {α} ∪ s.
Lemmas about singletons #
@[protected, instance]
Equations
- set.unique_singleton a = {to_inhabited := {default := ⟨a, _⟩}, uniq := _}
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]
Lemmas about complement #
Lemmas about set difference #
Powerset #
If-then-else for sets #
Inverse image #
@[simp]
Image of a set under a function #
theorem
function.injective.mem_set_image
{α : Type u}
{β : Type v}
{f : α → β}
(hf : function.injective f)
{s : set α}
{a : α} :
Image is monotone with respect to ⊆. See set.monotone_image for the statement in
terms of ≤.
theorem
set.image_inter
{α : Type u}
{β : Type v}
{f : α → β}
{s t : set α}
(H : function.injective f) :
theorem
set.image_univ_of_surjective
{β : Type v}
{ι : Type u_1}
{f : ι → β}
(H : function.surjective f) :
@[simp]
@[simp]
A variant of image_id
theorem
set.image_subset_preimage_of_inverse
{α : Type u}
{β : Type v}
{f : α → β}
{g : β → α}
(I : function.left_inverse g f)
(s : set α) :
theorem
set.preimage_subset_image_of_inverse
{α : Type u}
{β : Type v}
{f : α → β}
{g : β → α}
(I : function.left_inverse g f)
(s : set β) :
theorem
set.image_eq_preimage_of_inverse
{α : Type u}
{β : Type v}
{f : α → β}
{g : β → α}
(h₁ : function.left_inverse g f)
(h₂ : function.right_inverse g f) :
set.image f = set.preimage g
theorem
set.mem_image_iff_of_inverse
{α : Type u}
{β : Type v}
{f : α → β}
{g : β → α}
{b : β}
{s : set α}
(h₁ : function.left_inverse g f)
(h₂ : function.right_inverse g f) :
theorem
set.image_compl_subset
{α : Type u}
{β : Type v}
{f : α → β}
{s : set α}
(H : function.injective f) :
theorem
set.subset_image_compl
{α : Type u}
{β : Type v}
{f : α → β}
{s : set α}
(H : function.surjective f) :
theorem
set.image_compl_eq
{α : Type u}
{β : Type v}
{f : α → β}
{s : set α}
(H : function.bijective f) :
theorem
set.image_diff
{α : Type u}
{β : Type v}
{f : α → β}
(hf : function.injective f)
(s t : set α) :
theorem
set.nonempty.preimage
{α : Type u}
{β : Type v}
{s : set β}
(hs : s.nonempty)
{f : α → β}
(hf : function.surjective f) :
theorem
set.preimage_image_eq
{α : Type u}
{β : Type v}
{f : α → β}
(s : set α)
(h : function.injective f) :
theorem
set.image_preimage_eq
{α : Type u}
{β : Type v}
{f : α → β}
(s : set β)
(h : function.surjective f) :
theorem
set.preimage_eq_preimage
{α : Type u}
{β : Type v}
{s t : set α}
{f : β → α}
(hf : function.surjective f) :
theorem
set.image_eq_image
{α : Type u}
{β : Type v}
{s t : set α}
{f : α → β}
(hf : function.injective f) :
theorem
set.image_subset_image_iff
{α : Type u}
{β : Type v}
{s t : set α}
{f : α → β}
(hf : function.injective f) :
theorem
set.prod_quotient_preimage_eq_image
{α : Type u}
{β : Type v}
[s : setoid α]
(g : quotient s → β)
{h : α → β}
(Hh : h = g ∘ quotient.mk)
(r : set (β × β)) :
If the only elements outside s are those left fixed by σ, then mapping by σ has no effect.
Subsingleton #
@[protected]
A set s is a subsingleton, if it has at most one element.
Equations
- s.subsingleton = ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y
theorem
set.subsingleton.image
{α : Type u}
{β : Type v}
{s : set α}
(hs : s.subsingleton)
(f : α → β) :
(f '' s).subsingleton
theorem
set.subsingleton.eq_singleton_of_mem
{α : Type u}
{s : set α}
(hs : s.subsingleton)
{x : α}
(hx : x ∈ s) :
s = {x}
theorem
set.subsingleton_of_forall_eq
{α : Type u}
{s : set α}
(a : α)
(h : ∀ (b : α), b ∈ s → b = a) :
theorem
set.subsingleton_iff_singleton
{α : Type u}
{s : set α}
{x : α}
(hx : x ∈ s) :
s.subsingleton ↔ 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
@[simp]
theorem
set.exists_eq_singleton_iff_nonempty_subsingleton
{α : Type u}
{s : set α} :
(∃ (a : α), s = {a}) ↔ s.nonempty ∧ s.subsingleton
@[simp, norm_cast]
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) :
(f ⁻¹' s).subsingleton
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. #
@[simp]
Alias of range_iff_surjective.
@[simp]
@[simp]
@[protected, instance]
Equations
- set.set.can_lift = {coe := λ (s : set β), can_lift.coe '' s, cond := λ (s : set α), ∀ (x : α), x ∈ s → can_lift.cond β x, prf := _}
@[simp]
theorem
set.range_subset_singleton
{α : Type u}
{ι : Sort x}
{f : ι → α}
{x : α} :
set.range f ⊆ {x} ↔ f = function.const ι x
Any map f : ι → β factors through a map range_factorization f : ι → range f.
Equations
- set.range_factorization f = λ (i : ι), ⟨f i, _⟩
@[simp]
theorem
set.range_factorization_coe
{β : Type v}
{ι : Sort x}
(f : ι → β)
(a : ι) :
↑(set.range_factorization f a) = f a
@[simp]
theorem
set.coe_comp_range_factorization
{β : Type v}
{ι : Sort x}
(f : ι → β) :
coe ∘ set.range_factorization f = f
theorem
set.range_ite_subset
{α : Type u}
{β : Type v}
{p : α → Prop}
[decidable_pred p]
{f g : α → β} :
theorem
set.range_diff_image
{α : Type u}
{β : Type v}
{f : α → β}
(H : function.injective f)
(s : set α) :
We can use the axiom of choice to pick a preimage for every element of range f.
Equations
- set.range_splitting f = λ (x : ↥(set.range f)), Exists.some _
theorem
set.apply_range_splitting
{α : Type u}
{β : Type v}
(f : α → β)
(x : ↥(set.range f)) :
f (set.range_splitting f x) = ↑x
@[simp]
theorem
set.comp_range_splitting
{α : Type u}
{β : Type v}
(f : α → β) :
f ∘ set.range_splitting f = coe
theorem
set.right_inverse_range_splitting
{α : Type u}
{β : Type v}
{f : α → β}
(h : function.injective f) :
theorem
set.preimage_range_splitting
{α : Type u}
{β : Type v}
{f : α → β}
(hf : function.injective f) :
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 α) :
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 α} :
(f '' s).subsingleton ↔ s.subsingleton
theorem
function.surjective.image_preimage
{α : Type u_2}
{β : Type u_3}
{f : α → β}
(hf : function.surjective f)
(s : set β) :
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) :
theorem
function.surjective.range_comp
{ι : Sort u_1}
{α : Type u_2}
{ι' : Sort u_3}
{f : ι → ι'}
(hf : function.surjective f)
(g : ι' → α) :
theorem
function.injective.mem_range_iff_exists_unique
{α : Type u_2}
{β : Type u_3}
{f : α → β}
(hf : function.injective f)
{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.left_inverse.image_image
{α : Type u_2}
{β : Type u_3}
{f : α → β}
{g : β → α}
(h : function.left_inverse g f)
(s : set α) :
theorem
function.left_inverse.preimage_preimage
{α : Type u_2}
{β : Type u_3}
{f : α → β}
{g : β → α}
(h : function.left_inverse g f)
(s : set α) :
Image and preimage on subtypes #
A variant of range_coe. Try to use range_coe if possible.
This version is useful when defining a new type that is defined as the subtype of something.
In that case, the coercion doesn't fire anymore.
theorem
subtype.range_val_subtype
{α : Type u_1}
{p : α → Prop} :
set.range subtype.val = {x : α | p x}
theorem
subtype.image_preimage_val
{α : Type u_1}
(s t : set α) :
subtype.val '' (subtype.val ⁻¹' t) = t ∩ s
theorem
subtype.preimage_val_eq_preimage_val_iff
{α : Type u_1}
(s t u : set α) :
subtype.val ⁻¹' t = subtype.val ⁻¹' u ↔ t ∩ s = u ∩ s
Lemmas about inclusion, the injection of subtypes induced by ⊆ #
@[simp]
@[simp]
theorem
set.inclusion_inclusion
{α : Type u_1}
{s t u : set α}
(hst : s ⊆ t)
(htu : t ⊆ u)
(x : ↥s) :
set.inclusion htu (set.inclusion hst x) = set.inclusion _ x
@[simp]
theorem
set.coe_inclusion
{α : Type u_1}
{s t : set α}
(h : s ⊆ t)
(x : ↥s) :
↑(set.inclusion h x) = ↑x
@[simp]
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]
@[simp]
@[simp]
@[simp]
theorem
set.preimage_eq_iff_eq_image
{α : Type u}
{β : Type v}
{f : α → β}
(hf : function.bijective f)
{s : set β}
{t : set α} :
theorem
set.eq_preimage_iff_image_eq
{α : Type u}
{β : Type v}
{f : α → β}
(hf : function.bijective f)
{s : set α}
{t : set β} :
Images of binary and ternary functions #
This section is very similar to order.filter.n_ary. Please keep them in sync.
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) :
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') :
set.image2 f s t ⊆ set.image2 f s t'
theorem
set.image2_subset_right
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s s' : set α}
{t : set β}
(hs : s ⊆ s') :
set.image2 f s t ⊆ set.image2 f s' t
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 t → p z) ↔ ∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → p (f x y)
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 β} :
set.image2 f ∅ t = ∅
@[simp]
theorem
set.image2_empty_right
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s : set α} :
set.image2 f s ∅ = ∅
theorem
set.nonempty.image2
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s : set α}
{t : set β} :
s.nonempty → t.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 β} :
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 ∈ t → f a b = f' a b) :
set.image2 f s t = set.image2 f' s t
theorem
set.image2_congr'
{α : Type u_1}
{β : Type u_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 α × β × γ → δ.
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 ∈ u → g a b c = g' a b c) :
set.image3 g s t u = set.image3 g' s t u
theorem
set.image3_congr'
{α : Type u_1}
{β : Type u_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.set_cases
{α : Type u_1}
[subsingleton α]
{p : set α → Prop}
(h0 : p ∅)
(h1 : p set.univ)
(s : set α) :
p s
Decidability instances for sets #
@[protected, instance]
def
set.decidable_sdiff
{α : Type u}
(s t : set α)
(a : α)
[decidable (a ∈ s)]
[decidable (a ∈ t)] :
Equations
- s.decidable_sdiff t a = and.decidable
@[protected, instance]
def
set.decidable_inter
{α : Type u}
(s t : set α)
(a : α)
[decidable (a ∈ s)]
[decidable (a ∈ t)] :
Equations
- s.decidable_inter t a = and.decidable
@[protected, instance]
def
set.decidable_union
{α : Type u}
(s t : set α)
(a : α)
[decidable (a ∈ s)]
[decidable (a ∈ t)] :
Equations
- s.decidable_union t a = or.decidable
@[protected, instance]
Equations
@[protected, instance]
Equations
- set.decidable_emptyset = λ (_x : α), is_false _
@[protected, instance]
Equations
- set.decidable_univ = λ (_x : α), is_true _
@[protected, instance]
Equations
- set.decidable_set_of a p = _inst_1