Documentation

Mathlib.Data.Set.Function

Functions over sets #

Main definitions #

Predicate #

Functions #

Restrict #

def Set.restrict {α : Type u_1} {π : αType u_5} (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_eq {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
    Set.restrict s f = f Subtype.val
    @[simp]
    theorem Set.restrict_apply {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (x : s) :
    Set.restrict s f x = f x
    theorem Set.restrict_eq_iff {α : Type u_1} {π : αType u_5} {f : (a : α) → π a} {s : Set α} {g : (a : s) → π a} :
    Set.restrict s f = g ∀ (a : α) (ha : a s), f a = g { val := a, property := ha }
    theorem Set.eq_restrict_iff {α : Type u_1} {π : αType u_5} {s : Set α} {f : (a : s) → π a} {g : (a : α) → π a} :
    f = Set.restrict s g ∀ (a : α) (ha : a s), f { val := a, property := ha } = g a
    @[simp]
    theorem Set.range_restrict {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
    theorem Set.image_restrict {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (t : Set α) :
    Set.restrict s 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β) :
    (Set.restrict s fun a => if h : a s then f a h else g a h) = fun a => f a (_ : a s)
    @[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β) :
    (Set.restrict s fun a => if h : a s then f a h else g a h) = fun a => g a (_ : a s)
    @[simp]
    theorem Set.restrict_ite {α : Type u_1} {β : Type u_2} (f : αβ) (g : αβ) (s : Set α) [(x : α) → Decidable (x s)] :
    (Set.restrict s fun a => if a s then f a else g a) = Set.restrict s f
    @[simp]
    theorem Set.restrict_ite_compl {α : Type u_1} {β : Type u_2} (f : αβ) (g : αβ) (s : Set α) [(x : α) → Decidable (x s)] :
    (Set.restrict s fun a => if a s then f a else g a) = Set.restrict s 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' : βγ) :
    Set.restrict (Set.range f) (Function.extend f g g') = fun x => g (Exists.choose (_ : x Set.range f))
    @[simp]
    theorem Set.restrict_extend_compl_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ) (g : αγ) (g' : βγ) :
    Set.restrict (Set.range f) (Function.extend f g g') = g' Subtype.val
    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_4} (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_4} (f : ια) (s : Set α) (h : ∀ (x : ι), f x s) (x : ι) :
      ↑(Set.codRestrict f s h x) = f x
      @[simp]
      theorem Set.restrict_comp_codRestrict {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ια} {g : αβ} {b : Set α} (h : ∀ (x : ι), f x b) :
      @[simp]
      theorem Set.injective_codRestrict {α : Type u_1} {ι : Sort u_4} {f : ια} {s : Set α} (h : ∀ (x : ι), f x s) :
      theorem Function.Injective.codRestrict {α : Type u_1} {ι : Sort u_4} {f : ια} {s : Set α} (h : ∀ (x : ι), f x s) :

      Alias of the reverse direction of Set.injective_codRestrict.

      Equality on a set #

      def Set.EqOn {α : Type u_1} {β : Type u_2} (f₁ : αβ) (f₂ : αβ) (s : Set α) :

      Two functions f₁ f₂ : α → β are equal on s if f₁ x = f₂ x for all x ∈ s.

      Equations
      • Set.EqOn f₁ f₂ s = ∀ ⦃x : α⦄, x sf₁ x = f₂ x
      Instances For
        @[simp]
        theorem Set.eqOn_empty {α : Type u_1} {β : Type u_2} (f₁ : αβ) (f₂ : αβ) :
        Set.EqOn f₁ f₂
        @[simp]
        theorem Set.eqOn_singleton {α : Type u_1} {β : Type u_2} {f₁ : αβ} {f₂ : αβ} {a : α} :
        Set.EqOn f₁ f₂ {a} f₁ a = f₂ a
        @[simp]
        theorem Set.restrict_eq_restrict_iff {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} :
        Set.restrict s f₁ = Set.restrict s f₂ Set.EqOn f₁ f₂ s
        theorem Set.EqOn.symm {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} (h : Set.EqOn f₁ f₂ s) :
        Set.EqOn f₂ f₁ s
        theorem Set.eqOn_comm {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} :
        Set.EqOn f₁ f₂ s Set.EqOn f₂ f₁ s
        theorem Set.eqOn_refl {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
        Set.EqOn f f s
        theorem Set.EqOn.trans {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} {f₃ : αβ} (h₁ : Set.EqOn f₁ f₂ s) (h₂ : Set.EqOn f₂ f₃ s) :
        Set.EqOn f₁ f₃ s
        theorem Set.EqOn.image_eq {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} (heq : Set.EqOn f₁ f₂ s) :
        f₁ '' s = f₂ '' s
        theorem Set.EqOn.inter_preimage_eq {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} (heq : Set.EqOn f₁ f₂ s) (t : Set β) :
        s f₁ ⁻¹' t = s f₂ ⁻¹' t
        theorem Set.EqOn.mono {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {f₁ : αβ} {f₂ : αβ} (hs : s₁ s₂) (hf : Set.EqOn f₁ f₂ s₂) :
        Set.EqOn f₁ f₂ s₁
        @[simp]
        theorem Set.eqOn_union {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {f₁ : αβ} {f₂ : αβ} :
        Set.EqOn f₁ f₂ (s₁ s₂) Set.EqOn f₁ f₂ s₁ Set.EqOn f₁ f₂ s₂
        theorem Set.EqOn.union {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {f₁ : αβ} {f₂ : αβ} (h₁ : Set.EqOn f₁ f₂ s₁) (h₂ : Set.EqOn f₁ f₂ s₂) :
        Set.EqOn f₁ f₂ (s₁ s₂)
        theorem Set.EqOn.comp_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {f₁ : αβ} {f₂ : αβ} {g : βγ} (h : Set.EqOn f₁ f₂ s) :
        Set.EqOn (g f₁) (g f₂) s
        @[simp]
        theorem Set.eqOn_range {α : Type u_1} {β : Type u_2} {ι : Sort u_6} {f : ια} {g₁ : αβ} {g₂ : αβ} :
        Set.EqOn g₁ g₂ (Set.range f) g₁ f = g₂ f
        theorem Set.EqOn.comp_eq {α : Type u_1} {β : Type u_2} {ι : Sort u_6} {f : ια} {g₁ : αβ} {g₂ : αβ} :
        Set.EqOn g₁ g₂ (Set.range f)g₁ f = g₂ f

        Alias of the forward direction of Set.eqOn_range.

        Congruence lemmas #

        theorem MonotoneOn.congr {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} [Preorder α] [Preorder β] (h₁ : MonotoneOn f₁ s) (h : Set.EqOn f₁ f₂ s) :
        MonotoneOn f₂ s
        theorem AntitoneOn.congr {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} [Preorder α] [Preorder β] (h₁ : AntitoneOn f₁ s) (h : Set.EqOn f₁ f₂ s) :
        AntitoneOn f₂ s
        theorem StrictMonoOn.congr {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} [Preorder α] [Preorder β] (h₁ : StrictMonoOn f₁ s) (h : Set.EqOn f₁ f₂ s) :
        theorem StrictAntiOn.congr {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} [Preorder α] [Preorder β] (h₁ : StrictAntiOn f₁ s) (h : Set.EqOn f₁ f₂ s) :
        theorem Set.EqOn.congr_monotoneOn {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} [Preorder α] [Preorder β] (h : Set.EqOn f₁ f₂ s) :
        MonotoneOn f₁ s MonotoneOn f₂ s
        theorem Set.EqOn.congr_antitoneOn {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} [Preorder α] [Preorder β] (h : Set.EqOn f₁ f₂ s) :
        AntitoneOn f₁ s AntitoneOn f₂ s
        theorem Set.EqOn.congr_strictMonoOn {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} [Preorder α] [Preorder β] (h : Set.EqOn f₁ f₂ s) :
        theorem Set.EqOn.congr_strictAntiOn {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} [Preorder α] [Preorder β] (h : Set.EqOn f₁ f₂ s) :

        Mono lemmas #

        theorem MonotoneOn.mono {α : Type u_1} {β : Type u_2} {s : Set α} {s₂ : Set α} {f : αβ} [Preorder α] [Preorder β] (h : MonotoneOn f s) (h' : s₂ s) :
        MonotoneOn f s₂
        theorem AntitoneOn.mono {α : Type u_1} {β : Type u_2} {s : Set α} {s₂ : Set α} {f : αβ} [Preorder α] [Preorder β] (h : AntitoneOn f s) (h' : s₂ s) :
        AntitoneOn f s₂
        theorem StrictMonoOn.mono {α : Type u_1} {β : Type u_2} {s : Set α} {s₂ : Set α} {f : αβ} [Preorder α] [Preorder β] (h : StrictMonoOn f s) (h' : s₂ s) :
        theorem StrictAntiOn.mono {α : Type u_1} {β : Type u_2} {s : Set α} {s₂ : Set α} {f : αβ} [Preorder α] [Preorder β] (h : StrictAntiOn f s) (h' : s₂ s) :
        theorem MonotoneOn.monotone {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} [Preorder α] [Preorder β] (h : MonotoneOn f s) :
        Monotone (f Subtype.val)
        theorem AntitoneOn.monotone {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} [Preorder α] [Preorder β] (h : AntitoneOn f s) :
        Antitone (f Subtype.val)
        theorem StrictMonoOn.strictMono {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} [Preorder α] [Preorder β] (h : StrictMonoOn f s) :
        StrictMono (f Subtype.val)
        theorem StrictAntiOn.strictAnti {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} [Preorder α] [Preorder β] (h : StrictAntiOn f s) :
        StrictAnti (f Subtype.val)

        maps to #

        def Set.MapsTo {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (t : Set β) :

        MapsTo f a b means that the image of a is contained in b.

        Equations
        Instances For
          def Set.MapsTo.restrict {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (t : Set β) (h : Set.MapsTo f s t) :
          st

          Given a map f sending s : Set α into t : Set β, restrict domain of f to s and the codomain to t. Same as Subtype.map.

          Equations
          Instances For
            theorem Set.MapsTo.restrict_commutes {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (t : Set β) (h : Set.MapsTo f s t) :
            Subtype.val Set.MapsTo.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 : Set.MapsTo f s t) (x : s) :
            ↑(Set.MapsTo.restrict f s t h x) = f x
            @[simp]
            theorem Set.codRestrict_restrict {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : ∀ (x : s), f x t) :
            Set.codRestrict (Set.restrict s f) t h = Set.MapsTo.restrict f s t fun x hx => h { val := x, property := hx }

            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 : Set.MapsTo f s t) :
            Set.MapsTo.restrict f s t h = Set.codRestrict (Set.restrict s f) t fun x => h x (_ : x s)

            Reverse of Set.codRestrict_restrict.

            theorem Set.MapsTo.coe_restrict {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : Set.MapsTo f s t) :
            Subtype.val Set.MapsTo.restrict f s t h = Set.restrict s f
            theorem Set.MapsTo.range_restrict {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (t : Set β) (h : Set.MapsTo f s t) :
            Set.range (Set.MapsTo.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 : αβ} :
            Set.MapsTo f s t g, ∀ (x : s), f x = ↑(g x)
            theorem Set.mapsTo' {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} :
            Set.MapsTo f s t f '' s t
            theorem Set.mapsTo_prod_map_diagonal {α : Type u_1} {β : Type u_2} {f : αβ} :
            theorem Set.MapsTo.subset_preimage {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} {t : Set β} (hf : Set.MapsTo f s t) :
            s f ⁻¹' t
            @[simp]
            theorem Set.mapsTo_singleton {α : Type u_1} {β : Type u_2} {t : Set β} {f : αβ} {x : α} :
            Set.MapsTo f {x} t f x t
            theorem Set.mapsTo_empty {α : Type u_1} {β : Type u_2} (f : αβ) (t : Set β) :
            theorem Set.MapsTo.image_subset {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : Set.MapsTo f s t) :
            f '' s t
            theorem Set.MapsTo.congr {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f₁ : αβ} {f₂ : αβ} (h₁ : Set.MapsTo f₁ s t) (h : Set.EqOn f₁ f₂ s) :
            Set.MapsTo f₂ s t
            theorem Set.EqOn.comp_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : αβ} {g₁ : βγ} {g₂ : βγ} (hg : Set.EqOn g₁ g₂ t) (hf : Set.MapsTo f s t) :
            Set.EqOn (g₁ f) (g₂ f) s
            theorem Set.EqOn.mapsTo_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f₁ : αβ} {f₂ : αβ} (H : Set.EqOn f₁ f₂ s) :
            Set.MapsTo f₁ s t Set.MapsTo f₂ s t
            theorem Set.MapsTo.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {p : Set γ} {f : αβ} {g : βγ} (h₁ : Set.MapsTo g t p) (h₂ : Set.MapsTo f s t) :
            Set.MapsTo (g f) s p
            theorem Set.mapsTo_id {α : Type u_1} (s : Set α) :
            Set.MapsTo id s s
            theorem Set.MapsTo.iterate {α : Type u_1} {f : αα} {s : Set α} (h : Set.MapsTo f s s) (n : ) :
            theorem Set.MapsTo.iterate_restrict {α : Type u_1} {f : αα} {s : Set α} (h : Set.MapsTo f s s) (n : ) :
            theorem Set.mapsTo_of_subsingleton' {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} [Subsingleton β] (f : αβ) (h : Set.Nonempty sSet.Nonempty t) :
            theorem Set.mapsTo_of_subsingleton {α : Type u_1} [Subsingleton α] (f : αα) (s : Set α) :
            theorem Set.MapsTo.mono {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} {f : αβ} (hf : Set.MapsTo f s₁ t₁) (hs : s₂ s₁) (ht : t₁ t₂) :
            Set.MapsTo f s₂ t₂
            theorem Set.MapsTo.mono_left {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {t : Set β} {f : αβ} (hf : Set.MapsTo f s₁ t) (hs : s₂ s₁) :
            Set.MapsTo f s₂ t
            theorem Set.MapsTo.mono_right {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ : Set β} {t₂ : Set β} {f : αβ} (hf : Set.MapsTo f s t₁) (ht : t₁ t₂) :
            Set.MapsTo f s t₂
            theorem Set.MapsTo.union_union {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} {f : αβ} (h₁ : Set.MapsTo f s₁ t₁) (h₂ : Set.MapsTo f s₂ t₂) :
            Set.MapsTo f (s₁ s₂) (t₁ t₂)
            theorem Set.MapsTo.union {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {t : Set β} {f : αβ} (h₁ : Set.MapsTo f s₁ t) (h₂ : Set.MapsTo f s₂ t) :
            Set.MapsTo f (s₁ s₂) t
            @[simp]
            theorem Set.mapsTo_union {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {t : Set β} {f : αβ} :
            Set.MapsTo f (s₁ s₂) t Set.MapsTo f s₁ t Set.MapsTo f s₂ t
            theorem Set.MapsTo.inter {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ : Set β} {t₂ : Set β} {f : αβ} (h₁ : Set.MapsTo f s t₁) (h₂ : Set.MapsTo f s t₂) :
            Set.MapsTo f s (t₁ t₂)
            theorem Set.MapsTo.inter_inter {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} {f : αβ} (h₁ : Set.MapsTo f s₁ t₁) (h₂ : Set.MapsTo f s₂ t₂) :
            Set.MapsTo f (s₁ s₂) (t₁ t₂)
            @[simp]
            theorem Set.mapsTo_inter {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ : Set β} {t₂ : Set β} {f : αβ} :
            Set.MapsTo f s (t₁ t₂) Set.MapsTo f s t₁ Set.MapsTo f s t₂
            theorem Set.mapsTo_univ {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
            Set.MapsTo f s Set.univ
            theorem Set.mapsTo_image {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
            Set.MapsTo f s (f '' s)
            theorem Set.mapsTo_preimage {α : Type u_1} {β : Type u_2} (f : αβ) (t : Set β) :
            Set.MapsTo f (f ⁻¹' t) t
            theorem Set.mapsTo_range {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
            @[simp]
            theorem Set.maps_image_to {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ) (g : γα) (s : Set γ) (t : Set β) :
            Set.MapsTo f (g '' s) t Set.MapsTo (f g) s t
            theorem Set.MapsTo.comp_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : αβ} (g : βγ) (hf : Set.MapsTo f s t) :
            Set.MapsTo (g f) s (g '' t)
            theorem Set.MapsTo.comp_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : βγ} {s : Set β} {t : Set γ} (hg : Set.MapsTo g s t) (f : αβ) :
            Set.MapsTo (g f) (f ⁻¹' s) t
            @[simp]
            theorem Set.maps_univ_to {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set β) :
            Set.MapsTo f Set.univ s ∀ (a : α), f a s
            @[simp]
            theorem Set.maps_range_to {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ) (g : γα) (s : Set β) :
            Set.MapsTo f (Set.range g) s Set.MapsTo (f g) Set.univ s
            theorem Set.surjective_mapsTo_image_restrict {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
            theorem Set.MapsTo.mem_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : Set.MapsTo f s t) (hc : Set.MapsTo f s t) {x : α} :
            f x t x s

            Restriction onto preimage #

            @[simp]
            theorem Set.restrictPreimage_coe {α : Type u_1} {β : Type u_2} (t : Set β) (f : αβ) :
            ∀ (a : ↑(f ⁻¹' t)), ↑(Set.restrictPreimage t f a) = f a
            def Set.restrictPreimage {α : Type u_1} {β : Type u_2} (t : Set β) (f : αβ) :
            ↑(f ⁻¹' t)t

            The restriction of a function onto the preimage of a set.

            Equations
            Instances For
              theorem Set.range_restrictPreimage {α : Type u_1} {β : Type u_2} (t : Set β) (f : αβ) :
              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) :

              Injectivity on a set #

              def Set.InjOn {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :

              f is injective on a if the restriction of f to a is injective.

              Equations
              • Set.InjOn f s = ∀ ⦃x₁ : α⦄, x₁ s∀ ⦃x₂ : α⦄, x₂ sf x₁ = f x₂x₁ = x₂
              Instances For
                theorem Set.Subsingleton.injOn {α : Type u_1} {β : Type u_2} {s : Set α} (hs : Set.Subsingleton s) (f : αβ) :
                @[simp]
                theorem Set.injOn_empty {α : Type u_1} {β : Type u_2} (f : αβ) :
                @[simp]
                theorem Set.injOn_singleton {α : Type u_1} {β : Type u_2} (f : αβ) (a : α) :
                Set.InjOn f {a}
                theorem Set.InjOn.eq_iff {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {x : α} {y : α} (h : Set.InjOn f s) (hx : x s) (hy : y s) :
                f x = f y x = y
                theorem Set.InjOn.ne_iff {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {x : α} {y : α} (h : Set.InjOn f s) (hx : x s) (hy : y s) :
                f x f y x y
                theorem Set.InjOn.ne {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {x : α} {y : α} (h : Set.InjOn f s) (hx : x s) (hy : y s) :
                x yf x f y

                Alias of the reverse direction of Set.InjOn.ne_iff.

                theorem Set.InjOn.congr {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} (h₁ : Set.InjOn f₁ s) (h : Set.EqOn f₁ f₂ s) :
                Set.InjOn f₂ s
                theorem Set.EqOn.injOn_iff {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} (H : Set.EqOn f₁ f₂ s) :
                Set.InjOn f₁ s Set.InjOn f₂ s
                theorem Set.InjOn.mono {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {f : αβ} (h : s₁ s₂) (ht : Set.InjOn f s₂) :
                Set.InjOn f s₁
                theorem Set.injOn_union {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {f : αβ} (h : Disjoint s₁ s₂) :
                Set.InjOn f (s₁ s₂) Set.InjOn f s₁ Set.InjOn f s₂ ∀ (x : α), x s₁∀ (y : α), y s₂f x f y
                theorem Set.injOn_insert {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} {a : α} (has : ¬a s) :
                Set.InjOn f (insert a s) Set.InjOn f s ¬f a f '' s
                theorem Set.injective_iff_injOn_univ {α : Type u_1} {β : Type u_2} {f : αβ} :
                theorem Set.injOn_of_injective {α : Type u_1} {β : Type u_2} {f : αβ} (h : Function.Injective f) (s : Set α) :
                theorem Function.Injective.injOn {α : Type u_1} {β : Type u_2} {f : αβ} (h : Function.Injective f) (s : Set α) :

                Alias of Set.injOn_of_injective.

                theorem Set.injOn_subtype_val {γ : Type u_3} {p : Set γ} {s : Set { x // p x }} :
                Set.InjOn Subtype.val s
                theorem Set.injOn_id {α : Type u_1} (s : Set α) :
                theorem Set.InjOn.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : αβ} {g : βγ} (hg : Set.InjOn g t) (hf : Set.InjOn f s) (h : Set.MapsTo f s t) :
                Set.InjOn (g f) s
                theorem Set.InjOn.iterate {α : Type u_1} {f : αα} {s : Set α} (h : Set.InjOn f s) (hf : Set.MapsTo f s s) (n : ) :
                theorem Set.injOn_of_subsingleton {α : Type u_1} {β : Type u_2} [Subsingleton α] (f : αβ) (s : Set α) :
                theorem Function.Injective.injOn_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ} {g : βγ} (h : Function.Injective (g f)) :
                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 : Set.MapsTo f s t) :
                theorem Set.exists_injOn_iff_injective {α : Type u_1} {β : Type u_2} {s : Set α} [Nonempty β] :
                (f, Set.InjOn f s) f, Function.Injective f
                theorem Set.injOn_preimage {α : Type u_1} {β : Type u_2} {f : αβ} {B : Set (Set β)} (hB : B 𝒫 Set.range f) :
                theorem Set.InjOn.mem_of_mem_image {α : Type u_1} {β : Type u_2} {s : Set α} {s₁ : Set α} {f : αβ} {x : α} (hf : Set.InjOn f s) (hs : s₁ s) (h : x s) (h₁ : f x f '' s₁) :
                x s₁
                theorem Set.InjOn.mem_image_iff {α : Type u_1} {β : Type u_2} {s : Set α} {s₁ : Set α} {f : αβ} {x : α} (hf : Set.InjOn f s) (hs : s₁ s) (hx : x s) :
                f x f '' s₁ x s₁
                theorem Set.InjOn.preimage_image_inter {α : Type u_1} {β : Type u_2} {s : Set α} {s₁ : Set α} {f : αβ} (hf : Set.InjOn f s) (hs : s₁ s) :
                f ⁻¹' (f '' s₁) s = s₁
                theorem Set.EqOn.cancel_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f₁ : αβ} {f₂ : αβ} {g : βγ} (h : Set.EqOn (g f₁) (g f₂) s) (hg : Set.InjOn g t) (hf₁ : Set.MapsTo f₁ s t) (hf₂ : Set.MapsTo f₂ s t) :
                Set.EqOn f₁ f₂ s
                theorem Set.InjOn.cancel_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f₁ : αβ} {f₂ : αβ} {g : βγ} (hg : Set.InjOn g t) (hf₁ : Set.MapsTo f₁ s t) (hf₂ : Set.MapsTo f₂ s t) :
                Set.EqOn (g f₁) (g f₂) s Set.EqOn f₁ f₂ s
                theorem Set.InjOn.image_inter {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} {t : Set α} {u : Set α} (hf : Set.InjOn f u) (hs : s u) (ht : t u) :
                f '' (s t) = f '' s f '' t
                theorem Disjoint.image {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set α} {u : Set α} {f : αβ} (h : Disjoint s t) (hf : Set.InjOn f u) (hs : s u) (ht : t u) :
                Disjoint (f '' s) (f '' t)

                Surjectivity on a set #

                def Set.SurjOn {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (t : Set β) :

                f is surjective from a to b if b is contained in the image of a.

                Equations
                Instances For
                  theorem Set.SurjOn.subset_range {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : Set.SurjOn f s t) :
                  theorem Set.surjOn_iff_exists_map_subtype {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} :
                  Set.SurjOn f s t t' g, t t' Function.Surjective g ∀ (x : s), f x = ↑(g x)
                  theorem Set.surjOn_empty {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
                  @[simp]
                  theorem Set.surjOn_singleton {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {b : β} :
                  Set.SurjOn f s {b} b f '' s
                  theorem Set.surjOn_image {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
                  Set.SurjOn f s (f '' s)
                  theorem Set.SurjOn.comap_nonempty {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : Set.SurjOn f s t) (ht : Set.Nonempty t) :
                  theorem Set.SurjOn.congr {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f₁ : αβ} {f₂ : αβ} (h : Set.SurjOn f₁ s t) (H : Set.EqOn f₁ f₂ s) :
                  Set.SurjOn f₂ s t
                  theorem Set.EqOn.surjOn_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f₁ : αβ} {f₂ : αβ} (h : Set.EqOn f₁ f₂ s) :
                  Set.SurjOn f₁ s t Set.SurjOn f₂ s t
                  theorem Set.SurjOn.mono {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} {f : αβ} (hs : s₁ s₂) (ht : t₁ t₂) (hf : Set.SurjOn f s₁ t₂) :
                  Set.SurjOn f s₂ t₁
                  theorem Set.SurjOn.union {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ : Set β} {t₂ : Set β} {f : αβ} (h₁ : Set.SurjOn f s t₁) (h₂ : Set.SurjOn f s t₂) :
                  Set.SurjOn f s (t₁ t₂)
                  theorem Set.SurjOn.union_union {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} {f : αβ} (h₁ : Set.SurjOn f s₁ t₁) (h₂ : Set.SurjOn f s₂ t₂) :
                  Set.SurjOn f (s₁ s₂) (t₁ t₂)
                  theorem Set.SurjOn.inter_inter {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} {f : αβ} (h₁ : Set.SurjOn f s₁ t₁) (h₂ : Set.SurjOn f s₂ t₂) (h : Set.InjOn f (s₁ s₂)) :
                  Set.SurjOn f (s₁ s₂) (t₁ t₂)
                  theorem Set.SurjOn.inter {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {t : Set β} {f : αβ} (h₁ : Set.SurjOn f s₁ t) (h₂ : Set.SurjOn f s₂ t) (h : Set.InjOn f (s₁ s₂)) :
                  Set.SurjOn f (s₁ s₂) t
                  theorem Set.surjOn_id {α : Type u_1} (s : Set α) :
                  Set.SurjOn id s s
                  theorem Set.SurjOn.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {p : Set γ} {f : αβ} {g : βγ} (hg : Set.SurjOn g t p) (hf : Set.SurjOn f s t) :
                  Set.SurjOn (g f) s p
                  theorem Set.SurjOn.iterate {α : Type u_1} {f : αα} {s : Set α} (h : Set.SurjOn f s s) (n : ) :
                  theorem Set.SurjOn.comp_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : αβ} (hf : Set.SurjOn f s t) (g : βγ) :
                  Set.SurjOn (g f) s (g '' t)
                  theorem Set.SurjOn.comp_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ} {g : βγ} {s : Set β} {t : Set γ} (hf : Function.Surjective f) (hg : Set.SurjOn g s t) :
                  Set.SurjOn (g f) (f ⁻¹' s) t
                  theorem Set.surjOn_of_subsingleton' {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} [Subsingleton β] (f : αβ) (h : Set.Nonempty tSet.Nonempty s) :
                  theorem Set.surjOn_of_subsingleton {α : Type u_1} [Subsingleton α] (f : αα) (s : Set α) :
                  theorem Set.surjective_iff_surjOn_univ {α : Type u_1} {β : Type u_2} {f : αβ} :
                  Function.Surjective f Set.SurjOn f Set.univ Set.univ
                  theorem Set.surjOn_iff_surjective {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} :
                  theorem Set.SurjOn.image_eq_of_mapsTo {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h₁ : Set.SurjOn f s t) (h₂ : Set.MapsTo f s t) :
                  f '' s = t
                  theorem Set.image_eq_iff_surjOn_mapsTo {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} :
                  f '' s = t Set.SurjOn f s t Set.MapsTo f s t
                  theorem Set.SurjOn.mapsTo_compl {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : Set.SurjOn f s t) (h' : Function.Injective f) :
                  theorem Set.MapsTo.surjOn_compl {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : Set.MapsTo f s t) (h' : Function.Surjective f) :
                  theorem Set.EqOn.cancel_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : αβ} {g₁ : βγ} {g₂ : βγ} (hf : Set.EqOn (g₁ f) (g₂ f) s) (hf' : Set.SurjOn f s t) :
                  Set.EqOn g₁ g₂ t
                  theorem Set.SurjOn.cancel_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : αβ} {g₁ : βγ} {g₂ : βγ} (hf : Set.SurjOn f s t) (hf' : Set.MapsTo f s t) :
                  Set.EqOn (g₁ f) (g₂ f) s Set.EqOn g₁ g₂ t
                  theorem Set.eqOn_comp_right_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {f : αβ} {g₁ : βγ} {g₂ : βγ} :
                  Set.EqOn (g₁ f) (g₂ f) s Set.EqOn g₁ g₂ (f '' s)

                  Bijectivity #

                  def Set.BijOn {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (t : Set β) :

                  f is bijective from s to t if f is injective on s and f '' s = t.

                  Equations
                  Instances For
                    theorem Set.BijOn.mapsTo {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : Set.BijOn f s t) :
                    theorem Set.BijOn.injOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : Set.BijOn f s t) :
                    theorem Set.BijOn.surjOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : Set.BijOn f s t) :
                    theorem Set.BijOn.mk {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h₁ : Set.MapsTo f s t) (h₂ : Set.InjOn f s) (h₃ : Set.SurjOn f s t) :
                    Set.BijOn f s t
                    theorem Set.bijOn_empty {α : Type u_1} {β : Type u_2} (f : αβ) :
                    @[simp]
                    theorem Set.bijOn_singleton {α : Type u_1} {β : Type u_2} {f : αβ} {a : α} {b : β} :
                    Set.BijOn f {a} {b} f a = b
                    theorem Set.BijOn.inter_mapsTo {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} {f : αβ} (h₁ : Set.BijOn f s₁ t₁) (h₂ : Set.MapsTo f s₂ t₂) (h₃ : s₁ f ⁻¹' t₂ s₂) :
                    Set.BijOn f (s₁ s₂) (t₁ t₂)
                    theorem Set.MapsTo.inter_bijOn {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} {f : αβ} (h₁ : Set.MapsTo f s₁ t₁) (h₂ : Set.BijOn f s₂ t₂) (h₃ : s₂ f ⁻¹' t₁ s₁) :
                    Set.BijOn f (s₁ s₂) (t₁ t₂)
                    theorem Set.BijOn.inter {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} {f : αβ} (h₁ : Set.BijOn f s₁ t₁) (h₂ : Set.BijOn f s₂ t₂) (h : Set.InjOn f (s₁ s₂)) :
                    Set.BijOn f (s₁ s₂) (t₁ t₂)
                    theorem Set.BijOn.union {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} {f : αβ} (h₁ : Set.BijOn f s₁ t₁) (h₂ : Set.BijOn f s₂ t₂) (h : Set.InjOn f (s₁ s₂)) :
                    Set.BijOn f (s₁ s₂) (t₁ t₂)
                    theorem Set.BijOn.subset_range {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : Set.BijOn f s t) :
                    theorem Set.InjOn.bijOn_image {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} (h : Set.InjOn f s) :
                    Set.BijOn f s (f '' s)
                    theorem Set.BijOn.congr {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f₁ : αβ} {f₂ : αβ} (h₁ : Set.BijOn f₁ s t) (h : Set.EqOn f₁ f₂ s) :
                    Set.BijOn f₂ s t
                    theorem Set.EqOn.bijOn_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f₁ : αβ} {f₂ : αβ} (H : Set.EqOn f₁ f₂ s) :
                    Set.BijOn f₁ s t Set.BijOn f₂ s t
                    theorem Set.BijOn.image_eq {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : Set.BijOn f s t) :
                    f '' s = t
                    theorem Set.bijOn_id {α : Type u_1} (s : Set α) :
                    Set.BijOn id s s
                    theorem Set.BijOn.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {p : Set γ} {f : αβ} {g : βγ} (hg : Set.BijOn g t p) (hf : Set.BijOn f s t) :
                    Set.BijOn (g f) s p
                    theorem Set.BijOn.iterate {α : Type u_1} {f : αα} {s : Set α} (h : Set.BijOn f s s) (n : ) :
                    theorem Set.bijOn_of_subsingleton' {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} [Subsingleton α] [Subsingleton β] (f : αβ) (h : Set.Nonempty s Set.Nonempty t) :
                    Set.BijOn f s t
                    theorem Set.bijOn_of_subsingleton {α : Type u_1} [Subsingleton α] (f : αα) (s : Set α) :
                    Set.BijOn f s s
                    theorem Set.BijOn.bijective {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : Set.BijOn f s t) :
                    theorem Set.bijective_iff_bijOn_univ {α : Type u_1} {β : Type u_2} {f : αβ} :
                    Function.Bijective f Set.BijOn f Set.univ Set.univ
                    theorem Function.Bijective.bijOn_univ {α : Type u_1} {β : Type u_2} {f : αβ} :
                    Function.Bijective fSet.BijOn f Set.univ Set.univ

                    Alias of the forward direction of Set.bijective_iff_bijOn_univ.

                    theorem Set.BijOn.compl {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (hst : Set.BijOn f s t) (hf : Function.Bijective f) :

                    left inverse #

                    def Set.LeftInvOn {α : Type u_1} {β : Type u_2} (f' : βα) (f : αβ) (s : Set α) :

                    g is a left inverse to f on a means that g (f x) = x for all x ∈ a.

                    Equations
                    Instances For
                      theorem Set.LeftInvOn.eqOn {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {f' : βα} (h : Set.LeftInvOn f' f s) :
                      Set.EqOn (f' f) id s
                      theorem Set.LeftInvOn.eq {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {f' : βα} (h : Set.LeftInvOn f' f s) {x : α} (hx : x s) :
                      f' (f x) = x
                      theorem Set.LeftInvOn.congr_left {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {f₁' : βα} {f₂' : βα} (h₁ : Set.LeftInvOn f₁' f s) {t : Set β} (h₁' : Set.MapsTo f s t) (heq : Set.EqOn f₁' f₂' t) :
                      Set.LeftInvOn f₂' f s
                      theorem Set.LeftInvOn.congr_right {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} {f₁' : βα} (h₁ : Set.LeftInvOn f₁' f₁ s) (heq : Set.EqOn f₁ f₂ s) :
                      Set.LeftInvOn f₁' f₂ s
                      theorem Set.LeftInvOn.injOn {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {f₁' : βα} (h : Set.LeftInvOn f₁' f s) :
                      theorem Set.LeftInvOn.surjOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {f' : βα} (h : Set.LeftInvOn f' f s) (hf : Set.MapsTo f s t) :
                      Set.SurjOn f' t s
                      theorem Set.LeftInvOn.mapsTo {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {f' : βα} (h : Set.LeftInvOn f' f s) (hf : Set.SurjOn f s t) :
                      Set.MapsTo f' t s
                      theorem Set.leftInvOn_id {α : Type u_1} (s : Set α) :
                      theorem Set.LeftInvOn.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : αβ} {g : βγ} {f' : βα} {g' : γβ} (hf' : Set.LeftInvOn f' f s) (hg' : Set.LeftInvOn g' g t) (hf : Set.MapsTo f s t) :
                      Set.LeftInvOn (f' g') (g f) s
                      theorem Set.LeftInvOn.mono {α : Type u_1} {β : Type u_2} {s : Set α} {s₁ : Set α} {f : αβ} {f' : βα} (hf : Set.LeftInvOn f' f s) (ht : s₁ s) :
                      Set.LeftInvOn f' f s₁
                      theorem Set.LeftInvOn.image_inter' {α : Type u_1} {β : Type u_2} {s : Set α} {s₁ : Set α} {f : αβ} {f' : βα} (hf : Set.LeftInvOn f' f s) :
                      f '' (s₁ s) = f' ⁻¹' s₁ f '' s
                      theorem Set.LeftInvOn.image_inter {α : Type u_1} {β : Type u_2} {s : Set α} {s₁ : Set α} {f : αβ} {f' : βα} (hf : Set.LeftInvOn f' f s) :
                      f '' (s₁ s) = f' ⁻¹' (s₁ s) f '' s
                      theorem Set.LeftInvOn.image_image {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {f' : βα} (hf : Set.LeftInvOn f' f s) :
                      f' '' (f '' s) = s
                      theorem Set.LeftInvOn.image_image' {α : Type u_1} {β : Type u_2} {s : Set α} {s₁ : Set α} {f : αβ} {f' : βα} (hf : Set.LeftInvOn f' f s) (hs : s₁ s) :
                      f' '' (f '' s₁) = s₁

                      Right inverse #

                      @[reducible]
                      def Set.RightInvOn {α : Type u_1} {β : Type u_2} (f' : βα) (f : αβ) (t : Set β) :

                      g is a right inverse to f on b if f (g x) = x for all x ∈ b.

                      Equations
                      Instances For
                        theorem Set.RightInvOn.eqOn {α : Type u_1} {β : Type u_2} {t : Set β} {f : αβ} {f' : βα} (h : Set.RightInvOn f' f t) :
                        Set.EqOn (f f') id t
                        theorem Set.RightInvOn.eq {α : Type u_1} {β : Type u_2} {t : Set β} {f : αβ} {f' : βα} (h : Set.RightInvOn f' f t) {y : β} (hy : y t) :
                        f (f' y) = y
                        theorem Set.LeftInvOn.rightInvOn_image {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {f' : βα} (h : Set.LeftInvOn f' f s) :
                        Set.RightInvOn f' f (f '' s)
                        theorem Set.RightInvOn.congr_left {α : Type u_1} {β : Type u_2} {t : Set β} {f : αβ} {f₁' : βα} {f₂' : βα} (h₁ : Set.RightInvOn f₁' f t) (heq : Set.EqOn f₁' f₂' t) :
                        Set.RightInvOn f₂' f t
                        theorem Set.RightInvOn.congr_right {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f₁ : αβ} {f₂ : αβ} {f' : βα} (h₁ : Set.RightInvOn f' f₁ t) (hg : Set.MapsTo f' t s) (heq : Set.EqOn f₁ f₂ s) :
                        Set.RightInvOn f' f₂ t
                        theorem Set.RightInvOn.surjOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {f' : βα} (hf : Set.RightInvOn f' f t) (hf' : Set.MapsTo f' t s) :
                        theorem Set.RightInvOn.mapsTo {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {f' : βα} (h : Set.RightInvOn f' f t) (hf : Set.SurjOn f' t s) :
                        theorem Set.rightInvOn_id {α : Type u_1} (s : Set α) :
                        theorem Set.RightInvOn.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Set β} {p : Set γ} {f : αβ} {g : βγ} {f' : βα} {g' : γβ} (hf : Set.RightInvOn f' f t) (hg : Set.RightInvOn g' g p) (g'pt : Set.MapsTo g' p t) :
                        Set.RightInvOn (f' g') (g f) p
                        theorem Set.RightInvOn.mono {α : Type u_1} {β : Type u_2} {t : Set β} {t₁ : Set β} {f : αβ} {f' : βα} (hf : Set.RightInvOn f' f t) (ht : t₁ t) :
                        Set.RightInvOn f' f t₁
                        theorem Set.InjOn.rightInvOn_of_leftInvOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {f' : βα} (hf : Set.InjOn f s) (hf' : Set.LeftInvOn f f' t) (h₁ : Set.MapsTo f s t) (h₂ : Set.MapsTo f' t s) :
                        theorem Set.eqOn_of_leftInvOn_of_rightInvOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {f₁' : βα} {f₂' : βα} (h₁ : Set.LeftInvOn f₁' f s) (h₂ : Set.RightInvOn f₂' f t) (h : Set.MapsTo f₂' t s) :
                        Set.EqOn f₁' f₂' t
                        theorem Set.SurjOn.leftInvOn_of_rightInvOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {f' : βα} (hf : Set.SurjOn f s t) (hf' : Set.RightInvOn f f' s) :

                        Two-side inverses #

                        def Set.InvOn {α : Type u_1} {β : Type u_2} (g : βα) (f : αβ) (s : Set α) (t : Set β) :

                        g is an inverse to f viewed as a map from a to b

                        Equations
                        Instances For
                          theorem Set.invOn_id {α : Type u_1} (s : Set α) :
                          Set.InvOn id id s s
                          theorem Set.InvOn.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {p : Set γ} {f : αβ} {g : βγ} {f' : βα} {g' : γβ} (hf : Set.InvOn f' f s t) (hg : Set.InvOn g' g t p) (fst : Set.MapsTo f s t) (g'pt : Set.MapsTo g' p t) :
                          Set.InvOn (f' g') (g f) s p
                          theorem Set.InvOn.symm {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {f' : βα} (h : Set.InvOn f' f s t) :
                          Set.InvOn f f' t s
                          theorem Set.InvOn.mono {α : Type u_1} {β : Type u_2} {s : Set α} {s₁ : Set α} {t : Set β} {t₁ : Set β} {f : αβ} {f' : βα} (h : Set.InvOn f' f s t) (hs : s₁ s) (ht : t₁ t) :
                          Set.InvOn f' f s₁ t₁
                          theorem Set.InvOn.bijOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {f' : βα} (h : Set.InvOn f' f s t) (hf : Set.MapsTo f s t) (hf' : Set.MapsTo f' t s) :
                          Set.BijOn f s t

                          If functions f' and f are inverse on s and t, f maps s into t, and f' maps t into s, then f is a bijection between s and t. The mapsTo arguments can be deduced from surjOn statements using LeftInvOn.mapsTo and RightInvOn.mapsTo.

                          invFunOn is a left/right inverse #

                          noncomputable def Function.invFunOn {α : Type u_1} {β : Type u_2} [Nonempty α] (f : αβ) (s : Set α) (b : β) :
                          α

                          Construct the inverse for a function f on domain s. This function is a right inverse of f on f '' s. For a computable version, see Function.Injective.inv_of_mem_range.

                          Equations
                          Instances For
                            theorem Function.invFunOn_pos {α : Type u_1} {β : Type u_2} [Nonempty α] {s : Set α} {f : αβ} {b : β} (h : a, a s f a = b) :
                            theorem Function.invFunOn_mem {α : Type u_1} {β : Type u_2} [Nonempty α] {s : Set α} {f : αβ} {b : β} (h : a, a s f a = b) :
                            theorem Function.invFunOn_eq {α : Type u_1} {β : Type u_2} [Nonempty α] {s : Set α} {f : αβ} {b : β} (h : a, a s f a = b) :
                            f (Function.invFunOn f s b) = b
                            theorem Function.invFunOn_neg {α : Type u_1} {β : Type u_2} [Nonempty α] {s : Set α} {f : αβ} {b : β} (h : ¬a, a s f a = b) :
                            @[simp]
                            theorem Function.invFunOn_apply_mem {α : Type u_1} {β : Type u_2} [Nonempty α] {s : Set α} {f : αβ} {a : α} (h : a s) :
                            theorem Function.invFunOn_apply_eq {α : Type u_1} {β : Type u_2} [Nonempty α] {s : Set α} {f : αβ} {a : α} (h : a s) :
                            f (Function.invFunOn f s (f a)) = f a
                            theorem Set.InjOn.leftInvOn_invFunOn {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} [Nonempty α] (h : Set.InjOn f s) :
                            theorem Set.InjOn.invFunOn_image {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {f : αβ} [Nonempty α] (h : Set.InjOn f s₂) (ht : s₁ s₂) :
                            Function.invFunOn f s₂ '' (f '' s₁) = s₁
                            theorem Function.leftInvOn_invFunOn_of_subset_image_image {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} [Nonempty α] (h : s Function.invFunOn f s '' (f '' s)) :
                            theorem Set.injOn_iff_invFunOn_image_image_eq_self {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} [Nonempty α] :
                            theorem Function.invFunOn_injOn_image {α : Type u_1} {β : Type u_2} [Nonempty α] (f : αβ) (s : Set α) :
                            theorem Function.invFunOn_image_image_subset {α : Type u_1} {β : Type u_2} [Nonempty α] (f : αβ) (s : Set α) :
                            theorem Set.SurjOn.rightInvOn_invFunOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} [Nonempty α] (h : Set.SurjOn f s t) :
                            theorem Set.BijOn.invOn_invFunOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} [Nonempty α] (h : Set.BijOn f s t) :
                            theorem Set.SurjOn.invOn_invFunOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} [Nonempty α] (h : Set.SurjOn f s t) :
                            theorem Set.SurjOn.mapsTo_invFunOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} [Nonempty α] (h : Set.SurjOn f s t) :
                            theorem Set.SurjOn.bijOn_subset {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} [Nonempty α] (h : Set.SurjOn f s t) :
                            theorem Set.surjOn_iff_exists_bijOn_subset {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} :
                            Set.SurjOn f s t s' x, Set.BijOn f s' t
                            theorem Set.preimage_invFun_of_mem {α : Type u_1} {β : Type u_2} [n : Nonempty α] {f : αβ} (hf : Function.Injective f) {s : Set α} (h : Classical.choice n s) :
                            theorem Set.preimage_invFun_of_not_mem {α : Type u_1} {β : Type u_2} [n : Nonempty α] {f : αβ} (hf : Function.Injective f) {s : Set α} (h : ¬Classical.choice n s) :
                            theorem Set.BijOn.symm {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {g : βα} (h : Set.InvOn f g t s) (hf : Set.BijOn f s t) :
                            Set.BijOn g t s
                            theorem Set.bijOn_comm {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {g : βα} (h : Set.InvOn f g t s) :
                            Set.BijOn f s t Set.BijOn g t s

                            Monotone #

                            theorem Monotone.restrict {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} (h : Monotone f) (s : Set α) :
                            theorem Monotone.codRestrict {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} (h : Monotone f) {s : Set β} (hs : ∀ (x : α), f x s) :
                            theorem Monotone.rangeFactorization {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} (h : Monotone f) :

                            Piecewise defined function #

                            @[simp]
                            theorem Set.piecewise_empty {α : Type u_1} {δ : αSort u_6} (f : (i : α) → δ i) (g : (i : α) → δ i) [(i : α) → Decidable (i )] :
                            @[simp]
                            theorem Set.piecewise_univ {α : Type u_1} {δ : αSort u_6} (f : (i : α) → δ i) (g : (i : α) → δ i) [(i : α) → Decidable (i Set.univ)] :
                            Set.piecewise Set.univ f g = f
                            theorem Set.piecewise_insert_self {α : Type u_1} {δ : αSort u_6} (s : Set α) (f : (i : α) → δ i) (g : (i : α) → δ i) {j : α} [(i : α) → Decidable (i insert j s)] :
                            Set.piecewise (insert j s) f g j = f j
                            instance Set.Compl.decidableMem {α : Type u_1} (s : Set α) [(j : α) → Decidable (j s)] (j : α) :
                            Equations
                            theorem Set.piecewise_insert {α : Type u_1} {δ : αSort u_6} (s : Set α) (f : (i : α) → δ i) (g : (i : α) → δ i) [(j : α) → Decidable (j s)] [DecidableEq α] (j : α) [(i : α) → Decidable (i insert j s)] :
                            @[simp]
                            theorem Set.piecewise_eq_of_mem {α : Type u_1} {δ : αSort u_6} (s : Set α) (f : (i : α) → δ i) (g : (i : α) → δ i) [(j : α) → Decidable (j s)] {i : α} (hi : i s) :
                            Set.piecewise s f g i = f i
                            @[simp]
                            theorem Set.piecewise_eq_of_not_mem {α : Type u_1} {δ : αSort u_6} (s : Set α) (f : (i : α) → δ i) (g : (i : α) → δ i) [(j : α) → Decidable (j s)] {i : α} (hi : ¬i s) :
                            Set.piecewise s f g i = g i
                            theorem Set.piecewise_singleton {α : Type u_1} {β : Type u_2} (x : α) [(y : α) → Decidable (y {x})] [DecidableEq α] (f : αβ) (g : αβ) :
                            Set.piecewise {x} f g = Function.update g x (f x)
                            theorem Set.piecewise_eqOn {α : Type u_1} {β : Type u_2} (s : Set α) [(j : α) → Decidable (j s)] (f : αβ) (g : αβ) :
                            theorem Set.piecewise_eqOn_compl {α : Type u_1} {β : Type u_2} (s : Set α) [(j : α) → Decidable (j s)] (f : αβ) (g : αβ) :
                            theorem Set.piecewise_le {α : Type u_1} {δ : αType u_7} [(i : α) → Preorder (δ i)] {s : Set α} [(j : α) → Decidable (j s)] {f₁ : (i : α) → δ i} {f₂ : (i : α) → δ i} {g : (i : α) → δ i} (h₁ : ∀ (i : α), i sf₁ i g i) (h₂ : ∀ (i : α), ¬i sf₂ i g i) :
                            Set.piecewise s f₁ f₂ g
                            theorem Set.le_piecewise {α : Type u_1} {δ : αType u_7} [(i : α) → Preorder (δ i)] {s : Set α} [(j : α) → Decidable (j s)] {f₁ : (i : α) → δ i} {f₂ : (i : α) → δ i} {g : (i : α) → δ i} (h₁ : ∀ (i : α), i sg i f₁ i) (h₂ : ∀ (i : α), ¬i sg i f₂ i) :
                            g Set.piecewise s f₁ f₂
                            theorem Set.piecewise_le_piecewise {α : Type u_1} {δ : αType u_7} [(i : α) → Preorder (δ i)] {s : Set α} [(j : α) → Decidable (j s)] {f₁ : (i : α) → δ i} {f₂ : (i : α) → δ i} {g₁ : (i : α) → δ i} {g₂ : (i : α) → δ i} (h₁ : ∀ (i : α), i sf₁ i g₁ i) (h₂ : ∀ (i : α), ¬i sf₂ i g₂ i) :
                            Set.piecewise s f₁ f₂ Set.piecewise s g₁ g₂
                            @[simp]
                            theorem Set.piecewise_insert_of_ne {α : Type u_1} {δ : αSort u_6} (s : Set α) (f : (i : α) → δ i) (g : (i : α) → δ i) [(j : α) → Decidable (j s)] {i : α} {j : α} (h : i j) [(i : α) → Decidable (i insert j s)] :
                            Set.piecewise (insert j s) f g i = Set.piecewise s f g i
                            @[simp]
                            theorem Set.piecewise_compl {α : Type u_1} {δ : αSort u_6} (s : Set α) (f : (i : α) → δ i) (g : (i : α) → δ i) [(j : α) → Decidable (j s)] [(i : α) → Decidable (i s)] :
                            @[simp]
                            theorem Set.piecewise_range_comp {α : Type u_1} {β : Type u_2} {ι : Sort u_7} (f : ια) [(j : α) → Decidable (j Set.range f)] (g₁ : αβ) (g₂ : αβ) :
                            Set.piecewise (Set.range f) g₁ g₂ f = g₁ f
                            theorem Set.MapsTo.piecewise_ite {α : Type u_1} {β : Type u_2} {s : Set α} {s₁ : Set α} {s₂ : Set α} {t : Set β} {t₁ : Set β} {t₂ : Set β} {f₁ : αβ} {f₂ : αβ} [(i : α) → Decidable (i s)] (h₁ : Set.MapsTo f₁ (s₁ s) (t₁ t)) (h₂ : Set.MapsTo f₂ (s₂ s) (t₂ t)) :
                            Set.MapsTo (Set.piecewise s f₁ f₂) (Set.ite s s₁ s₂) (Set.ite t t₁ t₂)
                            theorem Set.eqOn_piecewise {α : Type u_1} {β : Type u_2} (s : Set α) [(j : α) → Decidable (j s)] {f : αβ} {f' : αβ} {g : αβ} {t : Set α} :
                            Set.EqOn (Set.piecewise s f f') g t Set.EqOn f g (t s) Set.EqOn f' g (t s)
                            theorem Set.EqOn.piecewise_ite' {α : Type u_1} {β : Type u_2} (s : Set α) [(j : α) → Decidable (j s)] {f : αβ} {f' : αβ} {g : αβ} {t : Set α} {t' : Set α} (h : Set.EqOn f g (t s)) (h' : Set.EqOn f' g (t' s)) :
                            Set.EqOn (Set.piecewise s f f') g (Set.ite s t t')
                            theorem Set.EqOn.piecewise_ite {α : Type u_1} {β : Type u_2} (s : Set α) [(j : α) → Decidable (j s)] {f : αβ} {f' : αβ} {g : αβ} {t : Set α} {t' : Set α} (h : Set.EqOn f g t) (h' : Set.EqOn f' g t') :
                            Set.EqOn (Set.piecewise s f f') g (Set.ite s t t')
                            theorem Set.piecewise_preimage {α : Type u_1} {β : Type u_2} (s : Set α) [(j : α) → Decidable (j s)] (f : αβ) (g : αβ) (t : Set β) :
                            Set.piecewise s f g ⁻¹' t = Set.ite s (f ⁻¹' t) (g ⁻¹' t)
                            theorem Set.apply_piecewise {α : Type u_1} {δ : αSort u_6} (s : Set α) (f : (i : α) → δ i) (g : (i : α) → δ i) [(j : α) → Decidable (j s)] {δ' : αSort u_7} (h : (i : α) → δ iδ' i) {x : α} :
                            h x (Set.piecewise s f g x) = Set.piecewise s (fun x => h x (f x)) (fun x => h x (g x)) x
                            theorem Set.apply_piecewise₂ {α : Type u_1} {δ : αSort u_6} (s : Set α) (f : (i : α) → δ i) (g : (i : α) → δ i) [(j : α) → Decidable (j s)] {δ' : αSort u_7} {δ'' : αSort u_8} (f' : (i : α) → δ' i) (g' : (i : α) → δ' i) (h : (i : α) → δ iδ' iδ'' i) {x : α} :
                            h x (Set.piecewise s f g x) (Set.piecewise s f' g' x) = Set.piecewise s (fun x => h x (f x) (f' x)) (fun x => h x (g x) (g' x)) x
                            theorem Set.piecewise_op {α : Type u_1} {δ : αSort u_6} (s : Set α) (f : (i : α) → δ i) (g : (i : α) → δ i) [(j : α) → Decidable (j s)] {δ' : αSort u_7} (h : (i : α) → δ iδ' i) :
                            (Set.piecewise s (fun x => h x (f x)) fun x => h x (g x)) = fun x => h x (Set.piecewise s f g x)
                            theorem Set.piecewise_op₂ {α : Type u_1} {δ : αSort u_6} (s : Set α) (f : (i : α) → δ i) (g : (i : α) → δ i) [(j : α) → Decidable (j s)] {δ' : αSort u_7} {δ'' : αSort u_8} (f' : (i : α) → δ' i) (g' : (i : α) → δ' i) (h : (i : α) → δ iδ' iδ'' i) :
                            (Set.piecewise s (fun x => h x (f x) (f' x)) fun x => h x (g x) (g' x)) = fun x => h x (Set.piecewise s f g x) (Set.piecewise s f' g' x)
                            @[simp]
                            theorem Set.piecewise_same {α : Type u_1} {δ : αSort u_6} (s : Set α) (f : (i : α) → δ i) [(j : α) → Decidable (j s)] :
                            theorem Set.range_piecewise {α : Type u_1} {β : Type u_2} (s : Set α) [(j : α) → Decidable (j s)] (f : αβ) (g : αβ) :
                            theorem Set.injective_piecewise_iff {α : Type u_1} {β : Type u_2} (s : Set α) [(j : α) → Decidable (j s)] {f : αβ} {g : αβ} :
                            Function.Injective (Set.piecewise s f g) Set.InjOn f s Set.InjOn g s ∀ (x : α), x s∀ (y : α), ¬y sf x g y
                            theorem Set.piecewise_mem_pi {α : Type u_1} (s : Set α) [(j : α) → Decidable (j s)] {δ : αType u_7} {t : Set α} {t' : (i : α) → Set (δ i)} {f : (i : α) → δ i} {g : (i : α) → δ i} (hf : f Set.pi t t') (hg : g Set.pi t t') :
                            @[simp]
                            theorem Set.pi_piecewise {ι : Type u_7} {α : ιType u_8} (s : Set ι) (s' : Set ι) (t : (i : ι) → Set (α i)) (t' : (i : ι) → Set (α i)) [(x : ι) → Decidable (x s')] :
                            Set.pi s (Set.piecewise s' t t') = Set.pi (s s') t Set.pi (s \ s') t'
                            theorem Set.univ_pi_piecewise {ι : Type u_7} {α : ιType u_8} (s : Set ι) (t : (i : ι) → Set (α i)) (t' : (i : ι) → Set (α i)) [(x : ι) → Decidable (x s)] :
                            Set.pi Set.univ (Set.piecewise s t t') = Set.pi s t Set.pi s t'
                            theorem Set.univ_pi_piecewise_univ {ι : Type u_7} {α : ιType u_8} (s : Set ι) (t : (i : ι) → Set (α i)) [(x : ι) → Decidable (x s)] :
                            Set.pi Set.univ (Set.piecewise s t fun x => Set.univ) = Set.pi s t
                            theorem StrictMonoOn.injOn {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : αβ} {s : Set α} (H : StrictMonoOn f s) :
                            theorem StrictAntiOn.injOn {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : αβ} {s : Set α} (H : StrictAntiOn f s) :
                            theorem StrictMonoOn.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] {g : βγ} {f : αβ} {s : Set α} {t : Set β} (hg : StrictMonoOn g t) (hf : StrictMonoOn f s) (hs : Set.MapsTo f s t) :
                            theorem StrictMonoOn.comp_strictAntiOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] {g : βγ} {f : αβ} {s : Set α} {t : Set β} (hg : StrictMonoOn g t) (hf : StrictAntiOn f s) (hs : Set.MapsTo f s t) :
                            theorem StrictAntiOn.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] {g : βγ} {f : αβ} {s : Set α} {t : Set β} (hg : StrictAntiOn g t) (hf : StrictAntiOn f s) (hs : Set.MapsTo f s t) :
                            theorem StrictAntiOn.comp_strictMonoOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] {g : βγ} {f : αβ} {s : Set α} {t : Set β} (hg : StrictAntiOn g t) (hf : StrictMonoOn f s) (hs : Set.MapsTo f s t) :
                            @[simp]
                            theorem strictMono_restrict {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} {s : Set α} :
                            theorem StrictMono.of_restrict {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} {s : Set α} :

                            Alias of the forward direction of strictMono_restrict.

                            theorem StrictMonoOn.restrict {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} {s : Set α} :

                            Alias of the reverse direction of strictMono_restrict.

                            theorem StrictMono.codRestrict {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} (hf : StrictMono f) {s : Set β} (hs : ∀ (x : α), f x s) :
                            theorem Function.Injective.comp_injOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ} {g : βγ} {s : Set α} (hg : Function.Injective g) (hf : Set.InjOn f s) :
                            Set.InjOn (g f) s
                            theorem Function.Surjective.surjOn {α : Type u_1} {β : Type u_2} {f : αβ} (hf : Function.Surjective f) (s : Set β) :
                            Set.SurjOn f Set.univ s
                            theorem Function.LeftInverse.leftInvOn {α : Type u_1} {β : Type u_2} {f : αβ} {g : βα} (h : Function.LeftInverse f g) (s : Set β) :
                            theorem Function.RightInverse.rightInvOn {α : Type u_1} {β : Type u_2} {f : αβ} {g : βα} (h : Function.RightInverse f g) (s : Set α) :
                            theorem Function.LeftInverse.rightInvOn_range {α : Type u_1} {β : Type u_2} {f : αβ} {g : βα} (h : Function.LeftInverse f g) :
                            theorem Function.Semiconj.mapsTo_image {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {f : αβ} {s : Set α} {t : Set α} (h : Function.Semiconj f fa fb) (ha : Set.MapsTo fa s t) :
                            Set.MapsTo fb (f '' s) (f '' t)
                            theorem Function.Semiconj.mapsTo_range {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {f : αβ} (h : Function.Semiconj f fa fb) :
                            theorem Function.Semiconj.surjOn_image {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {f : αβ} {s : Set α} {t : Set α} (h : Function.Semiconj f fa fb) (ha : Set.SurjOn fa s t) :
                            Set.SurjOn fb (f '' s) (f '' t)
                            theorem Function.Semiconj.surjOn_range {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {f : αβ} (h : Function.Semiconj f fa fb) (ha : Function.Surjective fa) :
                            theorem Function.Semiconj.injOn_image {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {f : αβ} {s : Set α} (h : Function.Semiconj f fa fb) (ha : Set.InjOn fa s) (hf : Set.InjOn f (fa '' s)) :
                            Set.InjOn fb (f '' s)
                            theorem Function.Semiconj.injOn_range {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {f : αβ} (h : Function.Semiconj f fa fb) (ha : Function.Injective fa) (hf : Set.InjOn f (Set.range fa)) :
                            theorem Function.Semiconj.bijOn_image {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {f : αβ} {s : Set α} {t : Set α} (h : Function.Semiconj f fa fb) (ha : Set.BijOn fa s t) (hf : Set.InjOn f t) :
                            Set.BijOn fb (f '' s) (f '' t)
                            theorem Function.Semiconj.bijOn_range {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {f : αβ} (h : Function.Semiconj f fa fb) (ha : Function.Bijective fa) (hf : Function.Injective f) :
                            theorem Function.Semiconj.mapsTo_preimage {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {f : αβ} (h : Function.Semiconj f fa fb) {s : Set β} {t : Set β} (hb : Set.MapsTo fb s t) :
                            Set.MapsTo fa (f ⁻¹' s) (f ⁻¹' t)
                            theorem Function.Semiconj.injOn_preimage {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {f : αβ} (h : Function.Semiconj f fa fb) {s : Set β} (hb : Set.InjOn fb s) (hf : Set.InjOn f (f ⁻¹' s)) :
                            Set.InjOn fa (f ⁻¹' s)
                            theorem Function.update_comp_eq_of_not_mem_range' {α : Sort u_7} {β : Type u_8} {γ : βSort u_6} [DecidableEq β] (g : (b : β) → γ b) {f : αβ} {i : β} (a : γ i) (h : ¬i Set.range f) :
                            (fun j => Function.update g i a (f j)) = fun j => g (f j)
                            theorem Function.update_comp_eq_of_not_mem_range {α : Sort u_6} {β : Type u_7} {γ : Sort u_8} [DecidableEq β] (g : βγ) {f : αβ} {i : β} (a : γ) (h : ¬i Set.range f) :
                            Function.update g i a f = g f

                            Non-dependent version of Function.update_comp_eq_of_not_mem_range'

                            theorem Function.insert_injOn {α : Type u_1} (s : Set α) :
                            Set.InjOn (fun a => insert a s) s
                            theorem Function.monotoneOn_of_rightInvOn_of_mapsTo {α : Type u_6} {β : Type u_7} [PartialOrder α] [LinearOrder β] {φ : βα} {ψ : αβ} {t : Set β} {s : Set α} (hφ : MonotoneOn φ t) (φψs : Set.RightInvOn ψ φ s) (ψts : Set.MapsTo ψ s t) :
                            theorem Function.antitoneOn_of_rightInvOn_of_mapsTo {α : Type u_6} {β : Type u_7} [PartialOrder α] [LinearOrder β] {φ : βα} {ψ : αβ} {t : Set β} {s : Set α} (hφ : AntitoneOn φ t) (φψs : Set.RightInvOn ψ φ s) (ψts : Set.MapsTo ψ s t) :

                            Equivalences, permutations #

                            theorem Set.MapsTo.extendDomain {α : Type u_1} {β : Type u_2} {p : βProp} [DecidablePred p] {f : α Subtype p} {g : Equiv.Perm α} {s : Set α} {t : Set α} (h : Set.MapsTo (g) s t) :
                            Set.MapsTo (↑(Equiv.Perm.extendDomain g f)) (Subtype.val f '' s) (Subtype.val f '' t)
                            theorem Set.SurjOn.extendDomain {α : Type u_1} {β : Type u_2} {p : βProp} [DecidablePred p] {f : α Subtype p} {g : Equiv.Perm α} {s : Set α} {t : Set α} (h : Set.SurjOn (g) s t) :
                            Set.SurjOn (↑(Equiv.Perm.extendDomain g f)) (Subtype.val f '' s) (Subtype.val f '' t)
                            theorem Set.BijOn.extendDomain {α : Type u_1} {β : Type u_2} {p : βProp} [DecidablePred p] {f : α Subtype p} {g : Equiv.Perm α} {s : Set α} {t : Set α} (h : Set.BijOn (g) s t) :
                            Set.BijOn (↑(Equiv.Perm.extendDomain g f)) (Subtype.val f '' s) (Subtype.val f '' t)
                            theorem Set.LeftInvOn.extendDomain {α : Type u_1} {β : Type u_2} {p : βProp} [DecidablePred p] {f : α Subtype p} {g₁ : Equiv.Perm α} {g₂ : Equiv.Perm α} {s : Set α} (h : Set.LeftInvOn (g₁) (g₂) s) :
                            Set.LeftInvOn (↑(Equiv.Perm.extendDomain g₁ f)) (↑(Equiv.Perm.extendDomain g₂ f)) (Subtype.val f '' s)
                            theorem Set.RightInvOn.extendDomain {α : Type u_1} {β : Type u_2} {p : βProp} [DecidablePred p] {f : α Subtype p} {g₁ : Equiv.Perm α} {g₂ : Equiv.Perm α} {t : Set α} (h : Set.RightInvOn (g₁) (g₂) t) :
                            Set.RightInvOn (↑(Equiv.Perm.extendDomain g₁ f)) (↑(Equiv.Perm.extendDomain g₂ f)) (Subtype.val f '' t)
                            theorem Set.InvOn.extendDomain {α : Type u_1} {β : Type u_2} {p : βProp} [DecidablePred p] {f : α Subtype p} {g₁ : Equiv.Perm α} {g₂ : Equiv.Perm α} {s : Set α} {t : Set α} (h : Set.InvOn (g₁) (g₂) s t) :
                            Set.InvOn (↑(Equiv.Perm.extendDomain g₁ f)) (↑(Equiv.Perm.extendDomain g₂ f)) (Subtype.val f '' s) (Subtype.val f '' t)
                            theorem Equiv.bijOn' {α : Type u_1} {β : Type u_2} (e : α β) {s : Set α} {t : Set β} (h₁ : Set.MapsTo (e) s t) (h₂ : Set.MapsTo (e.symm) t s) :
                            Set.BijOn (e) s t
                            theorem Equiv.bijOn {α : Type u_1} {β : Type u_2} (e : α β) {s : Set α} {t : Set β} (h : ∀ (a : α), e a t a s) :
                            Set.BijOn (e) s t
                            theorem Equiv.invOn {α : Type u_1} {β : Type u_2} (e : α β) {s : Set α} {t : Set β} :
                            Set.InvOn (e) (e.symm) t s
                            theorem Equiv.bijOn_image {α : Type u_1} {β : Type u_2} (e : α β) {s : Set α} :
                            Set.BijOn (e) s (e '' s)
                            theorem Equiv.bijOn_symm_image {α : Type u_1} {β : Type u_2} (e : α β) {s : Set α} :
                            Set.BijOn (e.symm) (e '' s) s
                            @[simp]
                            theorem Equiv.bijOn_symm {α : Type u_1} {β : Type u_2} {e : α β} {s : Set α} {t : Set β} :
                            Set.BijOn (e.symm) t s Set.BijOn (e) s t
                            theorem Set.BijOn.equiv_symm {α : Type u_1} {β : Type u_2} {e : α β} {s : Set α} {t : Set β} :
                            Set.BijOn (e) s tSet.BijOn (e.symm) t s

                            Alias of the reverse direction of Equiv.bijOn_symm.

                            theorem Set.BijOn.of_equiv_symm {α : Type u_1} {β : Type u_2} {e : α β} {s : Set α} {t : Set β} :
                            Set.BijOn (e.symm) t sSet.BijOn (e) s t

                            Alias of the forward direction of Equiv.bijOn_symm.

                            theorem Equiv.bijOn_swap {α : Type u_1} {s : Set α} [DecidableEq α] {a : α} {b : α} (ha : a s) (hb : b s) :
                            Set.BijOn (↑(Equiv.swap a b)) s s