Interactions between embeddings and sets.

@[simp]

theorem Equiv.asEmbedding_range {α : Sort u_1} {β : Type u_2} {p : β → Prop} (e : α ≃ Subtype p) : Set.range ⇑e.asEmbedding = setOf p

@[simp]

theorem Function.Embedding.coeWithTop_apply {α : Type u_1} : ∀ (a : α), Function.Embedding.coeWithTop a = ↑a

def Function.Embedding.coeWithTop {α : Type u_1} : α ↪ WithTop α

Embedding into WithTop α.

Equations

• Function.Embedding.coeWithTop = let __src := Function.Embedding.some; { toFun := WithTop.some, inj' := ⋯ }

@[simp]

theorem Function.Embedding.optionElim_apply {α : Type u_1} {β : Type u_2} (f : α ↪ β) (x : β) (h : x ∉ Set.range ⇑f) : ∀ (a : Option α), (f.optionElim x h) a = Option.elim' x (⇑f) a

def Function.Embedding.optionElim {α : Type u_1} {β : Type u_2} (f : α ↪ β) (x : β) (h : x ∉ Set.range ⇑f) : Option α ↪ β

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

Equations

• f.optionElim x h = { toFun := Option.elim' x ⇑f, inj' := ⋯ }

@[simp]

theorem Function.Embedding.optionEmbeddingEquiv_apply_snd_coe (α : Type u_1) (β : Type u_2) (f : Option α ↪ β) : ↑((Function.Embedding.optionEmbeddingEquiv α β) f).snd = f none

@[simp]

theorem Function.Embedding.optionEmbeddingEquiv_apply_fst (α : Type u_1) (β : Type u_2) (f : Option α ↪ β) : ((Function.Embedding.optionEmbeddingEquiv α β) 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)ᶜ) : (Function.Embedding.optionEmbeddingEquiv α β).symm f = f.fst.optionElim ↑f.snd ⋯

def Function.Embedding.optionEmbeddingEquiv (α : Type u_1) (β : Type u_2) : (Option α ↪ β) ≃ (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.

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

• Function.Embedding.codRestrict p f H = { toFun := fun (a : α) => ⟨f a, ⋯⟩, inj' := ⋯ }

@[simp]

theorem Function.Embedding.codRestrict_apply {α : Sort u_1} {β : Type u_2} (p : Set β) (f : α ↪ β) (H : ∀ (a : α), f a ∈ p) (a : α) : (Function.Embedding.codRestrict p f H) 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 := Set.image ⇑f, inj' := ⋯ }

@[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' := ⋯ }

@[simp]

theorem subtypeOrEquiv_apply {α : Type u_1} (p : α → Prop) (q : α → Prop) [DecidablePred p] (h : Disjoint p q) (a : { x : α // p x ∨ q x }) : (subtypeOrEquiv p q h) a = (subtypeOrLeftEmbedding p q) a

def subtypeOrEquiv {α : Type u_1} (p : α → Prop) (q : α → Prop) [DecidablePred p] (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.

@[simp]

theorem subtypeOrEquiv_symm_inl {α : Type u_1} (p : α → Prop) (q : α → Prop) [DecidablePred p] (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) [DecidablePred p] (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), (Function.Embedding.sumSet h) a = 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

• Function.Embedding.sumSet h = { toFun := Sum.elim Subtype.val Subtype.val, inj' := ⋯ }

theorem Function.Embedding.coe_sumSet {α : Type u_1} {s : Set α} {t : Set α} (h : Disjoint s t) : ⇑(Function.Embedding.sumSet h) = 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 ⁻¹' (⇑(Function.Embedding.sumSet h) ⁻¹' 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 ⁻¹' (⇑(Function.Embedding.sumSet h) ⁻¹' r)) = r ∩ t

@[simp]

theorem Function.Embedding.sumSet_range {α : Type u_1} {s : Set α} {t : Set α} (h : Disjoint s t) : Set.range ⇑(Function.Embedding.sumSet h) = 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)) : (Function.Embedding.sigmaSet h) x = ↑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

• Function.Embedding.sigmaSet h = { toFun := fun (x : (i : ι) × ↑(s i)) => ↑x.snd, inj' := ⋯ }

theorem Function.Embedding.coe_sigmaSet {α : Type u_1} {ι : Type u_2} {s : ι → Set α} (h : Pairwise (Disjoint on s)) : ⇑(Function.Embedding.sigmaSet h) = 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 '' (Sigma.mk i ⁻¹' (⇑(Function.Embedding.sigmaSet h) ⁻¹' r)) = r ∩ s i

@[simp]

theorem Function.Embedding.sigmaSet_range {α : Type u_1} {ι : Type u_2} {s : ι → Set α} (h : Pairwise (Disjoint on s)) : Set.range ⇑(Function.Embedding.sigmaSet h) = ⋃ (i : ι), s i