# Functions over sets #

## Main definitions #

### Predicate #

• Set.EqOn f₁ f₂ s : functions f₁ and f₂ are equal at every point of s;
• Set.MapsTo f s t : f sends every point of s to a point of t;
• Set.InjOn f s : restriction of f to s is injective;
• Set.SurjOn f s t : every point in s has a preimage in s;
• Set.BijOn f s t : f is a bijection between s and t;
• Set.LeftInvOn f' f s : for every x ∈ s we have f' (f x) = x;
• Set.RightInvOn f' f t : for every y ∈ t we have f (f' y) = y;
• Set.InvOn f' f s t : f' is a two-side inverse of f on s and t, i.e. we have Set.LeftInvOn f' f s and Set.RightInvOn f' f t.

### Functions #

• Set.restrict f s : restrict the domain of f to the set s;
• Set.codRestrict f s h : given h : ∀ x, f x ∈ s, restrict the codomain of f to the set s;
• Set.MapsTo.restrict f s t h: given h : MapsTo f s t, restrict the domain of f to s and the codomain to t.

### 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
@[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 : ) (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 = 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₂ : αβ} [] [] (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₂ : αβ} [] [] (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₂ : αβ} [] [] (h₁ : StrictMonoOn f₁ s) (h : Set.EqOn f₁ f₂ s) :
theorem StrictAntiOn.congr {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} [] [] (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₂ : αβ} [] [] (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₂ : αβ} [] [] (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₂ : αβ} [] [] (h : Set.EqOn f₁ f₂ s) :
theorem Set.EqOn.congr_strictAntiOn {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} [] [] (h : Set.EqOn f₁ f₂ s) :

### Monotonicity lemmas #

theorem MonotoneOn.mono {α : Type u_1} {β : Type u_2} {s : Set α} {s₂ : Set α} {f : αβ} [] [] (h : ) (h' : s₂ s) :
MonotoneOn f s₂
theorem AntitoneOn.mono {α : Type u_1} {β : Type u_2} {s : Set α} {s₂ : Set α} {f : αβ} [] [] (h : ) (h' : s₂ s) :
AntitoneOn f s₂
theorem StrictMonoOn.mono {α : Type u_1} {β : Type u_2} {s : Set α} {s₂ : Set α} {f : αβ} [] [] (h : ) (h' : s₂ s) :
theorem StrictAntiOn.mono {α : Type u_1} {β : Type u_2} {s : Set α} {s₂ : Set α} {f : αβ} [] [] (h : ) (h' : s₂ s) :
theorem MonotoneOn.monotone {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} [] [] (h : ) :
Monotone (f Subtype.val)
theorem AntitoneOn.monotone {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} [] [] (h : ) :
Antitone (f Subtype.val)
theorem StrictMonoOn.strictMono {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} [] [] (h : ) :
StrictMono (f Subtype.val)
theorem StrictAntiOn.strictAnti {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} [] [] (h : ) :
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 = 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 =

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.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 = 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 : αβ} :
s =
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 β} [] (f : αβ) (h : s.Nonemptyt.Nonempty) :
theorem Set.mapsTo_of_subsingleton {α : Type u_1} [] (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 ⁻¹'
@[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 (t.restrictPreimage f)
theorem Set.restrictPreimage_surjective {α : Type u_1} {β : Type u_2} (t : Set β) {f : αβ} (hf : ) :
Function.Surjective (t.restrictPreimage f)
theorem Set.restrictPreimage_bijective {α : Type u_1} {β : Type u_2} (t : Set β) {f : αβ} (hf : ) :
Function.Bijective (t.restrictPreimage f)
theorem Function.Injective.restrictPreimage {α : Type u_1} {β : Type u_2} (t : Set β) {f : αβ} (hf : ) :
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 (t.restrictPreimage f)

Alias of Set.restrictPreimage_surjective.

theorem Function.Bijective.restrictPreimage {α : Type u_1} {β : Type u_2} (t : Set β) {f : αβ} (hf : ) :
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 : ) (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 : ) (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 : ) (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) f af '' s
theorem Set.injective_iff_injOn_univ {α : Type u_1} {β : Type u_2} {f : αβ} :
Set.InjOn f Set.univ
theorem Set.injOn_of_injective {α : Type u_1} {β : Type u_2} {f : αβ} (h : ) {s : Set α} :
theorem Function.Injective.injOn {α : Type u_1} {β : Type u_2} {f : αβ} (h : ) {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 : ) (hf : ) (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 : ) (hf : Set.MapsTo f s s) (n : ) :
theorem Set.injOn_of_subsingleton {α : Type u_1} {β : Type u_2} [] (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 : αβ} :
Function.Injective (s.restrict f)
theorem Set.InjOn.injective {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} :
Function.Injective (s.restrict f)

Alias of the forward direction of Set.injOn_iff_injective.

theorem Set.MapsTo.restrict_inj {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : Set.MapsTo f s t) :
theorem Set.exists_injOn_iff_injective {α : Type u_1} {β : Type u_2} {s : Set α} [] :
(∃ (f : αβ), ) ∃ (f : sβ),
theorem Set.injOn_preimage {α : Type u_1} {β : Type u_2} {f : αβ} {B : Set (Set β)} (hB : B ) :
theorem Set.InjOn.mem_of_mem_image {α : Type u_1} {β : Type u_2} {s : Set α} {s₁ : Set α} {f : αβ} {x : α} (hf : ) (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 : ) (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 : ) (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 : ) (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 : ) (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 : ) (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 : ) :
theorem Set.InjOn.image_eq_image_iff {α : Type u_1} {β : Type u_2} {s : Set α} {s₁ : Set α} {s₂ : Set α} {f : αβ} (h : ) (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 : ) (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 : ) (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 : ) (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 : ) :
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 : ) (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 : ) :
@[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 α) :
Set.graphOn f (s t) =
@[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 '' = s
theorem Set.exists_eq_graphOn_image_fst {α : Type u_1} {β : Type u_2} [] {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} [] {s : Set (α × β)} :
(∃ (f : αβ) (t : Set α), s = ) 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) :
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' ∀ (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 : αβ} :
t =
@[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 : ) (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 β} [] (f : αβ) (h : t.Nonemptys.Nonempty) :
theorem Set.surjOn_of_subsingleton {α : Type u_1} [] (f : αα) (s : Set α) :
theorem Set.surjective_iff_surjOn_univ {α : Type u_1} {β : Type u_2} {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' : ) :
theorem Set.MapsTo.surjOn_compl {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : Set.MapsTo f s t) (h' : ) :
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₂ : ) (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 : αβ} :
s =
@[simp]
theorem Set.bijOn_empty_iff_right {α : Type u_1} {β : Type u_2} {t : Set β} {f : αβ} :
t =
@[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) :
t
theorem Set.InjOn.bijOn_image {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} (h : ) :
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 β} [] [] (f : αβ) (h : s.Nonempty t.Nonempty) :
Set.BijOn f s t
theorem Set.bijOn_of_subsingleton {α : Type u_1} [] (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 : αβ} :
Set.BijOn f Set.univ Set.univ
theorem Function.Bijective.bijOn_univ {α : Type u_1} {β : Type u_2} {f : αβ} :
Set.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 : ) :
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 : ) (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} [] (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} [] {s : Set α} {f : αβ} {b : β} (h : as, f a = b) :
s f (Function.invFunOn f s b) = b
theorem Function.invFunOn_mem {α : Type u_1} {β : Type u_2} [] {s : Set α} {f : αβ} {b : β} (h : as, f a = b) :
s
theorem Function.invFunOn_eq {α : Type u_1} {β : Type u_2} [] {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} [] {s : Set α} {f : αβ} {b : β} (h : ¬as, f a = b) :
@[simp]
theorem Function.invFunOn_apply_mem {α : Type u_1} {β : Type u_2} [] {s : Set α} {f : αβ} {a : α} (h : a s) :
theorem Function.invFunOn_apply_eq {α : Type u_1} {β : Type u_2} [] {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 : αβ} [] (h : ) :
theorem Set.InjOn.invFunOn_image {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {f : αβ} [] (h : Set.InjOn f s₂) (ht : s₁ s₂) :
'' (f '' s₁) = s₁
theorem Function.leftInvOn_invFunOn_of_subset_image_image {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} [] (h : s '' (f '' s)) :
theorem Set.injOn_iff_invFunOn_image_image_eq_self {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} [] :
'' (f '' s) = s
theorem Function.invFunOn_injOn_image {α : Type u_1} {β : Type u_2} [] (f : αβ) (s : Set α) :
theorem Function.invFunOn_image_image_subset {α : Type u_1} {β : Type u_2} [] (f : αβ) (s : Set α) :
'' (f '' s) s
theorem Set.SurjOn.rightInvOn_invFunOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} [] (h : Set.SurjOn f s t) :
theorem Set.BijOn.invOn_invFunOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} [] (h : Set.BijOn f s t) :
Set.InvOn f s t
theorem Set.SurjOn.invOn_invFunOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} [] (h : Set.SurjOn f s t) :
Set.InvOn f ( '' t) t
theorem Set.SurjOn.mapsTo_invFunOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} [] (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 : αβ} [] {r : Set β} (hf : Set.SurjOn f s t) (hrt : r t) :
f '' ( '' 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 : αβ} [] (hf : Set.SurjOn f s t) :
f '' ( '' 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 : αβ} [] (h : Set.SurjOn f s t) :
Set.BijOn f ( '' t) 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
theorem Set.exists_image_eq_injOn_of_subset_range {α : Type u_1} {β : Type u_2} {t : Set β} {f : αβ} (ht : t ) :
∃ (s : Set α), f '' s = t
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' ) :
∃ (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 : ) (hrs : r s) :
∃ (u : Set α), r u u s f '' u = f '' s
theorem Set.preimage_invFun_of_mem {α : Type u_1} {β : Type u_2} [n : ] {f : αβ} (hf : ) {s : Set α} (h : ) :
= f '' s (Set.range f)
theorem Set.preimage_invFun_of_not_mem {α : Type u_1} {β : Type u_2} [n : ] {f : αβ} (hf : ) {s : Set α} (h : s) :
= f '' s
theorem Set.BijOn.symm {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {g : βα} (h : Set.InvOn f g t s) (hf : Set.BijOn f s t) :
Set.BijOn g t s
theorem Set.bijOn_comm {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {g : βα} (h : Set.InvOn f g t s) :
Set.BijOn f s t Set.BijOn g t s

### Monotone #

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

### 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
• = instDecidableNot
theorem Set.piecewise_insert {α : Type u_1} {δ : αSort u_6} (s : Set α) (f : (i : α) → δ i) (g : (i : α) → δ i) [(j : α) → Decidable (j s)] [] (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})] [] (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 )] (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) 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} [] [] {f : αβ} {s : Set α} (H : ) :
theorem StrictAntiOn.injOn {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} (H : ) :
theorem StrictMonoOn.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {g : βγ} {f : αβ} {s : Set α} {t : Set β} (hg : ) (hf : ) (hs : Set.MapsTo f s t) :
theorem StrictMonoOn.comp_strictAntiOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {g : βγ} {f : αβ} {s : Set α} {t : Set β} (hg : ) (hf : ) (hs : Set.MapsTo f s t) :
theorem StrictAntiOn.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {g : βγ} {f : αβ} {s : Set α} {t : Set β} (hg : ) (hf : ) (hs : Set.MapsTo f s t) :
theorem StrictAntiOn.comp_strictMonoOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {g : βγ} {f : αβ} {s : Set α} {t : Set β} (hg : ) (hf : ) (hs : Set.MapsTo f s t) :
@[simp]
theorem strictMono_restrict {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} :
StrictMono (s.restrict f)
theorem StrictMonoOn.restrict {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} :
StrictMono (s.restrict f)

Alias of the reverse direction of strictMono_restrict.

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

Alias of the forward direction of strictMono_restrict.

theorem StrictMono.codRestrict {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) {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 : ) (hf : ) :
Set.InjOn (g f) s
theorem Function.Surjective.surjOn {α : Type u_1} {β : Type u_2} {f : αβ} (hf : ) (s : Set β) :
Set.SurjOn f Set.univ s
theorem Function.LeftInverse.leftInvOn {α : Type u_1} {β : Type u_2} {f : αβ} {g : βα} (h : ) (s : Set β) :
theorem Function.RightInverse.rightInvOn {α : Type u_1} {β : Type u_2} {f : αβ} {g : βα} (h : ) (s : Set α) :
theorem Function.LeftInverse.rightInvOn_range {α : Type u_1} {β : Type u_2} {f : αβ} {g : βα} (h : ) :
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 : ) :
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 : ) (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.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 : ) (hf : ) :
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} [] (g : (b : β) → γ b) {f : αβ} {i : β} (a : γ i) (h : i) :
(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} [] (g : βγ) {f : αβ} {i : β} (a : γ) (h : i) :
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} [] [] {φ : βα} {ψ : αβ} {t : Set β} {s : Set α} (hφ : ) (φψs : ) (ψts : Set.MapsTo ψ s t) :
theorem Function.antitoneOn_of_rightInvOn_of_mapsTo {α : Type u_1} {β : Type u_2} [] [] {φ : βα} {ψ : αβ} {t : Set β} {s : Set α} (hφ : ) (φψs : ) (ψts : Set.MapsTo ψ s t) :

### Equivalences, permutations #

theorem Set.MapsTo.extendDomain {α : Type u_1} {β : Type u_2} {p : βProp} [] {f : α } {g : } {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} [] {f : α } {g : } {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} [] {f : α } {g : } {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} [] {f : α } {g₁ : } {g₂ : } {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} [] {f : α } {g₁ : } {g₂ : } {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} [] {f : α } {g₁ : } {g₂ : } {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 α} [] {a : α} {b : α} (ha : a s) (hb : b s) :
Set.BijOn (⇑(Equiv.swap a b)) s s