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
  • s.restrict f x = f x
Instances For
    theorem Set.restrict_eq {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
    s.restrict f = f Subtype.val
    @[simp]
    theorem Set.restrict_apply {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (x : s) :
    s.restrict f x = f x
    theorem Set.restrict_eq_iff {α : Type u_1} {π : αType u_5} {f : (a : α) → π a} {s : Set α} {g : (a : s) → π a} :
    s.restrict f = g ∀ (a : α) (ha : a s), f a = g a, ha
    theorem Set.eq_restrict_iff {α : Type u_1} {π : αType u_5} {s : Set α} {f : (a : s) → π a} {g : (a : α) → π a} :
    f = s.restrict g ∀ (a : α) (ha : a s), f a, ha = g a
    @[simp]
    theorem Set.range_restrict {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
    Set.range (s.restrict f) = f '' s
    theorem Set.image_restrict {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (t : Set α) :
    s.restrict f '' (Subtype.val ⁻¹' t) = f '' (t s)
    @[simp]
    theorem Set.restrict_dite {α : Type u_1} {β : Type u_2} {s : Set α} [(x : α) → Decidable (x s)] (f : (a : α) → a sβ) (g : (a : α) → asβ) :
    (s.restrict fun (a : α) => if h : a s then f a h else g a h) = fun (a : s) => f a
    @[simp]
    theorem Set.restrict_dite_compl {α : Type u_1} {β : Type u_2} {s : Set α} [(x : α) → Decidable (x s)] (f : (a : α) → a sβ) (g : (a : α) → asβ) :
    (s.restrict fun (a : α) => if h : a s then f a h else g a h) = fun (a : s) => g a
    @[simp]
    theorem Set.restrict_ite {α : Type u_1} {β : Type u_2} (f : αβ) (g : αβ) (s : Set α) [(x : α) → Decidable (x s)] :
    (s.restrict fun (a : α) => if a s then f a else g a) = s.restrict f
    @[simp]
    theorem Set.restrict_ite_compl {α : Type u_1} {β : Type u_2} (f : αβ) (g : αβ) (s : Set α) [(x : α) → Decidable (x s)] :
    (s.restrict fun (a : α) => if a s then f a else g a) = s.restrict g
    @[simp]
    theorem Set.restrict_piecewise {α : Type u_1} {β : Type u_2} (f : αβ) (g : αβ) (s : Set α) [(x : α) → Decidable (x s)] :
    s.restrict (s.piecewise f g) = s.restrict f
    @[simp]
    theorem Set.restrict_piecewise_compl {α : Type u_1} {β : Type u_2} (f : αβ) (g : αβ) (s : Set α) [(x : α) → Decidable (x s)] :
    s.restrict (s.piecewise f g) = s.restrict g
    theorem Set.restrict_extend_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ) (g : αγ) (g' : βγ) :
    (Set.range f).restrict (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.range f).restrict (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) :
      b.restrict g Set.codRestrict f b h = g f
      @[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₂ : αβ} :
      s.restrict f₁ = s.restrict 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 for monotonicity and antitonicity #

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

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

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

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

      Reverse of Set.codRestrict_restrict.

      theorem Set.MapsTo.coe_restrict {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : Set.MapsTo f s t) :
      Subtype.val Set.MapsTo.restrict f s t h = s.restrict f
      theorem Set.MapsTo.range_restrict {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (t : Set β) (h : 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 β) :
      @[simp]
      theorem Set.mapsTo_empty_iff {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} :
      theorem Set.MapsTo.nonempty {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : Set.MapsTo f s t) (hs : s.Nonempty) :
      t.Nonempty

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

      Alias of Set.restrictPreimage_injective.

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

      Alias of Set.restrictPreimage_surjective.

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

      Alias of Set.restrictPreimage_bijective.

      Injectivity on a set #

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

      Alias of the forward direction of Set.injOn_iff_injective.

      theorem Set.MapsTo.restrict_inj {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : 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 Set.InjOn.image {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} (h : Set.InjOn f s) :
      theorem Set.InjOn.image_eq_image_iff {α : Type u_1} {β : Type u_2} {s : Set α} {s₁ : Set α} {s₂ : Set α} {f : αβ} (h : Set.InjOn f s) (h₁ : s₁ s) (h₂ : s₂ s) :
      f '' s₁ = f '' s₂ s₁ = s₂
      theorem Set.InjOn.image_subset_image_iff {α : Type u_1} {β : Type u_2} {s : Set α} {s₁ : Set α} {s₂ : Set α} {f : αβ} (h : Set.InjOn f s) (h₁ : s₁ s) (h₂ : s₂ s) :
      f '' s₁ f '' s₂ s₁ s₂
      theorem Set.InjOn.image_ssubset_image_iff {α : Type u_1} {β : Type u_2} {s : Set α} {s₁ : Set α} {s₂ : Set α} {f : αβ} (h : Set.InjOn f s) (h₁ : s₁ s) (h₂ : s₂ s) :
      f '' s₁ f '' s₂ s₁ s₂
      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)
      theorem Set.InjOn.image_diff {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {t : Set α} (h : Set.InjOn f s) :
      f '' (s \ t) = f '' s \ f '' (s t)
      theorem Set.InjOn.image_diff_subset {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {t : Set α} (h : Set.InjOn f s) (hst : t s) :
      f '' (s \ t) = f '' s \ f '' t
      theorem Set.InjOn.imageFactorization_injective {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} (h : Set.InjOn f s) :
      @[simp]
      theorem Set.imageFactorization_injective_iff {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} :
      @[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_empty_iff {α : Type u_1} {β : Type u_2} {t : Set β} {f : αβ} :
      @[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 : t.Nonempty) :
      s.Nonempty
      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 : t.Nonemptys.Nonempty) :
      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 : αβ} :
      Set.SurjOn f s Set.univ Function.Surjective (s.restrict f)
      @[simp]
      theorem Set.MapsTo.restrict_surjective_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : 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)
      theorem Set.SurjOn.forall {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {p : βProp} (hf : Set.SurjOn f s t) (hf' : Set.MapsTo f s t) :
      (yt, p y) xs, p (f x)

      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_empty_iff_left {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} :
      @[simp]
      theorem Set.bijOn_empty_iff_right {α : Type u_1} {β : Type u_2} {t : Set β} {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.forall {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {p : βProp} (hf : Set.BijOn f s t) :
      (bt, p b) as, p (f a)
      theorem Set.BijOn.exists {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {p : βProp} (hf : Set.BijOn f s t) :
      (bt, p b) as, p (f a)
      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 : s.Nonempty t.Nonempty) :
      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) :
      theorem Set.BijOn.subset_right {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {r : Set β} (hf : Set.BijOn f s t) (hrt : r t) :
      Set.BijOn f (s f ⁻¹' r) r
      theorem Set.BijOn.subset_left {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {r : Set α} (hf : Set.BijOn f s t) (hrs : r s) :
      Set.BijOn f r (f '' r)

      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 : as, f a = b) :
        theorem Function.invFunOn_mem {α : Type u_1} {β : Type u_2} [Nonempty α] {s : Set α} {f : αβ} {b : β} (h : as, f a = b) :
        theorem Function.invFunOn_eq {α : Type u_1} {β : Type u_2} [Nonempty α] {s : Set α} {f : αβ} {b : β} (h : as, 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 : ¬as, 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.image_invFunOn_image_of_subset {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} [Nonempty α] {r : Set β} (hf : Set.SurjOn f s t) (hrt : r t) :
        f '' (Function.invFunOn f s '' r) = r

        This lemma is a special case of rightInvOn_invFunOn.image_image'; it may make more sense to use the other lemma directly in an application.

        theorem Set.SurjOn.image_invFunOn_image {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} [Nonempty α] (hf : Set.SurjOn f s t) :
        f '' (Function.invFunOn f s '' t) = t

        This lemma is a special case of rightInvOn_invFunOn.image_image; it may make more sense to use the other lemma directly in an application.

        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 ts'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.BijOn.exists_extend_of_subset {α : Type u_1} {β : Type u_2} {s : Set α} {s₁ : Set α} {t : Set β} {f : αβ} {t' : Set β} (h : Set.BijOn f s t) (hss₁ : s s₁) (htt' : t t') (ht' : Set.SurjOn f s₁ t') :
        ∃ (s' : Set α), s s' s' s₁ Set.BijOn f s' t'

        If f maps s bijectively to t and a set t' is contained in the image of some s₁ ⊇ s, then s₁ has a subset containing s that f maps bijectively to t'.

        theorem Set.BijOn.exists_extend {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {t' : Set β} (h : Set.BijOn f s t) (htt' : t t') (ht' : t' Set.range f) :
        ∃ (s' : Set α), s s' Set.BijOn f s' t'

        If f maps s bijectively to t, and t' is a superset of t contained in the range of f, then f maps some superset of s bijectively to t'.

        theorem Set.InjOn.exists_subset_injOn_subset_range_eq {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {r : Set α} (hinj : Set.InjOn f r) (hrs : r s) :
        ∃ (u : Set α), r u u s f '' u = f '' s Set.InjOn f u
        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 α) :
        Monotone (s.restrict f)
        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 )] :
        .piecewise f g = g
        @[simp]
        theorem Set.piecewise_univ {α : Type u_1} {δ : αSort u_6} (f : (i : α) → δ i) (g : (i : α) → δ i) [(i : α) → Decidable (i Set.univ)] :
        Set.univ.piecewise 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)] :
        (insert j s).piecewise 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)] :
        (insert j s).piecewise f g = Function.update (s.piecewise f g) j (f j)
        @[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) :
        s.piecewise 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) :
        s.piecewise f g i = g i
        theorem Set.piecewise_singleton {α : Type u_1} {β : Type u_2} (x : α) [(y : α) → Decidable (y {x})] [DecidableEq α] (f : αβ) (g : αβ) :
        {x}.piecewise 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 : αβ) :
        Set.EqOn (s.piecewise f g) f s
        theorem Set.piecewise_eqOn_compl {α : Type u_1} {β : Type u_2} (s : Set α) [(j : α) → Decidable (j s)] (f : αβ) (g : αβ) :
        Set.EqOn (s.piecewise f g) g s
        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) :
        s.piecewise 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 s.piecewise 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) :
        s.piecewise f₁ f₂ s.piecewise 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)] :
        (insert j s).piecewise f g i = s.piecewise 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)] :
        s.piecewise f g = s.piecewise g f
        @[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.range f).piecewise 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 (s.piecewise f₁ f₂) (s.ite s₁ s₂) (t.ite 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 (s.piecewise 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 (s.piecewise f f') g (s.ite 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 (s.piecewise f f') g (s.ite t t')
        theorem Set.piecewise_preimage {α : Type u_1} {β : Type u_2} (s : Set α) [(j : α) → Decidable (j s)] (f : αβ) (g : αβ) (t : Set β) :
        s.piecewise f g ⁻¹' t = s.ite (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 (s.piecewise f g x) = s.piecewise (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 (s.piecewise f g x) (s.piecewise f' g' x) = s.piecewise (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) :
        (s.piecewise (fun (x : α) => h x (f x)) fun (x : α) => h x (g x)) = fun (x : α) => h x (s.piecewise 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) :
        (s.piecewise (fun (x : α) => h x (f x) (f' x)) fun (x : α) => h x (g x) (g' x)) = fun (x : α) => h x (s.piecewise f g x) (s.piecewise f' g' x)
        @[simp]
        theorem Set.piecewise_same {α : Type u_1} {δ : αSort u_6} (s : Set α) (f : (i : α) → δ i) [(j : α) → Decidable (j s)] :
        s.piecewise f f = f
        theorem Set.range_piecewise {α : Type u_1} {β : Type u_2} (s : Set α) [(j : α) → Decidable (j s)] (f : αβ) (g : αβ) :
        Set.range (s.piecewise f g) = f '' s g '' s
        theorem Set.injective_piecewise_iff {α : Type u_1} {β : Type u_2} (s : Set α) [(j : α) → Decidable (j s)] {f : αβ} {g : αβ} :
        Function.Injective (s.piecewise 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 t.pi t') (hg : g t.pi t') :
        s.piecewise f g t.pi 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')] :
        s.pi (s'.piecewise t t') = (s s').pi t (s \ s').pi 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.univ.pi (s.piecewise t t') = s.pi t s.pi t'
        theorem Set.univ_pi_piecewise_univ {ι : Type u_7} {α : ιType u_8} (s : Set ι) (t : (i : ι) → Set (α i)) [(x : ι) → Decidable (x s)] :
        Set.univ.pi (s.piecewise t fun (x : ι) => Set.univ) = s.pi 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 α} :
        StrictMono (s.restrict f) StrictMonoOn f s
        theorem StrictMonoOn.restrict {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} {s : Set α} :
        StrictMonoOn f sStrictMono (s.restrict f)

        Alias of the reverse direction of strictMono_restrict.

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

        Alias of the forward 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 ((g.extendDomain 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 ((g.extendDomain 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 ((g.extendDomain 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 ((g₁.extendDomain f)) ((g₂.extendDomain 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 ((g₁.extendDomain f)) ((g₂.extendDomain 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 ((g₁.extendDomain f)) ((g₂.extendDomain f)) (Subtype.val f '' s) (Subtype.val f '' t)
        theorem Set.InjOn.prodMap {α₁ : Type u_6} {α₂ : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} {s₁ : Set α₁} {s₂ : Set α₂} {f₁ : α₁β₁} {f₂ : α₂β₂} (h₁ : Set.InjOn f₁ s₁) (h₂ : Set.InjOn f₂ s₂) :
        Set.InjOn (fun (x : α₁ × α₂) => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂)
        theorem Set.SurjOn.prodMap {α₁ : Type u_6} {α₂ : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} {s₁ : Set α₁} {s₂ : Set α₂} {t₁ : Set β₁} {t₂ : Set β₂} {f₁ : α₁β₁} {f₂ : α₂β₂} (h₁ : Set.SurjOn f₁ s₁ t₁) (h₂ : Set.SurjOn f₂ s₂ t₂) :
        Set.SurjOn (fun (x : α₁ × α₂) => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)
        theorem Set.MapsTo.prodMap {α₁ : Type u_6} {α₂ : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} {s₁ : Set α₁} {s₂ : Set α₂} {t₁ : Set β₁} {t₂ : Set β₂} {f₁ : α₁β₁} {f₂ : α₂β₂} (h₁ : Set.MapsTo f₁ s₁ t₁) (h₂ : Set.MapsTo f₂ s₂ t₂) :
        Set.MapsTo (fun (x : α₁ × α₂) => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)
        theorem Set.BijOn.prodMap {α₁ : Type u_6} {α₂ : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} {s₁ : Set α₁} {s₂ : Set α₂} {t₁ : Set β₁} {t₂ : Set β₂} {f₁ : α₁β₁} {f₂ : α₂β₂} (h₁ : Set.BijOn f₁ s₁ t₁) (h₂ : Set.BijOn f₂ s₂ t₂) :
        Set.BijOn (fun (x : α₁ × α₂) => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)
        theorem Set.LeftInvOn.prodMap {α₁ : Type u_6} {α₂ : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} {s₁ : Set α₁} {s₂ : Set α₂} {f₁ : α₁β₁} {f₂ : α₂β₂} {g₁ : β₁α₁} {g₂ : β₂α₂} (h₁ : Set.LeftInvOn g₁ f₁ s₁) (h₂ : Set.LeftInvOn g₂ f₂ s₂) :
        Set.LeftInvOn (fun (x : β₁ × β₂) => (g₁ x.1, g₂ x.2)) (fun (x : α₁ × α₂) => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂)
        theorem Set.RightInvOn.prodMap {α₁ : Type u_6} {α₂ : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} {t₁ : Set β₁} {t₂ : Set β₂} {f₁ : α₁β₁} {f₂ : α₂β₂} {g₁ : β₁α₁} {g₂ : β₂α₂} (h₁ : Set.RightInvOn g₁ f₁ t₁) (h₂ : Set.RightInvOn g₂ f₂ t₂) :
        Set.RightInvOn (fun (x : β₁ × β₂) => (g₁ x.1, g₂ x.2)) (fun (x : α₁ × α₂) => (f₁ x.1, f₂ x.2)) (t₁ ×ˢ t₂)
        theorem Set.InvOn.prodMap {α₁ : Type u_6} {α₂ : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} {s₁ : Set α₁} {s₂ : Set α₂} {t₁ : Set β₁} {t₂ : Set β₂} {f₁ : α₁β₁} {f₂ : α₂β₂} {g₁ : β₁α₁} {g₂ : β₂α₂} (h₁ : Set.InvOn g₁ f₁ s₁ t₁) (h₂ : Set.InvOn g₂ f₂ s₂ t₂) :
        Set.InvOn (fun (x : β₁ × β₂) => (g₁ x.1, g₂ x.2)) (fun (x : α₁ × α₂) => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ 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.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 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 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