Restrict the domain of a function to a set

Main definitions

• Set.restrict 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;

Restrict

def Set.restrict {α : 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.restrict f x = f ↑x

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

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

@[simp]

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

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

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

@[simp]

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

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

@[simp]

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.restrict fun (a : α) => if h : a ∈ s then f a h else g a h) = fun (a : ↑s) => f ↑a ⋯

@[simp]

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ᶜ.restrict fun (a : α) => if h : a ∈ s then f a h else g a h) = fun (a : ↑sᶜ) => g ↑a ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

def Set.restrict₂ {α : 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.restrict₂ hst f x = f ⟨↑x, ⋯⟩

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

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

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

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)ᶜ

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.restrict_comp_codRestrict {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : ι → α} {g : α → β} {b : Set α} (h : ∀ (x : ι), f x ∈ b) : b.restrict 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.restrict_eq_restrict_iff {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} : s.restrict f₁ = s.restrict f₂ ↔ EqOn f₁ f₂ s

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_restrict {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : ∀ (x : ↑s), f ↑x ∈ t) : codRestrict (s.restrict f) t h = MapsTo.restrict f s t ⋯

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.restrict f) t ⋯

Reverse of Set.codRestrict_restrict.

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.restrict 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.restrict f)

theorem Set.InjOn.injective {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} : InjOn f s → Function.Injective (s.restrict 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.restrict 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