@[simp]

theorem Equiv.ofInjective_image {α : Type u_1} {β : Type u_2} (f : α → β) (hf : Function.Injective f) (s : Set α) : Subtype.val '' ⇑(ofInjective f hf) '' s = f '' s

theorem Function.Embedding.range_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α ↪ β) (g : β ↪ γ) : Set.range ⇑(f.trans g) = ⇑g '' Set.range ⇑f

@[simp]

theorem Function.Embedding.preimage_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α ↪ β) (g : β ↪ γ) (s : Set γ) : ⇑(f.trans g) ⁻¹' s = ⇑f ⁻¹' ⇑g ⁻¹' s

theorem Function.Embedding.image_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} (f : α ↪ β) (g : β ↪ γ) : ⇑(f.trans g) '' s = ⇑g '' ⇑f '' s

theorem Set.embeddingOfSubset_apply {α : Type u_1} {s t : Set α} (hst : s ⊆ t) (x : ↑s) : (s.embeddingOfSubset t hst) x = ⟨↑x, ⋯⟩

theorem Set.embeddingOfSubset_image {α : Type u_1} {s t : Set α} (hst : s ⊆ t) (r : Set ↑s) : ⇑(s.embeddingOfSubset t hst) '' r = {x : ↑t | ↑x ∈ Subtype.val '' r}

theorem Set.embeddingOfSubset_preimage {α : Type u_1} {s t : Set α} (hst : s ⊆ t) (r : Set ↑t) : ⇑(s.embeddingOfSubset t hst) ⁻¹' r = {x : ↑s | ↑x ∈ Subtype.val '' r}

@[simp]

theorem Set.embeddingOfSubset_coeFun {α : Type u_1} {s t : Set α} (hst : s ⊆ t) : ⇑(s.embeddingOfSubset t hst) = inclusion hst

@[simp]

theorem image_val_image_comp_inclusion {α : Type u_1} {β : Type u_2} (s : Set α) (r : Set ↑s) {t t' : Set β} (ht : t ⊆ t') (f : ↑s → ↑t) : Subtype.val '' (fun (x : ↑s) => Set.inclusion ht (f x)) '' r = Subtype.val '' f '' r

@[simp]

theorem image_val_range_comp_inclusion {α : Type u_1} {β : Type u_2} (s : Set α) {t t' : Set β} (ht : t ⊆ t') (f : ↑s → ↑t) : (Subtype.val '' Set.range fun (x : ↑s) => Set.inclusion ht (f x)) = Subtype.val '' Set.range f

@[simp]

theorem image_val_image_inclusion {α : Type u_1} {s t : Set α} (hst : s ⊆ t) (r : Set ↑s) : Subtype.val '' Set.inclusion hst '' r = Subtype.val '' r

@[simp]

theorem iUnion_preimage_image_sigmaMk_eq {ι : Type u_4} {α : ι → Type u_5} {f : (i : ι) → Set (α i)} {j : ι} : ⋃ (i : ι), Sigma.mk j ⁻¹' Sigma.mk i '' f i = f j

def Function.Embedding.setSubtype {α : Type u_4} (s : Set α) : ↑s ↪ α

The same as Function.Embedding.subtype, but for the special case of a set coercion. Can be more convenient for rewriting.

Equations

• Function.Embedding.setSubtype s = Function.Embedding.subtype fun (x : α) => x ∈ s

@[simp]

theorem Function.Embedding.setSubtype_apply {α : Type u_4} (s : Set α) (self : { x : α // x ∈ s }) : (setSubtype s) self = ↑self

@[simp]

theorem Function.Embedding.preimage_setSubtype {α : Type u_1} (s x : Set α) : ⇑(setSubtype s) ⁻¹' x = Subtype.val ⁻¹' x

@[simp]

theorem Function.Embedding.image_setSubtype {α : Type u_1} (s : Set α) (x : Set ↑s) : ⇑(setSubtype s) '' x = Subtype.val '' x

@[simp]

theorem Function.Embedding.range_setSubtype_eq {α : Type u_1} (s : Set α) : Set.range ⇑(setSubtype s) = s

noncomputable def Subtype.embeddingInsert {α : Type u_1} {β : Type u_2} {a : α} {b : β} {s : Set α} (f : ↑s ↪ β) (ha : ¬a ∈ s) (hb : ¬b ∈ Set.range ⇑f) : ↑(insert a s) ↪ β

An embedding defined on a coerced set can be extended to an embedding on an insertion.

Equations

• Subtype.embeddingInsert f ha hb = { toFun := Function.extend (Set.inclusion ⋯) ⇑f fun (x : ↑(insert a s)) => b, inj' := ⋯ }

theorem Subtype.embeddingInsert_apply_mem {α : Type u_1} {β : Type u_2} {a : α} {b : β} {s : Set α} (f : ↑s ↪ β) (ha : ¬a ∈ s) (hb : ¬b ∈ Set.range ⇑f) {x : ↑(insert a s)} (hx : ↑x ∈ s) : (embeddingInsert f ha hb) x = f ⟨↑x, hx⟩

theorem Subtype.embeddingInsert_apply {α : Type u_1} {β : Type u_2} {a : α} {b : β} {s : Set α} (f : ↑s ↪ β) (ha : ¬a ∈ s) (hb : ¬b ∈ Set.range ⇑f) : (embeddingInsert f ha hb) ⟨a, ⋯⟩ = b

theorem Subtype.embeddingInsert_apply' {α : Type u_1} {β : Type u_2} {a : α} {b : β} {s : Set α} (f : ↑s ↪ β) (ha : ¬a ∈ s) (hb : ¬b ∈ Set.range ⇑f) {x : ↑(insert a s)} (hx : ¬↑x ∈ s) : (embeddingInsert f ha hb) x = b

theorem Subtype.embeddingInsert_apply_eq_ite {α : Type u_1} {β : Type u_2} {a : α} {b : β} {s : Set α} (f : ↑s ↪ β) (ha : ¬a ∈ s) (hb : ¬b ∈ Set.range ⇑f) {x : ↑(insert a s)} [DecidablePred fun (x : α) => x ∈ s] : (embeddingInsert f ha hb) x = if hx : ↑x ∈ s then f ⟨↑x, hx⟩ else b

@[simp]

theorem Subtype.range_embeddingInsert {α : Type u_1} {β : Type u_2} {a : α} {b : β} {s : Set α} (f : ↑s ↪ β) (ha : ¬a ∈ s) (hb : ¬b ∈ Set.range ⇑f) : Set.range ⇑(embeddingInsert f ha hb) = insert b (Set.range ⇑f)

def Equiv.subsetEquivSubset {α : Type u_4} {β : Type u_5} {a s : Set α} {b t : Set β} (e : ↑s ≃ ↑t) (has : a ⊆ s) (hbt : b ⊆ t) (h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a) : ↑a ≃ ↑b

The restriction of an equivalence e : s ≃ t to a subset a of s and its image b.

Equations

• e.subsetEquivSubset has hbt h_eq = { toFun := fun (x : ↑a) => ⟨↑(e ⟨↑x, ⋯⟩), ⋯⟩, invFun := fun (x : ↑b) => ⟨↑(e.symm ⟨↑x, ⋯⟩), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.subsetEquivSubset_symm_apply_coe {α : Type u_4} {β : Type u_5} {a s : Set α} {b t : Set β} (e : ↑s ≃ ↑t) (has : a ⊆ s) (hbt : b ⊆ t) (h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a) (x : ↑b) : ↑((e.subsetEquivSubset has hbt h_eq).symm x) = ↑(e.symm ⟨↑x, ⋯⟩)

@[simp]

theorem Equiv.subsetEquivSubset_apply_coe {α : Type u_4} {β : Type u_5} {a s : Set α} {b t : Set β} (e : ↑s ≃ ↑t) (has : a ⊆ s) (hbt : b ⊆ t) (h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a) (x : ↑a) : ↑((e.subsetEquivSubset has hbt h_eq) x) = ↑(e ⟨↑x, ⋯⟩)

@[simp]

theorem Equiv.subsetEquivSubset_image_val {α : Type u_4} {β : Type u_5} {a s : Set α} {b t : Set β} (e : ↑s ≃ ↑t) (has : a ⊆ s) (hbt : b ⊆ t) (h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a) (u : Set ↑a) : Subtype.val '' ⇑(e.subsetEquivSubset has hbt h_eq) '' u = Subtype.val '' ⇑e '' Set.inclusion has '' u

def Equiv.subsetEquivImage {α : Type u_4} {β : Type u_5} {a s : Set α} {t : Set β} (e : ↑s ≃ ↑t) (has : a ⊆ s) : ↑a ≃ ↑(Subtype.val '' ⇑e '' Subtype.val ⁻¹' a)

Equations

• e.subsetEquivImage has = e.subsetEquivSubset has ⋯ ⋯

@[simp]

theorem Equiv.subsetEquivImage_apply_coe {α : Type u_4} {β : Type u_5} {a s : Set α} {t : Set β} (e : ↑s ≃ ↑t) (has : a ⊆ s) (x : ↑a) : ↑((e.subsetEquivImage has) x) = ↑(e ⟨↑x, ⋯⟩)

@[simp]

theorem Equiv.subsetEquivImage_symm_apply_coe {α : Type u_4} {β : Type u_5} {a s : Set α} {t : Set β} (e : ↑s ≃ ↑t) (has : a ⊆ s) (x : ↑(Subtype.val '' ⇑e '' Subtype.val ⁻¹' a)) : ↑((e.subsetEquivImage has).symm x) = ↑(e.symm ⟨↑x, ⋯⟩)