Restrict the domain of a function to a set

Main definitions

• Set.domRestrict f s : restrict the domain of f to the set s;
• Set.codRestrict f s h : given h : ∀ x, f x ∈ s, restrict the codomain of f to the set s;

Domain restriction

def Set.domRestrict {α : Type u_1} {π : α → Type u_6} (s : Set α) (f : (a : α) → π a) (a : ↑s) : π ↑a

Restrict domain of a function f to a set s. Same as Subtype.restrict but this version takes an argument ↥s instead of Subtype s.

Equations

• s.domRestrict f x = f ↑x

theorem Set.domRestrict_def {α : Type u_1} {π : α → Type u_6} (s : Set α) : s.domRestrict = fun (f : (a : α) → π a) (x : ↑s) => f ↑x

theorem Set.domRestrict_eq {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) : s.domRestrict f = f ∘ Subtype.val

@[simp]

theorem Set.domRestrict_id {α : Type u_1} (s : Set α) : s.domRestrict id = Subtype.val

@[simp]

theorem Set.domRestrict_apply {α : Type u_1} {π : α → Type u_6} (f : (a : α) → π a) (s : Set α) (x : ↑s) : s.domRestrict f x = f ↑x

theorem Set.domRestrict_eq_iff {α : Type u_1} {π : α → Type u_6} {f : (a : α) → π a} {s : Set α} {g : (a : ↑s) → π ↑a} : s.domRestrict f = g ↔ ∀ (a : α) (ha : a ∈ s), f a = g ⟨a, ha⟩

theorem Set.eq_domRestrict_iff {α : Type u_1} {π : α → Type u_6} {s : Set α} {f : (a : ↑s) → π ↑a} {g : (a : α) → π a} : f = s.domRestrict g ↔ ∀ (a : α) (ha : a ∈ s), f ⟨a, ha⟩ = g a

@[simp]

theorem Set.range_domRestrict {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) : range (s.domRestrict f) = f '' s

theorem Set.image_domRestrict {α : Type u_1} {β : Type u_2} (f : α → β) (s t : Set α) : s.domRestrict f '' Subtype.val ⁻¹' t = f '' (t ∩ s)

@[simp]

theorem Set.domRestrict_dite {α : Type u_1} {β : Type u_2} {s : Set α} [(x : α) → Decidable (x ∈ s)] (f : (a : α) → a ∈ s → β) (g : (a : α) → ¬a ∈ s → β) : (s.domRestrict fun (a : α) => if h : a ∈ s then f a h else g a h) = fun (a : ↑s) => f ↑a ⋯

@[simp]

theorem Set.domRestrict_dite_compl {α : Type u_1} {β : Type u_2} {s : Set α} [(x : α) → Decidable (x ∈ s)] (f : (a : α) → a ∈ s → β) (g : (a : α) → ¬a ∈ s → β) : (sᶜ.domRestrict fun (a : α) => if h : a ∈ s then f a h else g a h) = fun (a : ↑sᶜ) => g ↑a ⋯

@[simp]

theorem Set.domRestrict_ite {α : Type u_1} {β : Type u_2} (f g : α → β) (s : Set α) [(x : α) → Decidable (x ∈ s)] : (s.domRestrict fun (a : α) => if a ∈ s then f a else g a) = s.domRestrict f

@[simp]

theorem Set.domRestrict_ite_compl {α : Type u_1} {β : Type u_2} (f g : α → β) (s : Set α) [(x : α) → Decidable (x ∈ s)] : (sᶜ.domRestrict fun (a : α) => if a ∈ s then f a else g a) = sᶜ.domRestrict g

@[simp]

theorem Set.domRestrict_piecewise {α : Type u_1} {β : Type u_2} (f g : α → β) (s : Set α) [(x : α) → Decidable (x ∈ s)] : s.domRestrict (s.piecewise f g) = s.domRestrict f

@[simp]

theorem Set.domRestrict_piecewise_compl {α : Type u_1} {β : Type u_2} (f g : α → β) (s : Set α) [(x : α) → Decidable (x ∈ s)] : sᶜ.domRestrict (s.piecewise f g) = sᶜ.domRestrict g

theorem Set.domRestrict_extend_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : α → γ) (g' : β → γ) : (range f).domRestrict (Function.extend f g g') = fun (x : ↑(range f)) => g (Exists.choose ⋯)

@[simp]

theorem Set.domRestrict_extend_compl_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : α → γ) (g' : β → γ) : (range f)ᶜ.domRestrict (Function.extend f g g') = g' ∘ Subtype.val

def Set.domRestrict₂ {α : Type u_1} {π : α → Type u_6} {s t : Set α} (hst : s ⊆ t) (f : (a : ↑t) → π ↑a) (a : ↑s) : π ↑a

If a function f is restricted to a set t, and s ⊆ t, this is the restriction to s.

Equations

• Set.domRestrict₂ hst f x = f ⟨↑x, ⋯⟩

theorem Set.domRestrict₂_def {α : Type u_1} {π : α → Type u_6} {s t : Set α} (hst : s ⊆ t) : domRestrict₂ hst = fun (f : (a : ↑t) → π ↑a) (x : ↑s) => f ⟨↑x, ⋯⟩

theorem Set.domRestrict₂_comp_domRestrict {α : Type u_1} {π : α → Type u_6} {s t : Set α} (hst : s ⊆ t) : domRestrict₂ hst ∘ t.domRestrict = s.domRestrict

theorem Set.domRestrict₂_comp_domRestrict₂ {α : Type u_1} {π : α → Type u_6} {s t u : Set α} (hst : s ⊆ t) (htu : t ⊆ u) : domRestrict₂ hst ∘ domRestrict₂ htu = domRestrict₂ ⋯

theorem Set.range_extend_subset {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : α → γ) (g' : β → γ) : range (Function.extend f g g') ⊆ range g ∪ g' '' (range f)ᶜ

theorem Set.range_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} (hf : Function.Injective f) (g : α → γ) (g' : β → γ) : range (Function.extend f g g') = range g ∪ g' '' (range f)ᶜ

theorem Function.FactorsThrough.extend_injOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} {j : β → γ} (hf : FactorsThrough g f) (hg : Injective g) : Set.InjOn (extend f g j) (Set.range f)

If g factors through f and g is injective, then extend f g j is injective on the range of f.

theorem Function.Injective.extend_injOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} {j : β → γ} (hf : Injective f) (hg : Injective g) : Set.InjOn (extend f g j) (Set.range f)

If f and g are injective, then extend f g j is injective on the range of f.

def Set.codRestrict {α : Type u_1} {ι : Sort u_5} (f : ι → α) (s : Set α) (h : ∀ (x : ι), f x ∈ s) : ι → ↑s

Restrict codomain of a function f to a set s. Same as Subtype.coind but this version has codomain ↥s instead of Subtype s.

Equations

• Set.codRestrict f s h x = ⟨f x, ⋯⟩

@[simp]

theorem Set.val_codRestrict_apply {α : Type u_1} {ι : Sort u_5} (f : ι → α) (s : Set α) (h : ∀ (x : ι), f x ∈ s) (x : ι) : ↑(codRestrict f s h x) = f x

@[simp]

theorem Set.domRestrict_comp_codRestrict {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : ι → α} {g : α → β} {b : Set α} (h : ∀ (x : ι), f x ∈ b) : b.domRestrict g ∘ codRestrict f b h = g ∘ f

@[simp]

theorem Set.injective_codRestrict {α : Type u_1} {ι : Sort u_5} {f : ι → α} {s : Set α} (h : ∀ (x : ι), f x ∈ s) : Function.Injective (codRestrict f s h) ↔ Function.Injective f

theorem Function.Injective.codRestrict {α : Type u_1} {ι : Sort u_5} {f : ι → α} {s : Set α} (h : ∀ (x : ι), f x ∈ s) : Injective f → Injective (Set.codRestrict f s h)

Alias of the reverse direction of Set.injective_codRestrict.

@[simp]

theorem Set.range_codRestrict {α : Type u_1} {ι : Sort u_5} {f : ι → α} {s : Set α} (h : ∀ (x : ι), f x ∈ s) : range (codRestrict f s h) = Subtype.val ⁻¹' range f

theorem Set.surjective_codRestrict {α : Type u_1} {ι : Sort u_5} {f : ι → α} {s : Set α} (h : ∀ (x : ι), f x ∈ s) : Function.Surjective (codRestrict f s h) ↔ range f = s

theorem Set.codRestrict_range_surjective {α : Type u_1} {ι : Sort u_5} (f : ι → α) : Function.Surjective (codRestrict f (range f) ⋯)

@[simp]

theorem Set.domRestrict_eq_domRestrict_iff {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} : s.domRestrict f₁ = s.domRestrict f₂ ↔ EqOn f₁ f₂ s

@[deprecated Set.domRestrict (since := "2026-07-19")]

def Set.restrict {α : Type u_1} {π : α → Type u_6} (s : Set α) (f : (a : α) → π a) (a : ↑s) : π ↑a

Alias of Set.domRestrict.

---

Restrict domain of a function f to a set s. Same as Subtype.restrict but this version takes an argument ↥s instead of Subtype s.

Equations

• @Set.restrict = @Set.domRestrict

@[deprecated Set.domRestrict_def (since := "2026-07-19")]

theorem Set.restrict_def {α : Type u_1} {π : α → Type u_6} (s : Set α) : s.domRestrict = fun (f : (a : α) → π a) (x : ↑s) => f ↑x

Alias of Set.domRestrict_def.

@[deprecated Set.domRestrict_eq (since := "2026-07-19")]

theorem Set.restrict_eq {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) : s.domRestrict f = f ∘ Subtype.val

Alias of Set.domRestrict_eq.

@[deprecated Set.domRestrict_id (since := "2026-07-19")]

theorem Set.restrict_id {α : Type u_1} (s : Set α) : s.domRestrict id = Subtype.val

Alias of Set.domRestrict_id.

@[deprecated Set.domRestrict_apply (since := "2026-07-19")]

theorem Set.restrict_apply {α : Type u_1} {π : α → Type u_6} (f : (a : α) → π a) (s : Set α) (x : ↑s) : s.domRestrict f x = f ↑x

Alias of Set.domRestrict_apply.

@[deprecated Set.domRestrict_eq_iff (since := "2026-07-19")]

theorem Set.restrict_eq_iff {α : Type u_1} {π : α → Type u_6} {f : (a : α) → π a} {s : Set α} {g : (a : ↑s) → π ↑a} : s.domRestrict f = g ↔ ∀ (a : α) (ha : a ∈ s), f a = g ⟨a, ha⟩

Alias of Set.domRestrict_eq_iff.

@[deprecated Set.eq_domRestrict_iff (since := "2026-07-19")]

theorem Set.eq_restrict_iff {α : Type u_1} {π : α → Type u_6} {s : Set α} {f : (a : ↑s) → π ↑a} {g : (a : α) → π a} : f = s.domRestrict g ↔ ∀ (a : α) (ha : a ∈ s), f ⟨a, ha⟩ = g a

Alias of Set.eq_domRestrict_iff.

@[deprecated Set.range_domRestrict (since := "2026-07-19")]

theorem Set.range_restrict {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) : range (s.domRestrict f) = f '' s

Alias of Set.range_domRestrict.

@[deprecated Set.image_domRestrict (since := "2026-07-19")]

theorem Set.image_restrict {α : Type u_1} {β : Type u_2} (f : α → β) (s t : Set α) : s.domRestrict f '' Subtype.val ⁻¹' t = f '' (t ∩ s)

Alias of Set.image_domRestrict.

@[deprecated Set.domRestrict_dite (since := "2026-07-19")]

theorem Set.restrict_dite {α : Type u_1} {β : Type u_2} {s : Set α} [(x : α) → Decidable (x ∈ s)] (f : (a : α) → a ∈ s → β) (g : (a : α) → ¬a ∈ s → β) : (s.domRestrict fun (a : α) => if h : a ∈ s then f a h else g a h) = fun (a : ↑s) => f ↑a ⋯

Alias of Set.domRestrict_dite.

@[deprecated Set.domRestrict_dite_compl (since := "2026-07-19")]

theorem Set.restrict_dite_compl {α : Type u_1} {β : Type u_2} {s : Set α} [(x : α) → Decidable (x ∈ s)] (f : (a : α) → a ∈ s → β) (g : (a : α) → ¬a ∈ s → β) : (sᶜ.domRestrict fun (a : α) => if h : a ∈ s then f a h else g a h) = fun (a : ↑sᶜ) => g ↑a ⋯

Alias of Set.domRestrict_dite_compl.

@[deprecated Set.domRestrict_ite (since := "2026-07-19")]

theorem Set.restrict_ite {α : Type u_1} {β : Type u_2} (f g : α → β) (s : Set α) [(x : α) → Decidable (x ∈ s)] : (s.domRestrict fun (a : α) => if a ∈ s then f a else g a) = s.domRestrict f

Alias of Set.domRestrict_ite.

@[deprecated Set.domRestrict_ite_compl (since := "2026-07-19")]

theorem Set.restrict_ite_compl {α : Type u_1} {β : Type u_2} (f g : α → β) (s : Set α) [(x : α) → Decidable (x ∈ s)] : (sᶜ.domRestrict fun (a : α) => if a ∈ s then f a else g a) = sᶜ.domRestrict g

Alias of Set.domRestrict_ite_compl.

@[deprecated Set.domRestrict_piecewise (since := "2026-07-19")]

theorem Set.restrict_piecewise {α : Type u_1} {β : Type u_2} (f g : α → β) (s : Set α) [(x : α) → Decidable (x ∈ s)] : s.domRestrict (s.piecewise f g) = s.domRestrict f

Alias of Set.domRestrict_piecewise.

@[deprecated Set.domRestrict_piecewise_compl (since := "2026-07-19")]

theorem Set.restrict_piecewise_compl {α : Type u_1} {β : Type u_2} (f g : α → β) (s : Set α) [(x : α) → Decidable (x ∈ s)] : sᶜ.domRestrict (s.piecewise f g) = sᶜ.domRestrict g

Alias of Set.domRestrict_piecewise_compl.

@[deprecated Set.domRestrict_extend_range (since := "2026-07-19")]

theorem Set.restrict_extend_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : α → γ) (g' : β → γ) : (range f).domRestrict (Function.extend f g g') = fun (x : ↑(range f)) => g (Exists.choose ⋯)

Alias of Set.domRestrict_extend_range.

@[deprecated Set.domRestrict_extend_compl_range (since := "2026-07-19")]

theorem Set.restrict_extend_compl_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : α → γ) (g' : β → γ) : (range f)ᶜ.domRestrict (Function.extend f g g') = g' ∘ Subtype.val

Alias of Set.domRestrict_extend_compl_range.

@[deprecated Set.domRestrict₂ (since := "2026-07-19")]

def Set.restrict₂ {α : Type u_1} {π : α → Type u_6} {s t : Set α} (hst : s ⊆ t) (f : (a : ↑t) → π ↑a) (a : ↑s) : π ↑a

Alias of Set.domRestrict₂.

---

If a function f is restricted to a set t, and s ⊆ t, this is the restriction to s.

Equations

• @Set.restrict₂ = @Set.domRestrict₂

@[deprecated Set.domRestrict₂_def (since := "2026-07-19")]

theorem Set.restrict₂_def {α : Type u_1} {π : α → Type u_6} {s t : Set α} (hst : s ⊆ t) : domRestrict₂ hst = fun (f : (a : ↑t) → π ↑a) (x : ↑s) => f ⟨↑x, ⋯⟩

Alias of Set.domRestrict₂_def.

@[deprecated Set.domRestrict₂_comp_domRestrict (since := "2026-07-19")]

theorem Set.restrict₂_comp_restrict {α : Type u_1} {π : α → Type u_6} {s t : Set α} (hst : s ⊆ t) : domRestrict₂ hst ∘ t.domRestrict = s.domRestrict

Alias of Set.domRestrict₂_comp_domRestrict.

@[deprecated Set.domRestrict₂_comp_domRestrict₂ (since := "2026-07-19")]

theorem Set.restrict₂_comp_restrict₂ {α : Type u_1} {π : α → Type u_6} {s t u : Set α} (hst : s ⊆ t) (htu : t ⊆ u) : domRestrict₂ hst ∘ domRestrict₂ htu = domRestrict₂ ⋯

Alias of Set.domRestrict₂_comp_domRestrict₂.

@[deprecated Set.domRestrict_comp_codRestrict (since := "2026-07-19")]

theorem Set.restrict_comp_codRestrict {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : ι → α} {g : α → β} {b : Set α} (h : ∀ (x : ι), f x ∈ b) : b.domRestrict g ∘ codRestrict f b h = g ∘ f

Alias of Set.domRestrict_comp_codRestrict.

@[deprecated Set.domRestrict_eq_domRestrict_iff (since := "2026-07-19")]

theorem Set.restrict_eq_restrict_iff {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} : s.domRestrict f₁ = s.domRestrict f₂ ↔ EqOn f₁ f₂ s

Alias of Set.domRestrict_eq_domRestrict_iff.

theorem Set.MapsTo.restrict_commutes {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) (t : Set β) (h : MapsTo f s t) : Subtype.val ∘ restrict f s t h = f ∘ Subtype.val

@[simp]

theorem Set.MapsTo.val_restrict_apply {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : MapsTo f s t) (x : ↑s) : ↑(restrict f s t h x) = f ↑x

theorem Set.MapsTo.coe_iterate_restrict {α : Type u_1} {s : Set α} {f : α → α} (h : MapsTo f s s) (x : ↑s) (k : ℕ) : ↑((restrict f s s h)^[k] x) = f^[k] ↑x

@[simp]

theorem Set.codRestrict_domRestrict {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : ∀ (x : ↑s), f ↑x ∈ t) : codRestrict (s.domRestrict f) t h = MapsTo.restrict f s t ⋯

Restricting the domain and then the codomain is the same as MapsTo.restrict.

@[deprecated Set.codRestrict_domRestrict (since := "2026-07-19")]

theorem Set.codRestrict_restrict {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : ∀ (x : ↑s), f ↑x ∈ t) : codRestrict (s.domRestrict f) t h = MapsTo.restrict f s t ⋯

Alias of Set.codRestrict_domRestrict.

---

Restricting the domain and then the codomain is the same as MapsTo.restrict.

theorem Set.MapsTo.restrict_eq_codRestrict {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : MapsTo f s t) : restrict f s t h = codRestrict (s.domRestrict f) t ⋯

Reverse of Set.codRestrict_domRestrict.

theorem Set.MapsTo.coe_restrict {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : MapsTo f s t) : Subtype.val ∘ restrict f s t h = s.domRestrict f

theorem Set.MapsTo.range_restrict {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) (t : Set β) (h : MapsTo f s t) : range (restrict f s t h) = Subtype.val ⁻¹' f '' s

theorem Set.mapsTo_iff_exists_map_subtype {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} : MapsTo f s t ↔ ∃ (g : ↑s → ↑t), ∀ (x : ↑s), f ↑x = ↑(g x)

theorem Set.surjective_mapsTo_image_restrict {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) : Function.Surjective (MapsTo.restrict f s (f '' s) ⋯)

Restriction onto preimage

theorem Set.image_restrictPreimage {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) (f : α → β) : t.restrictPreimage f '' Subtype.val ⁻¹' s = Subtype.val ⁻¹' f '' s

theorem Set.range_restrictPreimage {α : Type u_1} {β : Type u_2} (t : Set β) (f : α → β) : range (t.restrictPreimage f) = Subtype.val ⁻¹' range f

@[simp]

theorem Set.restrictPreimage_mk {α : Type u_1} {β : Type u_2} (t : Set β) {f : α → β} {a : α} (h : a ∈ f ⁻¹' t) : t.restrictPreimage f ⟨a, h⟩ = ⟨f a, h⟩

theorem Set.image_val_preimage_restrictPreimage {α : Type u_1} {β : Type u_2} (t : Set β) {f : α → β} {u : Set ↑t} : Subtype.val '' t.restrictPreimage f ⁻¹' u = f ⁻¹' Subtype.val '' u

theorem Set.preimage_restrictPreimage {α : Type u_1} {β : Type u_2} (t : Set β) {f : α → β} {u : Set ↑t} : t.restrictPreimage f ⁻¹' u = (fun (a : ↑(f ⁻¹' t)) => f ↑a) ⁻¹' Subtype.val '' u

theorem Set.restrictPreimage_injective {α : Type u_1} {β : Type u_2} (t : Set β) {f : α → β} (hf : Function.Injective f) : Function.Injective (t.restrictPreimage f)

theorem Set.restrictPreimage_surjective {α : Type u_1} {β : Type u_2} (t : Set β) {f : α → β} (hf : Function.Surjective f) : Function.Surjective (t.restrictPreimage f)

theorem Set.restrictPreimage_bijective {α : Type u_1} {β : Type u_2} (t : Set β) {f : α → β} (hf : Function.Bijective f) : Function.Bijective (t.restrictPreimage f)

theorem Function.Injective.restrictPreimage {α : Type u_1} {β : Type u_2} (t : Set β) {f : α → β} (hf : Injective f) : Injective (t.restrictPreimage f)

Alias of Set.restrictPreimage_injective.

theorem Function.Surjective.restrictPreimage {α : Type u_1} {β : Type u_2} (t : Set β) {f : α → β} (hf : Surjective f) : Surjective (t.restrictPreimage f)

Alias of Set.restrictPreimage_surjective.

theorem Function.Bijective.restrictPreimage {α : Type u_1} {β : Type u_2} (t : Set β) {f : α → β} (hf : Bijective f) : Bijective (t.restrictPreimage f)

Alias of Set.restrictPreimage_bijective.

Injectivity on a set

theorem Set.injOn_iff_injective {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} : InjOn f s ↔ Function.Injective (s.domRestrict f)

theorem Set.InjOn.injective {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} : InjOn f s → Function.Injective (s.domRestrict f)

Alias of the forward direction of Set.injOn_iff_injective.

theorem Set.MapsTo.restrict_inj {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : MapsTo f s t) : Function.Injective (restrict f s t h) ↔ InjOn f s

Surjectivity on a set

theorem Set.surjOn_iff_surjective {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} : SurjOn f s univ ↔ Function.Surjective (s.domRestrict f)

@[simp]

theorem Set.MapsTo.restrict_surjective_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : MapsTo f s t) : Function.Surjective (restrict f s t h) ↔ SurjOn f s t