Documentation

Mathlib.Data.Set.Restrict

Restrict the domain of a function to a set #

Main definitions #

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
    Instances For
      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 α) :
      @[simp]
      theorem Set.restrict_id {α : Type u_1} (s : Set α) :
      @[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 : α) → asβ) :
      (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 : α) → asβ) :
      (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)] :
      @[simp]
      theorem Set.restrict_piecewise_compl {α : Type u_1} {β : Type u_2} (f g : αβ) (s : Set α) [(x : α) → Decidable (x s)] :
      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' : βγ) :
      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
        Instances For
          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) :
          theorem Set.restrict₂_comp_restrict₂ {α : Type u_1} {π : αType u_6} {s t u : Set α} (hst : s t) (htu : t u) :
          theorem Set.range_extend_subset {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ) (g : αγ) (g' : βγ) :
          theorem Set.range_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ} (hf : Function.Injective f) (g : αγ) (g' : βγ) :
          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
            Instances For
              @[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) :
              theorem Function.Injective.codRestrict {α : Type u_1} {ι : Sort u_5} {f : ια} {s : Set α} (h : ∀ (x : ι), f x s) :

              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) :
              @[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) :

              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) :
              theorem Set.MapsTo.range_restrict {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (t : Set β) (h : MapsTo f s t) :
              theorem Set.mapsTo_iff_exists_map_subtype {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} :
              MapsTo f s t ∃ (g : st), ∀ (x : s), f x = (g x)
              theorem Set.surjective_mapsTo_image_restrict {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :

              Restriction onto preimage #

              theorem Set.image_restrictPreimage {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) (f : αβ) :
              theorem Set.range_restrictPreimage {α : Type u_1} {β : Type u_2} (t : Set β) (f : αβ) :
              @[simp]
              theorem Set.restrictPreimage_mk {α : Type u_1} {β : Type u_2} (t : Set β) {f : αβ} {a : α} (h : a f ⁻¹' t) :
              theorem Set.image_val_preimage_restrictPreimage {α : Type u_1} {β : Type u_2} (t : Set β) {f : αβ} {u : Set t} :
              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) :
              theorem Set.restrictPreimage_surjective {α : Type u_1} {β : Type u_2} (t : Set β) {f : αβ} (hf : Function.Surjective f) :
              theorem Set.restrictPreimage_bijective {α : Type u_1} {β : Type u_2} (t : Set β) {f : αβ} (hf : Function.Bijective f) :
              theorem Function.Injective.restrictPreimage {α : Type u_1} {β : Type u_2} (t : Set β) {f : αβ} (hf : Injective f) :

              Alias of Set.restrictPreimage_injective.

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

              Alias of Set.restrictPreimage_surjective.

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

              Alias of Set.restrictPreimage_bijective.

              Injectivity on a set #

              theorem Set.injOn_iff_injective {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} :
              theorem Set.InjOn.injective {α : Type u_1} {β : Type u_2} {s : Set α} {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) :

              Surjectivity on a set #

              theorem Set.surjOn_iff_surjective {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} :
              @[simp]
              theorem Set.MapsTo.restrict_surjective_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : MapsTo f s t) :