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 : α) → asβ) :
    (Set.restrict s 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β) :
    (Set.restrict s 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)] :
    (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 : (Set.range f)) => g (Exists.choose )
    @[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 #

      @[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.eqOn_univ {α : Type u_1} {β : Type u_2} (f₁ : αβ) (f₂ : αβ) :
      Set.EqOn f₁ f₂ Set.univ f₁ = f₂
      @[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.image_eq_self {α : Type u_1} {s : Set α} {f : αα} (h : Set.EqOn f id s) :
      f '' s = s

      Variant of EqOn.image_eq, for one function being the identity.

      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 #

      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
      theorem Set.MapsTo.coe_iterate_restrict {α : Type u_1} {s : Set α} {f : αα} (h : Set.MapsTo f s s) (x : s) (k : ) :
      ((Set.MapsTo.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 : Set.MapsTo f s t) :

      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 : st), ∀ (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.nonempty {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : Set.MapsTo f s t) (hs : Set.Nonempty s) :

      If f maps s to t and s is non-empty, t is non-empty.

      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_range {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
      @[simp]
      theorem Set.mapsTo_image_iff {α : 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
      @[deprecated]
      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.mapsTo_univ_iff {α : Type u_1} {β : Type u_2} {t : Set β} {f : αβ} :
      Set.MapsTo f Set.univ t ∀ (x : α), f x t
      @[deprecated]
      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.mapsTo_range_iff {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {t : Set β} {f : αβ} {g : ια} :
      Set.MapsTo f (Set.range g) t ∀ (i : ι), f (g i) t
      @[deprecated Set.mapsTo_range_iff]
      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 #

      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 #

      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}
      @[simp]
      theorem Set.injOn_pair {α : Type u_1} {β : Type u_2} {f : αβ} {a : α} {b : α} :
      Set.InjOn f {a, b} f a = f ba = b
      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₂ xs₁, ys₂, f x f y
      theorem Set.injOn_insert {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} {a : α} (has : as) :
      Set.InjOn f (insert a s) Set.InjOn f s f af '' 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.image_of_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {f : αβ} {g : βγ} (h : Set.InjOn (g f) s) :
      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 : sβ), 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)
      @[simp]
      theorem Set.graphOn_empty {α : Type u_1} {β : Type u_2} (f : αβ) :
      @[simp]
      theorem Set.graphOn_union {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (t : Set α) :
      @[simp]
      theorem Set.graphOn_singleton {α : Type u_1} {β : Type u_2} (f : αβ) (x : α) :
      Set.graphOn f {x} = {(x, f x)}
      @[simp]
      theorem Set.graphOn_insert {α : Type u_1} {β : Type u_2} (f : αβ) (x : α) (s : Set α) :
      Set.graphOn f (insert x s) = insert (x, f x) (Set.graphOn f s)
      @[simp]
      theorem Set.image_fst_graphOn {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
      Prod.fst '' Set.graphOn f s = s
      theorem Set.exists_eq_graphOn_image_fst {α : Type u_1} {β : Type u_2} [Nonempty β] {s : Set (α × β)} :
      (∃ (f : αβ), s = Set.graphOn f (Prod.fst '' s)) Set.InjOn Prod.fst s
      theorem Set.exists_eq_graphOn {α : Type u_1} {β : Type u_2} [Nonempty β] {s : Set (α × β)} :
      (∃ (f : αβ) (t : Set α), s = Set.graphOn f t) Set.InjOn Prod.fst s

      Surjectivity on a set #

      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' : Set β) (g : st'), 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 : αβ} :
      @[simp]
      theorem Set.MapsTo.restrict_surjective_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : Set.MapsTo f s t) :
      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.image_preimage {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {t₁ : Set β} {f : αβ} (h : Set.SurjOn f s t) (ht : t₁ t) :
      f '' (f ⁻¹' t₁) = 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 #

      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 Equiv.image_eq_iff_bijOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (e : α β) :
      e '' s = t Set.BijOn (e) 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 #

      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 #

      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 #

      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.Embedding.invOfMemRange.

      Equations
      Instances For
        theorem Function.invFunOn_pos {α : Type u_1} {β : Type u_2} [Nonempty α] {s : Set α} {f : αβ} {b : β} (h : ∃ a ∈ s, f a = b) :
        theorem Function.invFunOn_mem {α : Type u_1} {β : Type u_2} [Nonempty α] {s : Set α} {f : αβ} {b : β} (h : ∃ a ∈ s, f a = b) :
        theorem Function.invFunOn_eq {α : Type u_1} {β : Type u_2} [Nonempty α] {s : Set α} {f : αβ} {b : β} (h : ∃ 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 ∈ 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' ⊆ s, Set.BijOn f s' t
        theorem Set.SurjOn.exists_bijOn_subset {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} :
        Set.SurjOn f s t∃ s' ⊆ s, Set.BijOn f s' t

        Alias of the forward direction of Set.surjOn_iff_exists_bijOn_subset.

        theorem Set.exists_subset_bijOn {α : Type u_1} {β : Type u_2} (s : Set α) (f : αβ) :
        ∃ s' ⊆ s, Set.BijOn f s' (f '' s)
        theorem Set.exists_image_eq_and_injOn {α : Type u_1} {β : Type u_2} (s : Set α) (f : αβ) :
        ∃ (u : Set α), f '' u = f '' s Set.InjOn f u
        theorem Set.exists_image_eq_injOn_of_subset_range {α : Type u_1} {β : Type u_2} {t : Set β} {f : αβ} (ht : t Set.range f) :
        ∃ (s : Set α), f '' s = t Set.InjOn f s
        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 ns) :
        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 : is) :
        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₁ : is, f₁ i g i) (h₂ : is, f₂ 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₁ : is, g i f₁ i) (h₂ : is, g 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₁ : is, f₁ i g₁ i) (h₂ : is, f₂ 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 xs, ys, f 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_6} {β : Type u_7} {γ : βSort u_8} [DecidableEq β] (g : (b : β) → γ b) {f : αβ} {i : β} (a : γ i) (h : iSet.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 : iSet.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_1} {β : Type u_2} [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