mathlib documentation

data.equiv.set

Equivalences and sets #

In this file we provide lemmas linking equivalences to sets.

Some notable definitions are:

This file is separate from equiv/basic such that we do not require the full lattice structure on sets before defining what an equivalence is.

source
@[simp]
theorem equiv.range_eq_univ {α : Type u_1} {β : Type u_2} (e : α ≃ β) :
set.range ⇑e = set.univ
source
@[protected]
theorem equiv.image_eq_preimage {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set α) :
⇑e '' s = ⇑(e.symm) ⁻¹' s
source
theorem set.mem_image_equiv {α : Type u_1} {β : Type u_2} {S : set α} {f : α ≃ β} {x : β} :
x ∈ ⇑f '' S ↔ ⇑(f.symm) x ∈ S
source
theorem set.image_equiv_eq_preimage_symm {α : Type u_1} {β : Type u_2} (S : set α) (f : α ≃ β) :
⇑f '' S = ⇑(f.symm) ⁻¹' S

Alias for equiv.image_eq_preimage

source
theorem set.preimage_equiv_eq_image_symm {α : Type u_1} {β : Type u_2} (S : set α) (f : β ≃ α) :
⇑f ⁻¹' S = ⇑(f.symm) '' S

Alias for equiv.image_eq_preimage

source
@[protected, simp]
theorem equiv.subset_image {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set α) (t : set β) :
⇑(e.symm) '' t ⊆ s ↔ t ⊆ ⇑e '' s
source
@[protected, simp]
theorem equiv.subset_image' {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set α) (t : set β) :
s ⊆ ⇑(e.symm) '' t ↔ ⇑e '' s ⊆ t
source
@[simp]
theorem equiv.symm_image_image {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set α) :
⇑(e.symm) '' (⇑e '' s) = s
source
theorem equiv.eq_image_iff_symm_image_eq {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set α) (t : set β) :
t = ⇑e '' s ↔ ⇑(e.symm) '' t = s
source
@[simp]
theorem equiv.image_symm_image {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set β) :
⇑e '' (⇑(e.symm) '' s) = s
source
@[simp]
theorem equiv.image_preimage {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set β) :
⇑e '' (⇑e ⁻¹' s) = s
source
@[simp]
theorem equiv.preimage_image {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set α) :
⇑e ⁻¹' (⇑e '' s) = s
source
@[protected]
theorem equiv.image_compl {α : Type u_1} {β : Type u_2} (f : α ≃ β) (s : set α) :
⇑f '' sᶜ = (⇑f '' s)ᶜ
source
@[simp]
theorem equiv.symm_preimage_preimage {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set β) :
⇑(e.symm) ⁻¹' (⇑e ⁻¹' s) = s
source
@[simp]
theorem equiv.preimage_symm_preimage {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set α) :
⇑e ⁻¹' (⇑(e.symm) ⁻¹' s) = s
source
@[simp]
theorem equiv.preimage_subset {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s t : set β) :
⇑e ⁻¹' s ⊆ ⇑e ⁻¹' t ↔ s ⊆ t
source
@[simp]
theorem equiv.image_subset {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s t : set α) :
⇑e '' s ⊆ ⇑e '' t ↔ s ⊆ t
source
@[simp]
theorem equiv.image_eq_iff_eq {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s t : set α) :
⇑e '' s = ⇑e '' t ↔ s = t
source
theorem equiv.preimage_eq_iff_eq_image {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set β) (t : set α) :
⇑e ⁻¹' s = t ↔ s = ⇑e '' t
source
theorem equiv.eq_preimage_iff_image_eq {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set α) (t : set β) :
s = ⇑e ⁻¹' t ↔ ⇑e '' s = t
source
theorem equiv.prod_assoc_preimage {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : set α} {t : set β} {u : set γ} :
⇑(equiv.prod_assoc α β γ) ⁻¹' s.prod (t.prod u) = (s.prod t).prod u
source
def equiv.set_prod_equiv_sigma {α : Type u_1} {β : Type u_2} (s : set (α × β)) :
↥s ≃ Σ (x : α), ↥{y : β | (x, y) ∈ s}

A set s in α × β is equivalent to the sigma-type Σ x, {y | (x, y) ∈ s}.

Equations
source
def equiv.set_congr {α : Type u_1} {s t : set α} (h : s = t) :
↥s ≃ ↥t

The subtypes corresponding to equal sets are equivalent.

Equations
source
@[simp]
theorem equiv.set_congr_apply {α : Type u_1} {s t : set α} (h : s = t) (x : {a // (λ (a : α), (λ (x : α), x ∈ s) a) a}) :
⇑(equiv.set_congr h) x = ⟨↑x, _⟩
source
@[simp]
theorem equiv.image_apply_coe {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set α) (x : ↥s) :
↑(⇑(e.image s) x) = ⇑e x.val
source
def equiv.image {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set α) :
↥s ≃ ↥(⇑e '' s)

A set is equivalent to its image under an equivalence.

Equations
source
@[simp]
theorem equiv.image_symm_apply_coe {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set α) (y : ↥(⇑e '' s)) :
↑(⇑((e.image s).symm) y) = ⇑(e.symm) y.val
source
@[simp]
theorem equiv.set.univ_symm_apply (α : Type u_1) (a : α) :
⇑((equiv.set.univ α).symm) a = ⟨a, trivial⟩
source
@[protected]
def equiv.set.univ (α : Type u_1) :
↥set.univ ≃ α

univ α is equivalent to α.

Equations
source
@[simp]
theorem equiv.set.univ_apply (α : Type u_1) (ᾰ : ↥set.univ) :
⇑(equiv.set.univ α) ᾰ = ↑ᾰ
source
@[protected]
def equiv.set.empty (α : Type u_1) :
↥∅ ≃ empty

An empty set is equivalent to the empty type.

Equations
source
@[protected]
def equiv.set.pempty (α : Type u_1) :
↥∅ ≃ pempty

An empty set is equivalent to a pempty type.

Equations
source
@[protected]
def equiv.set.union' {α : Type u_1} {s t : set α} (p : α → Prop) [decidable_pred p] (hs : ∀ (x : α), x ∈ s → p x) (ht : ∀ (x : α), x ∈ t → ¬p x) :
↥(s ∪ t) ≃ ↥s ⊕ ↥t

If sets s and t are separated by a decidable predicate, then s ∪ t is equivalent to s ⊕ t.

Equations
source
@[protected]
def equiv.set.union {α : Type u_1} {s t : set α} [decidable_pred (λ (x : α), x ∈ s)] (H : s ∩ t ⊆ ∅) :
↥(s ∪ t) ≃ ↥s ⊕ ↥t

If sets s and t are disjoint, then s ∪ t is equivalent to s ⊕ t.

Equations
source
theorem equiv.set.union_apply_left {α : Type u_1} {s t : set α} [decidable_pred (λ (x : α), x ∈ s)] (H : s ∩ t ⊆ ∅) {a : ↥(s ∪ t)} (ha : ↑a ∈ s) :
⇑(equiv.set.union H) a = sum.inl ⟨↑a, ha⟩
source
theorem equiv.set.union_apply_right {α : Type u_1} {s t : set α} [decidable_pred (λ (x : α), x ∈ s)] (H : s ∩ t ⊆ ∅) {a : ↥(s ∪ t)} (ha : ↑a ∈ t) :
⇑(equiv.set.union H) a = sum.inr ⟨↑a, ha⟩
source
@[simp]
theorem equiv.set.union_symm_apply_left {α : Type u_1} {s t : set α} [decidable_pred (λ (x : α), x ∈ s)] (H : s ∩ t ⊆ ∅) (a : ↥s) :
⇑((equiv.set.union H).symm) (sum.inl a) = ⟨↑a, _⟩
source
@[simp]
theorem equiv.set.union_symm_apply_right {α : Type u_1} {s t : set α} [decidable_pred (λ (x : α), x ∈ s)] (H : s ∩ t ⊆ ∅) (a : ↥t) :
⇑((equiv.set.union H).symm) (sum.inr a) = ⟨↑a, _⟩
source
@[protected]
def equiv.set.singleton {α : Type u_1} (a : α) :
↥{a} ≃ punit

A singleton set is equivalent to a punit type.

Equations
source
@[simp]
theorem equiv.set.of_eq_apply {α : Type u} {s t : set α} (h : s = t) (x : ↥s) :
⇑(equiv.set.of_eq h) x = ⟨↑x, _⟩
source
@[protected]
def equiv.set.of_eq {α : Type u} {s t : set α} (h : s = t) :
↥s ≃ ↥t

Equal sets are equivalent.

Equations
source
@[simp]
theorem equiv.set.of_eq_symm_apply {α : Type u} {s t : set α} (h : s = t) (x : ↥t) :
⇑((equiv.set.of_eq h).symm) x = ⟨↑x, _⟩
source
@[protected]
def equiv.set.insert {α : Type u} {s : set α} [decidable_pred (λ (_x : α), _x ∈ s)] {a : α} (H : a ∉ s) :
↥(insert a s) ≃ ↥s ⊕ punit

If a ∉ s, then insert a s is equivalent to s ⊕ punit.

Equations
source
@[simp]
theorem equiv.set.insert_symm_apply_inl {α : Type u} {s : set α} [decidable_pred (λ (_x : α), _x ∈ s)] {a : α} (H : a ∉ s) (b : ↥s) :
⇑((equiv.set.insert H).symm) (sum.inl b) = ⟨↑b, _⟩
source
@[simp]
theorem equiv.set.insert_symm_apply_inr {α : Type u} {s : set α} [decidable_pred (λ (_x : α), _x ∈ s)] {a : α} (H : a ∉ s) (b : punit) :
⇑((equiv.set.insert H).symm) (sum.inr b) = ⟨a, _⟩
source
@[simp]
theorem equiv.set.insert_apply_left {α : Type u} {s : set α} [decidable_pred (λ (_x : α), _x ∈ s)] {a : α} (H : a ∉ s) :
⇑(equiv.set.insert H) ⟨a, _⟩ = sum.inr punit.star
source
@[simp]
theorem equiv.set.insert_apply_right {α : Type u} {s : set α} [decidable_pred (λ (_x : α), _x ∈ s)] {a : α} (H : a ∉ s) (b : ↥s) :
⇑(equiv.set.insert H) ⟨↑b, _⟩ = sum.inl b
source
@[protected]
def equiv.set.sum_compl {α : Type u_1} (s : set α) [decidable_pred (λ (_x : α), _x ∈ s)] :
↥s ⊕ ↥sᶜ ≃ α

If s : set α is a set with decidable membership, then s ⊕ sᶜ is equivalent to α.

Equations
source
@[simp]
theorem equiv.set.sum_compl_apply_inl {α : Type u} (s : set α) [decidable_pred (λ (_x : α), _x ∈ s)] (x : ↥s) :
⇑(equiv.set.sum_compl s) (sum.inl x) = ↑x
source
@[simp]
theorem equiv.set.sum_compl_apply_inr {α : Type u} (s : set α) [decidable_pred (λ (_x : α), _x ∈ s)] (x : ↥sᶜ) :
⇑(equiv.set.sum_compl s) (sum.inr x) = ↑x
source
theorem equiv.set.sum_compl_symm_apply_of_mem {α : Type u} {s : set α} [decidable_pred (λ (_x : α), _x ∈ s)] {x : α} (hx : x ∈ s) :
⇑((equiv.set.sum_compl s).symm) x = sum.inl ⟨x, hx⟩
source
theorem equiv.set.sum_compl_symm_apply_of_not_mem {α : Type u} {s : set α} [decidable_pred (λ (_x : α), _x ∈ s)] {x : α} (hx : x ∉ s) :
⇑((equiv.set.sum_compl s).symm) x = sum.inr ⟨x, hx⟩
source
@[simp]
theorem equiv.set.sum_compl_symm_apply {α : Type u_1} {s : set α} [decidable_pred (λ (_x : α), _x ∈ s)] {x : ↥s} :
⇑((equiv.set.sum_compl s).symm) ↑x = sum.inl x
source
@[simp]
theorem equiv.set.sum_compl_symm_apply_compl {α : Type u_1} {s : set α} [decidable_pred (λ (_x : α), _x ∈ s)] {x : ↥sᶜ} :
⇑((equiv.set.sum_compl s).symm) ↑x = sum.inr x
source
@[protected]
def equiv.set.sum_diff_subset {α : Type u_1} {s t : set α} (h : s ⊆ t) [decidable_pred (λ (_x : α), _x ∈ s)] :
↥s ⊕ ↥(t \ s) ≃ ↥t

sum_diff_subset s t is the natural equivalence between s ⊕ (t \ s) and t, where s and t are two sets.

Equations
source
@[simp]
theorem equiv.set.sum_diff_subset_apply_inl {α : Type u_1} {s t : set α} (h : s ⊆ t) [decidable_pred (λ (_x : α), _x ∈ s)] (x : ↥s) :
⇑(equiv.set.sum_diff_subset h) (sum.inl x) = set.inclusion h x
source
@[simp]
theorem equiv.set.sum_diff_subset_apply_inr {α : Type u_1} {s t : set α} (h : s ⊆ t) [decidable_pred (λ (_x : α), _x ∈ s)] (x : ↥(t \ s)) :
⇑(equiv.set.sum_diff_subset h) (sum.inr x) = set.inclusion _ x
source
theorem equiv.set.sum_diff_subset_symm_apply_of_mem {α : Type u_1} {s t : set α} (h : s ⊆ t) [decidable_pred (λ (_x : α), _x ∈ s)] {x : ↥t} (hx : x.val ∈ s) :
⇑((equiv.set.sum_diff_subset h).symm) x = sum.inl ⟨↑x, hx⟩
source
theorem equiv.set.sum_diff_subset_symm_apply_of_not_mem {α : Type u_1} {s t : set α} (h : s ⊆ t) [decidable_pred (λ (_x : α), _x ∈ s)] {x : ↥t} (hx : x.val ∉ s) :
⇑((equiv.set.sum_diff_subset h).symm) x = sum.inr ⟨↑x, _⟩
source
@[protected]
def equiv.set.union_sum_inter {α : Type u} (s t : set α) [decidable_pred (λ (_x : α), _x ∈ s)] :
↥(s ∪ t) ⊕ ↥(s ∩ t) ≃ ↥s ⊕ ↥t

If s is a set with decidable membership, then the sum of s ∪ t and s ∩ t is equivalent to s ⊕ t.

Equations
source
@[protected]
def equiv.set.compl {α : Type u} {β : Type v} {s : set α} {t : set β} [decidable_pred (λ (_x : α), _x ∈ s)] [decidable_pred (λ (_x : β), _x ∈ t)] (e₀ : ↥s ≃ ↥t) :
{e // ∀ (x : ↥s), ⇑e ↑x = ↑(⇑e₀ x)} ≃ (↥sᶜ ≃ ↥tᶜ)

Given an equivalence e₀ between sets s : set α and t : set β, the set of equivalences e : α ≃ β such that e ↑x = ↑(e₀ x) for each x : s is equivalent to the set of equivalences between sᶜ and tᶜ.

Equations
source
@[protected]
def equiv.set.prod {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :
↥(s.prod t) ≃ ↥s × ↥t

The set product of two sets is equivalent to the type product of their coercions to types.

Equations
source
@[protected]
noncomputable def equiv.set.image_of_inj_on {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) (H : set.inj_on f s) :
↥s ≃ ↥(f '' s)

If a function f is injective on a set s, then s is equivalent to f '' s.

Equations
source
@[protected]
noncomputable def equiv.set.image {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) (H : function.injective f) :
↥s ≃ ↥(f '' s)

If f is an injective function, then s is equivalent to f '' s.

Equations
source
@[simp]
theorem equiv.set.image_apply {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) (H : function.injective f) (p : ↥s) :
⇑(equiv.set.image f s H) p = ⟨f ↑p, _⟩
source
@[protected, simp]
theorem equiv.set.image_symm_apply {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) (H : function.injective f) (x : α) (h : x ∈ s) :
⇑((equiv.set.image f s H).symm) ⟨f x, _⟩ = ⟨x, h⟩
source
theorem equiv.set.image_symm_preimage {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.injective f) (u s : set α) :
(λ (x : ↥(f '' s)), ↑(⇑((equiv.set.image f s hf).symm) x)) ⁻¹' u = coe ⁻¹' (f '' u)
source
@[simp]
theorem equiv.set.congr_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set α) :
⇑(equiv.set.congr e) s = ⇑e '' s
source
@[protected]
def equiv.set.congr {α : Type u_1} {β : Type u_2} (e : α ≃ β) :
set α ≃ set β

If α is equivalent to β, then set α is equivalent to set β.

Equations
source
@[simp]
theorem equiv.set.congr_symm_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (t : set β) :
⇑((equiv.set.congr e).symm) t = ⇑(e.symm) '' t
source
@[protected]
def equiv.set.sep {α : Type u} (s : set α) (t : α → Prop) :
↥{x ∈ s | t x} ≃ ↥{x : ↥s | t ↑x}

The set {x ∈ s | t x} is equivalent to the set of x : s such that t x.

Equations
source
@[protected]
def equiv.set.powerset {α : Type u_1} (S : set α) :
↥𝒫S ≃ set ↥S

The set 𝒫 S := {x | x ⊆ S} is equivalent to the type set S.

Equations
source
@[simp]
theorem equiv.set.range_splitting_image_equiv_symm_apply_coe {α : Type u_1} {β : Type u_2} (f : α → β) (s : set ↥(set.range f)) (x : ↥s) :
↑(⇑((equiv.set.range_splitting_image_equiv f s).symm) x) = set.range_splitting f ↑x
source
noncomputable def equiv.set.range_splitting_image_equiv {α : Type u_1} {β : Type u_2} (f : α → β) (s : set ↥(set.range f)) :
↥(set.range_splitting f '' s) ≃ ↥s

If s is a set in range f, then its image under range_splitting f is in bijection (via f) with s.

Equations
source
@[simp]
theorem equiv.set.range_splitting_image_equiv_apply_coe_coe {α : Type u_1} {β : Type u_2} (f : α → β) (s : set ↥(set.range f)) (x : ↥(set.range_splitting f '' s)) :
↑↑(⇑(equiv.set.range_splitting_image_equiv f s) x) = f ↑x
source
@[simp]
theorem equiv.of_left_inverse_symm_apply {α : Sort u_1} {β : Type u_2} (f : α → β) (f_inv : nonempty α → β → α) (hf : ∀ (h : nonempty α), function.left_inverse (f_inv h) f) (b : ↥(set.range f)) :
⇑((equiv.of_left_inverse f f_inv hf).symm) b = f_inv _ ↑b
source
def equiv.of_left_inverse {α : Sort u_1} {β : Type u_2} (f : α → β) (f_inv : nonempty α → β → α) (hf : ∀ (h : nonempty α), function.left_inverse (f_inv h) f) :
α ≃ ↥(set.range f)

If f : α → β has a left-inverse when α is nonempty, then α is computably equivalent to the range of f.

While awkward, the nonempty α hypothesis on f_inv and hf allows this to be used when α is empty too. This hypothesis is absent on analogous definitions on stronger equivs like linear_equiv.of_left_inverse and ring_equiv.of_left_inverse as their typeclass assumptions are already sufficient to ensure non-emptiness.

Equations
source
@[simp]
theorem equiv.of_left_inverse_apply_coe {α : Sort u_1} {β : Type u_2} (f : α → β) (f_inv : nonempty α → β → α) (hf : ∀ (h : nonempty α), function.left_inverse (f_inv h) f) (a : α) :
↑(⇑(equiv.of_left_inverse f f_inv hf) a) = f a
source
def equiv.of_left_inverse' {α : Sort u_1} {β : Type u_2} (f : α → β) (f_inv : β → α) (hf : function.left_inverse f_inv f) :
α ≃ ↥(set.range f)

If f : α → β has a left-inverse, then α is computably equivalent to the range of f.

Note that if α is empty, no such f_inv exists and so this definition can't be used, unlike the stronger but less convenient of_left_inverse.

source
@[simp]
theorem equiv.of_injective_apply {α : Sort u_1} {β : Type u_2} (f : α → β) (hf : function.injective f) (a : α) :
⇑(equiv.of_injective f hf) a = ⟨f a, _⟩
source
noncomputable def equiv.of_injective {α : Sort u_1} {β : Type u_2} (f : α → β) (hf : function.injective f) :
α ≃ ↥(set.range f)

If f : α → β is an injective function, then domain α is equivalent to the range of f.

Equations
source
theorem equiv.apply_of_injective_symm {α : Sort u_1} {β : Type u_2} (f : α → β) (hf : function.injective f) (b : ↥(set.range f)) :
f (⇑((equiv.of_injective f hf).symm) b) = ↑b
source
@[simp]
theorem equiv.of_injective_symm_apply {α : Sort u_1} {β : Type u_2} (f : α → β) (hf : function.injective f) (a : α) :
⇑((equiv.of_injective f hf).symm) ⟨f a, _⟩ = a
source
theorem equiv.coe_of_injective_symm {α : Type u_1} {β : Type u_2} (f : α → β) (hf : function.injective f) :
⇑((equiv.of_injective f hf).symm) = set.range_splitting f
source
@[simp]
theorem equiv.self_comp_of_injective_symm {α : Sort u_1} {β : Type u_2} (f : α → β) (hf : function.injective f) :
f ∘ ⇑((equiv.of_injective f hf).symm) = coe
source
theorem equiv.of_left_inverse_eq_of_injective {α : Type u_1} {β : Type u_2} (f : α → β) (f_inv : nonempty α → β → α) (hf : ∀ (h : nonempty α), function.left_inverse (f_inv h) f) :
equiv.of_left_inverse f f_inv hf = equiv.of_injective f _
source
theorem equiv.of_left_inverse'_eq_of_injective {α : Type u_1} {β : Type u_2} (f : α → β) (f_inv : β → α) (hf : function.left_inverse f_inv f) :
equiv.of_left_inverse' f f_inv hf = equiv.of_injective f _
source
@[protected]
theorem equiv.set_forall_iff {α : Type u_1} {β : Type u_2} (e : α ≃ β) {p : set α → Prop} :
(∀ (a : set α), p a) ↔ ∀ (a : set β), p (⇑e ⁻¹' a)
source
@[protected]
theorem equiv.preimage_sUnion {α : Type u_1} {β : Type u_2} (f : α ≃ β) {s : set (set β)} :
⇑f ⁻¹' ⋃₀s = ⋃₀(set.image ⇑f ⁻¹' s)
source
noncomputable def set.bij_on.equiv {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} (f : α → β) (h : set.bij_on f s t) :
↥s ≃ ↥t

If a function is a bijection between two sets s and t, then it induces an equivalence between the types ↥s and ``↥t`.

Equations
source
theorem dite_comp_equiv_update {α : Type u_1} {β : Sort u_2} {γ : Sort u_3} {s : set α} (e : β ≃ ↥s) (v : β → γ) (w : α → γ) (j : β) (x : γ) [decidable_eq β] [decidable_eq α] [Π (j : α), decidable (j ∈ s)] :
(λ (i : α), dite (i ∈ s) (λ (h : i ∈ s), function.update v j x (⇑(e.symm) ⟨i, h⟩)) (λ (h : i ∉ s), w i)) = function.update (λ (i : α), dite (i ∈ s) (λ (h : i ∈ s), v (⇑(e.symm) ⟨i, h⟩)) (λ (h : i ∉ s), w i)) ↑(⇑e j) x

The composition of an updated function with an equiv on a subset can be expressed as an updated function.