# Interactions between embeddings and sets. #

@[simp]
theorem Equiv.asEmbedding_range {α : Sort u_1} {β : Type u_2} {p : βProp} (e : α ) :
Set.range e.asEmbedding =
@[simp]
theorem Function.Embedding.coeWithTop_apply {α : Type u_1} :
∀ (a : α), Function.Embedding.coeWithTop a = a

Embedding into WithTop α.

Equations
• Function.Embedding.coeWithTop = let __src := Function.Embedding.some; { toFun := WithTop.some, inj' := }
Instances For
@[simp]
theorem Function.Embedding.optionElim_apply {α : Type u_1} {β : Type u_2} (f : α β) (x : β) (h : x) :
∀ (a : ), (f.optionElim x h) a = Option.elim' x (⇑f) a
def Function.Embedding.optionElim {α : Type u_1} {β : Type u_2} (f : α β) (x : β) (h : x) :
β

Given an embedding f : α ↪ β and a point outside of Set.range f, construct an embedding Option α ↪ β.

Equations
Instances For
@[simp]
theorem Function.Embedding.optionEmbeddingEquiv_apply_snd_coe (α : Type u_1) (β : Type u_2) (f : β) :
.snd = f none
@[simp]
theorem Function.Embedding.optionEmbeddingEquiv_apply_fst (α : Type u_1) (β : Type u_2) (f : β) :
.fst = Function.Embedding.coeWithTop.trans f
@[simp]
theorem Function.Embedding.optionEmbeddingEquiv_symm_apply (α : Type u_1) (β : Type u_2) (f : (f : α β) × (Set.range f)) :
.symm f = f.fst.optionElim f.snd
def Function.Embedding.optionEmbeddingEquiv (α : Type u_1) (β : Type u_2) :
( β) (f : α β) × (Set.range f)

Equivalence between embeddings of Option α and a sigma type over the embeddings of α.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Function.Embedding.codRestrict {α : Sort u_1} {β : Type u_2} (p : Set β) (f : α β) (H : ∀ (a : α), f a p) :
α p

Restrict the codomain of an embedding.

Equations
• = { toFun := fun (a : α) => f a, , inj' := }
Instances For
@[simp]
theorem Function.Embedding.codRestrict_apply {α : Sort u_1} {β : Type u_2} (p : Set β) (f : α β) (H : ∀ (a : α), f a p) (a : α) :
a = f a,
@[simp]
theorem Function.Embedding.image_apply {α : Type u_1} {β : Type u_2} (f : α β) (s : Set α) :
f.image s = f '' s
def Function.Embedding.image {α : Type u_1} {β : Type u_2} (f : α β) :
Set α Set β

Set.image as an embedding Set α ↪ Set β.

Equations
• f.image = { toFun := , inj' := }
Instances For
@[simp]
theorem Set.embeddingOfSubset_apply_coe {α : Type u_1} (s : Set α) (t : Set α) (h : s t) (x : s) :
((s.embeddingOfSubset t h) x) = x
def Set.embeddingOfSubset {α : Type u_1} (s : Set α) (t : Set α) (h : s t) :
s t

The injection map is an embedding between subsets.

Equations
• s.embeddingOfSubset t h = { toFun := fun (x : s) => x, , inj' := }
Instances For
@[simp]
theorem subtypeOrEquiv_apply {α : Type u_1} (p : αProp) (q : αProp) [] (h : Disjoint p q) (a : { x : α // p x q x }) :
(subtypeOrEquiv p q h) a = a
def subtypeOrEquiv {α : Type u_1} (p : αProp) (q : αProp) [] (h : Disjoint p q) :
{ x : α // p x q x } { x : α // p x } { x : α // q x }

A subtype {x // p x ∨ q x} over a disjunction of p q : α → Prop is equivalent to a sum of subtypes {x // p x} ⊕ {x // q x} such that ¬ p x is sent to the right, when Disjoint p q.

See also Equiv.sumCompl, for when IsCompl p q.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem subtypeOrEquiv_symm_inl {α : Type u_1} (p : αProp) (q : αProp) [] (h : Disjoint p q) (x : { x : α // p x }) :
(subtypeOrEquiv p q h).symm (Sum.inl x) = x,
@[simp]
theorem subtypeOrEquiv_symm_inr {α : Type u_1} (p : αProp) (q : αProp) [] (h : Disjoint p q) (x : { x : α // q x }) :
(subtypeOrEquiv p q h).symm (Sum.inr x) = x,
@[simp]
theorem Function.Embedding.sumSet_apply {α : Type u_1} {s : Set α} {t : Set α} (h : Disjoint s t) :
∀ (a : s t), = Sum.elim Subtype.val Subtype.val a
def Function.Embedding.sumSet {α : Type u_1} {s : Set α} {t : Set α} (h : Disjoint s t) :
s t α

For disjoint s t : Set α, the natural injection from ↑s ⊕ ↑t to α.

Equations
• = { toFun := Sum.elim Subtype.val Subtype.val, inj' := }
Instances For
theorem Function.Embedding.coe_sumSet {α : Type u_1} {s : Set α} {t : Set α} (h : Disjoint s t) :
= Sum.elim Subtype.val Subtype.val
@[simp]
theorem Function.Embedding.sumSet_preimage_inl {α : Type u_1} {s : Set α} {t : Set α} {r : Set α} (h : Disjoint s t) :
Subtype.val '' (Sum.inl ⁻¹' ( ⁻¹' r)) = r s
@[simp]
theorem Function.Embedding.sumSet_preimage_inr {α : Type u_1} {s : Set α} {t : Set α} {r : Set α} (h : Disjoint s t) :
Subtype.val '' (Sum.inr ⁻¹' ( ⁻¹' r)) = r t
@[simp]
theorem Function.Embedding.sumSet_range {α : Type u_1} {s : Set α} {t : Set α} (h : Disjoint s t) :
= s t
@[simp]
theorem Function.Embedding.sigmaSet_apply {α : Type u_1} {ι : Type u_2} {s : ιSet α} (h : Pairwise (Disjoint on s)) (x : (i : ι) × (s i)) :
= x.snd
def Function.Embedding.sigmaSet {α : Type u_1} {ι : Type u_2} {s : ιSet α} (h : Pairwise (Disjoint on s)) :
(i : ι) × (s i) α

For an indexed family s : ι → Set α of disjoint sets, the natural injection from the sigma-type (i : ι) × ↑(s i) to α.

Equations
• = { toFun := fun (x : (i : ι) × (s i)) => x.snd, inj' := }
Instances For
theorem Function.Embedding.coe_sigmaSet {α : Type u_1} {ι : Type u_2} {s : ιSet α} (h : Pairwise (Disjoint on s)) :
= fun (x : (i : ι) × (s i)) => x.snd
@[simp]
theorem Function.Embedding.sigmaSet_preimage {α : Type u_1} {ι : Type u_2} {s : ιSet α} (h : Pairwise (Disjoint on s)) (i : ι) (r : Set α) :
Subtype.val '' ( ⁻¹' ( ⁻¹' r)) = r s i
@[simp]
theorem Function.Embedding.sigmaSet_range {α : Type u_1} {ι : Type u_2} {s : ιSet α} (h : Pairwise (Disjoint on s)) :
= ⋃ (i : ι), s i