Interactions between embeddings and sets.

@[simp]

theorem Equiv.asEmbedding_range {α : Sort u_1} {β : Type u_2} {p : β → Prop} (e : α ≃ Subtype p) : Set.range ↑(Equiv.asEmbedding e) = 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' := (_ : Function.Injective Function.Embedding.some.toFun) }

@[simp]

theorem Function.Embedding.optionElim_apply {α : Type u_1} {β : Type u_2} (f : α ↪ β) (x : β) (h : ¬x ∈ Set.range ↑f) : ∀ (a : Option α), ↑(Function.Embedding.optionElim f 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

• Function.Embedding.optionElim f x h = { toFun := Option.elim' x ↑f, inj' := (_ : Function.Injective (Option.elim' x ↑f)) }

@[simp]

theorem Function.Embedding.optionEmbeddingEquiv_symm_apply (α : Type u_1) (β : Type u_2) (f : (f : α ↪ β) × ↑(Set.range ↑f)ᶜ) : ↑(Function.Embedding.optionEmbeddingEquiv α β).symm f = Function.Embedding.optionElim f.fst ↑f.snd (_ : ↑f.snd ∈ (Set.range ↑f.fst)ᶜ)

@[simp]

theorem Function.Embedding.optionEmbeddingEquiv_apply_fst (α : Type u_1) (β : Type u_2) (f : Option α ↪ β) : (↑(Function.Embedding.optionEmbeddingEquiv α β) f).fst = Function.Embedding.trans Function.Embedding.coeWithTop f

@[simp]

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

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

• One or more equations did not get rendered due to their size.

@[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 = { val := ↑f a, property := H a }

@[simp]

theorem Function.Embedding.image_apply {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Set α) : ↑(Function.Embedding.image f) s = ↑f '' s

def Function.Embedding.image {α : Type u_1} {β : Type u_2} (f : α ↪ β) : Set α ↪ Set β

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

Equations

• Function.Embedding.image f = { toFun := Set.image ↑f, inj' := (_ : Function.Injective (Set.image f.toFun)) }

@[simp]

theorem Set.embeddingOfSubset_apply {α : Type u_1} (s : Set α) (t : Set α) (h : s ⊆ t) (x : ↑s) : ↑(Set.embeddingOfSubset s t h) x = { val := ↑x, property := (_ : ↑x ∈ t) }

def Set.embeddingOfSubset {α : Type u_1} (s : Set α) (t : Set α) (h : s ⊆ t) : ↑s ↪ ↑t

The injection map is an embedding between subsets.

Equations

• One or more equations did not get rendered due to their size.

@[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) = { val := ↑x, property := (_ : p ↑x ∨ q ↑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) = { val := ↑x, property := (_ : p ↑x ∨ q ↑x) }