Documentation

Mathlib.Data.Set.Function

Functions over sets #

Main definitions #

Predicate #

Functions #

Restrict #

def Set.restrict {α : Type u_1} {π : αType u_6} (s : Set α) (f : (a : α) → π a) (a : s) :
π a

Restrict domain of a function f to a set s. Same as Subtype.restrict but this version takes an argument ↥s instead of Subtype s.

Equations
theorem Set.restrict_def {α : Type u_1} {π : αType u_6} (s : Set α) :
s.restrict = fun (f : (a : α) → π a) (x : s) => f x
theorem Set.restrict_eq {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
@[simp]
theorem Set.restrict_apply {α : Type u_1} {π : αType u_6} (f : (a : α) → π a) (s : Set α) (x : s) :
s.restrict f x = f x
theorem Set.restrict_eq_iff {α : Type u_1} {π : αType u_6} {f : (a : α) → π a} {s : Set α} {g : (a : s) → π a} :
s.restrict f = g ∀ (a : α) (ha : a s), f a = g a, ha
theorem Set.eq_restrict_iff {α : Type u_1} {π : αType u_6} {s : Set α} {f : (a : s) → π a} {g : (a : α) → π a} :
f = s.restrict g ∀ (a : α) (ha : a s), f a, ha = g a
@[simp]
theorem Set.range_restrict {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
range (s.restrict f) = f '' s
theorem Set.image_restrict {α : Type u_1} {β : Type u_2} (f : αβ) (s t : Set α) :
s.restrict f '' (Subtype.val ⁻¹' t) = f '' (t s)
@[simp]
theorem Set.restrict_dite {α : Type u_1} {β : Type u_2} {s : Set α} [(x : α) → Decidable (x s)] (f : (a : α) → a sβ) (g : (a : α) → asβ) :
(s.restrict fun (a : α) => if h : a s then f a h else g a h) = fun (a : s) => f a
@[simp]
theorem Set.restrict_dite_compl {α : Type u_1} {β : Type u_2} {s : Set α} [(x : α) → Decidable (x s)] (f : (a : α) → a sβ) (g : (a : α) → asβ) :
(s.restrict fun (a : α) => if h : a s then f a h else g a h) = fun (a : s) => g a
@[simp]
theorem Set.restrict_ite {α : Type u_1} {β : Type u_2} (f g : αβ) (s : Set α) [(x : α) → Decidable (x s)] :
(s.restrict fun (a : α) => if a s then f a else g a) = s.restrict f
@[simp]
theorem Set.restrict_ite_compl {α : Type u_1} {β : Type u_2} (f g : αβ) (s : Set α) [(x : α) → Decidable (x s)] :
(s.restrict fun (a : α) => if a s then f a else g a) = s.restrict g
@[simp]
theorem Set.restrict_piecewise {α : Type u_1} {β : Type u_2} (f g : αβ) (s : Set α) [(x : α) → Decidable (x s)] :
@[simp]
theorem Set.restrict_piecewise_compl {α : Type u_1} {β : Type u_2} (f g : αβ) (s : Set α) [(x : α) → Decidable (x s)] :
theorem Set.restrict_extend_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ) (g : αγ) (g' : βγ) :
(range f).restrict (Function.extend f g g') = fun (x : (range f)) => g (Exists.choose )
@[simp]
theorem Set.restrict_extend_compl_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ) (g : αγ) (g' : βγ) :
def Set.restrict₂ {α : Type u_1} {π : αType u_6} {s t : Set α} (hst : s t) (f : (a : t) → π a) (a : s) :
π a

If a function f is restricted to a set t, and s ⊆ t, this is the restriction to s.

Equations
theorem Set.restrict₂_def {α : Type u_1} {π : αType u_6} {s t : Set α} (hst : s t) :
restrict₂ hst = fun (f : (a : t) → π a) (x : s) => f x,
theorem Set.restrict₂_comp_restrict {α : Type u_1} {π : αType u_6} {s t : Set α} (hst : s t) :
theorem Set.restrict₂_comp_restrict₂ {α : Type u_1} {π : αType u_6} {s t u : Set α} (hst : s t) (htu : t u) :
theorem Set.range_extend_subset {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ) (g : αγ) (g' : βγ) :
theorem Set.range_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ} (hf : Function.Injective f) (g : αγ) (g' : βγ) :
def Set.codRestrict {α : Type u_1} {ι : Sort u_5} (f : ια) (s : Set α) (h : ∀ (x : ι), f x s) :
ιs

Restrict codomain of a function f to a set s. Same as Subtype.coind but this version has codomain ↥s instead of Subtype s.

Equations
@[simp]
theorem Set.val_codRestrict_apply {α : Type u_1} {ι : Sort u_5} (f : ια) (s : Set α) (h : ∀ (x : ι), f x s) (x : ι) :
(codRestrict f s h x) = f x
@[simp]
theorem Set.restrict_comp_codRestrict {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : ια} {g : αβ} {b : Set α} (h : ∀ (x : ι), f x b) :
b.restrict g codRestrict f b h = g f
@[simp]
theorem Set.injective_codRestrict {α : Type u_1} {ι : Sort u_5} {f : ια} {s : Set α} (h : ∀ (x : ι), f x s) :
theorem Function.Injective.codRestrict {α : Type u_1} {ι : Sort u_5} {f : ια} {s : Set α} (h : ∀ (x : ι), f x s) :

Alias of the reverse direction of Set.injective_codRestrict.

Equality on a set #

@[simp]
theorem Set.eqOn_empty {α : Type u_1} {β : Type u_2} (f₁ f₂ : αβ) :
EqOn f₁ f₂
@[simp]
theorem Set.eqOn_singleton {α : Type u_1} {β : Type u_2} {f₁ f₂ : αβ} {a : α} :
EqOn f₁ f₂ {a} f₁ a = f₂ a
@[simp]
theorem Set.eqOn_univ {α : Type u_1} {β : Type u_2} (f₁ f₂ : αβ) :
EqOn f₁ f₂ 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₂ EqOn f₁ f₂ s
theorem Set.EqOn.symm {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : αβ} (h : EqOn f₁ f₂ s) :
EqOn f₂ f₁ s
theorem Set.eqOn_comm {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : αβ} :
EqOn f₁ f₂ s EqOn f₂ f₁ s
theorem Set.eqOn_refl {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
EqOn f f s
theorem Set.EqOn.trans {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ f₃ : αβ} (h₁ : EqOn f₁ f₂ s) (h₂ : EqOn f₂ f₃ s) :
EqOn f₁ f₃ s
theorem Set.EqOn.image_eq {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : αβ} (heq : EqOn f₁ f₂ s) :
f₁ '' s = f₂ '' s
theorem Set.EqOn.image_eq_self {α : Type u_1} {s : Set α} {f : αα} (h : 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 : EqOn f₁ f₂ s) (t : Set β) :
s f₁ ⁻¹' t = s f₂ ⁻¹' t
theorem Set.EqOn.mono {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {f₁ f₂ : αβ} (hs : s₁ s₂) (hf : EqOn f₁ f₂ s₂) :
EqOn f₁ f₂ s₁
@[simp]
theorem Set.eqOn_union {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {f₁ f₂ : αβ} :
EqOn f₁ f₂ (s₁ s₂) EqOn f₁ f₂ s₁ EqOn f₁ f₂ s₂
theorem Set.EqOn.union {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {f₁ f₂ : αβ} (h₁ : EqOn f₁ f₂ s₁) (h₂ : EqOn f₁ f₂ s₂) :
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 : EqOn f₁ f₂ s) :
EqOn (g f₁) (g f₂) s
@[simp]
theorem Set.eqOn_range {α : Type u_1} {β : Type u_2} {ι : Sort u_7} {f : ια} {g₁ g₂ : αβ} :
EqOn g₁ g₂ (range f) g₁ f = g₂ f
theorem Set.EqOn.comp_eq {α : Type u_1} {β : Type u_2} {ι : Sort u_7} {f : ια} {g₁ g₂ : αβ} :
EqOn g₁ g₂ (range f)g₁ f = g₂ f

Alias of the forward direction of Set.eqOn_range.

theorem Set.MapsTo.restrict_commutes {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (t : Set β) (h : MapsTo f s t) :
@[simp]
theorem Set.MapsTo.val_restrict_apply {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : MapsTo f s t) (x : s) :
(restrict f s t h x) = f x
theorem Set.MapsTo.coe_iterate_restrict {α : Type u_1} {s : Set α} {f : αα} (h : MapsTo f s s) (x : s) (k : ) :
((restrict f s s h)^[k] x) = f^[k] x
@[simp]
theorem Set.codRestrict_restrict {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : ∀ (x : s), f x t) :

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

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

Reverse of Set.codRestrict_restrict.

theorem Set.MapsTo.coe_restrict {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : MapsTo f s t) :
theorem Set.MapsTo.range_restrict {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (t : Set β) (h : MapsTo f s t) :
theorem Set.mapsTo_iff_exists_map_subtype {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} :
MapsTo f s t ∃ (g : st), ∀ (x : s), f x = (g x)
theorem Set.mapsTo' {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} :
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} {s : Set α} {t : Set β} {f : αβ} (hf : MapsTo f s t) :
s f ⁻¹' t
theorem Set.mapsTo_iff_subset_preimage {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} :
MapsTo f s t s f ⁻¹' t
@[simp]
theorem Set.mapsTo_singleton {α : Type u_1} {β : Type u_2} {t : Set β} {f : αβ} {x : α} :
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 : MapsTo f s t) (hs : s.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 : MapsTo f s t) :
f '' s t
theorem Set.MapsTo.congr {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f₁ f₂ : αβ} (h₁ : MapsTo f₁ s t) (h : EqOn f₁ f₂ s) :
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 : EqOn g₁ g₂ t) (hf : MapsTo f s t) :
EqOn (g₁ f) (g₂ f) s
theorem Set.EqOn.mapsTo_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f₁ f₂ : αβ} (H : EqOn f₁ f₂ s) :
MapsTo f₁ s t 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₁ : MapsTo g t p) (h₂ : MapsTo f s t) :
MapsTo (g f) s p
theorem Set.mapsTo_id {α : Type u_1} (s : Set α) :
theorem Set.MapsTo.iterate {α : Type u_1} {f : αα} {s : Set α} (h : MapsTo f s s) (n : ) :
MapsTo f^[n] s s
theorem Set.MapsTo.iterate_restrict {α : Type u_1} {f : αα} {s : Set α} (h : MapsTo f s s) (n : ) :
(restrict f s s h)^[n] = restrict f^[n] s s
theorem Set.mapsTo_of_subsingleton' {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} [Subsingleton β] (f : αβ) (h : s.Nonemptyt.Nonempty) :
MapsTo f s t
theorem Set.mapsTo_of_subsingleton {α : Type u_1} [Subsingleton α] (f : αα) (s : Set α) :
MapsTo f s s
theorem Set.MapsTo.mono {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : αβ} (hf : MapsTo f s₁ t₁) (hs : s₂ s₁) (ht : t₁ t₂) :
MapsTo f s₂ t₂
theorem Set.MapsTo.mono_left {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t : Set β} {f : αβ} (hf : MapsTo f s₁ t) (hs : s₂ s₁) :
MapsTo f s₂ t
theorem Set.MapsTo.mono_right {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ t₂ : Set β} {f : αβ} (hf : MapsTo f s t₁) (ht : t₁ t₂) :
MapsTo f s t₂
theorem Set.MapsTo.union_union {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : αβ} (h₁ : MapsTo f s₁ t₁) (h₂ : MapsTo f s₂ t₂) :
MapsTo f (s₁ s₂) (t₁ t₂)
theorem Set.MapsTo.union {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t : Set β} {f : αβ} (h₁ : MapsTo f s₁ t) (h₂ : MapsTo f s₂ t) :
MapsTo f (s₁ s₂) t
@[simp]
theorem Set.mapsTo_union {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t : Set β} {f : αβ} :
MapsTo f (s₁ s₂) t MapsTo f s₁ t MapsTo f s₂ t
theorem Set.MapsTo.inter {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ t₂ : Set β} {f : αβ} (h₁ : MapsTo f s t₁) (h₂ : MapsTo f s t₂) :
MapsTo f s (t₁ t₂)
theorem Set.MapsTo.insert {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : MapsTo f s t) (x : α) :
theorem Set.MapsTo.inter_inter {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : αβ} (h₁ : MapsTo f s₁ t₁) (h₂ : MapsTo f s₂ t₂) :
MapsTo f (s₁ s₂) (t₁ t₂)
@[simp]
theorem Set.mapsTo_inter {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ t₂ : Set β} {f : αβ} :
MapsTo f s (t₁ t₂) MapsTo f s t₁ MapsTo f s t₂
theorem Set.mapsTo_univ {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
theorem Set.mapsTo_range {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
MapsTo f s (range f)
@[simp]
theorem Set.mapsTo_image_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ} {g : γα} {s : Set γ} {t : Set β} :
MapsTo f (g '' s) t 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 : MapsTo f s t) :
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 : MapsTo g s t) (f : αβ) :
MapsTo (g f) (f ⁻¹' s) t
@[simp]
theorem Set.mapsTo_univ_iff {α : Type u_1} {β : Type u_2} {t : Set β} {f : αβ} :
MapsTo f univ t ∀ (x : α), f x t
@[simp]
theorem Set.mapsTo_range_iff {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {t : Set β} {f : αβ} {g : ια} :
MapsTo f (range g) t ∀ (i : ι), f (g i) t
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 : MapsTo f s t) (hc : 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 : αβ) :
theorem Set.range_restrictPreimage {α : Type u_1} {β : Type u_2} (t : Set β) (f : αβ) :
@[simp]
theorem Set.restrictPreimage_mk {α : Type u_1} {β : Type u_2} (t : Set β) {f : αβ} {a : α} (h : a f ⁻¹' t) :
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} :
theorem Set.preimage_restrictPreimage {α : Type u_1} {β : Type u_2} (t : Set β) {f : αβ} {u : Set t} :
t.restrictPreimage f ⁻¹' u = (fun (a : ↑(f ⁻¹' t)) => f a) ⁻¹' (Subtype.val '' u)
theorem Set.restrictPreimage_injective {α : Type u_1} {β : Type u_2} (t : Set β) {f : αβ} (hf : Function.Injective f) :
theorem Set.restrictPreimage_surjective {α : Type u_1} {β : Type u_2} (t : Set β) {f : αβ} (hf : Function.Surjective f) :
theorem Set.restrictPreimage_bijective {α : Type u_1} {β : Type u_2} (t : Set β) {f : αβ} (hf : Function.Bijective f) :
theorem Function.Injective.restrictPreimage {α : Type u_1} {β : Type u_2} (t : Set β) {f : αβ} (hf : Injective f) :

Alias of Set.restrictPreimage_injective.

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

Alias of Set.restrictPreimage_surjective.

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

Alias of Set.restrictPreimage_bijective.

Injectivity on a set #

theorem Set.Subsingleton.injOn {α : Type u_1} {β : Type u_2} {s : Set α} (hs : s.Subsingleton) (f : αβ) :
InjOn f s
@[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 : α) :
@[simp]
theorem Set.injOn_pair {α : Type u_1} {β : Type u_2} {f : αβ} {a b : α} :
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 : 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 : 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 : 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₁ : InjOn f₁ s) (h : EqOn f₁ f₂ s) :
InjOn f₂ s
theorem Set.EqOn.injOn_iff {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : αβ} (H : EqOn f₁ f₂ s) :
InjOn f₁ s InjOn f₂ s
theorem Set.InjOn.mono {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {f : αβ} (h : s₁ s₂) (ht : InjOn f s₂) :
InjOn f s₁
theorem Set.injOn_union {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {f : αβ} (h : Disjoint s₁ s₂) :
InjOn f (s₁ s₂) InjOn f s₁ 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) :
InjOn f (insert a s) 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 α} :
InjOn f s
theorem Function.Injective.injOn {α : Type u_1} {β : Type u_2} {f : αβ} (h : 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 }} :
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 : InjOn g t) (hf : InjOn f s) (h : MapsTo f s t) :
InjOn (g f) s
theorem Set.InjOn.of_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {f : αβ} {g : βγ} (h : InjOn (g f) s) :
InjOn f s
theorem Set.InjOn.image_of_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {f : αβ} {g : βγ} (h : InjOn (g f) s) :
InjOn g (f '' s)
theorem Set.InjOn.iterate {α : Type u_1} {f : αα} {s : Set α} (h : InjOn f s) (hf : MapsTo f s s) (n : ) :
theorem Set.injOn_of_subsingleton {α : Type u_1} {β : Type u_2} [Subsingleton α] (f : αβ) (s : Set α) :
InjOn f s
theorem Function.Injective.injOn_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ} {g : βγ} (h : Injective (g f)) :
theorem Set.InjOn.injective_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ} {g : βγ} (s : Set β) (h : InjOn g s) (hs : range f s) :
theorem Set.injOn_iff_injective {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} :
theorem Set.InjOn.injective {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} :

Alias of the forward direction of Set.injOn_iff_injective.

theorem Set.MapsTo.restrict_inj {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : MapsTo f s t) :
theorem Set.exists_injOn_iff_injective {α : Type u_1} {β : Type u_2} {s : Set α} [Nonempty β] :
(∃ (f : αβ), InjOn f s) ∃ (f : sβ), Function.Injective f
theorem Set.injOn_preimage {α : Type u_1} {β : Type u_2} {f : αβ} {B : Set (Set β)} (hB : B 𝒫 range f) :
theorem Set.InjOn.mem_of_mem_image {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {f : αβ} {x : α} (hf : 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 s₁ : Set α} {f : αβ} {x : α} (hf : 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 s₁ : Set α} {f : αβ} (hf : 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 : EqOn (g f₁) (g f₂) s) (hg : InjOn g t) (hf₁ : MapsTo f₁ s t) (hf₂ : MapsTo f₂ s t) :
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 : InjOn g t) (hf₁ : MapsTo f₁ s t) (hf₂ : MapsTo f₂ s t) :
EqOn (g f₁) (g f₂) s EqOn f₁ f₂ s
theorem Set.InjOn.image_inter {α : Type u_1} {β : Type u_2} {f : αβ} {s t u : Set α} (hf : 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 : InjOn f s) :
theorem Set.InjOn.image_eq_image_iff {α : Type u_1} {β : Type u_2} {s s₁ s₂ : Set α} {f : αβ} (h : 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 s₁ s₂ : Set α} {f : αβ} (h : 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 s₁ s₂ : Set α} {f : αβ} (h : 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 t 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 : 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 : InjOn f s) (hst : t s) :
f '' (s \ t) = f '' s \ f '' t
theorem Set.image_diff_of_injOn {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {t : Set α} (h : InjOn f s) (hst : t s) :
f '' (s \ t) = f '' s \ f '' t

Alias of Set.InjOn.image_diff_subset.

theorem Set.InjOn.imageFactorization_injective {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} (h : InjOn f s) :
@[simp]
theorem Set.imageFactorization_injective_iff {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} :
@[simp]
theorem Set.mem_graphOn {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {x : α × β} :
x graphOn f s x.1 s f x.1 = x.2
@[simp]
theorem Set.graphOn_empty {α : Type u_1} {β : Type u_2} (f : αβ) :
@[simp]
theorem Set.graphOn_eq_empty {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} :
@[simp]
theorem Set.graphOn_nonempty {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} :
theorem Set.Nonempty.graphOn {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} :

Alias of the reverse direction of Set.graphOn_nonempty.

@[simp]
theorem Set.graphOn_union {α : Type u_1} {β : Type u_2} (f : αβ) (s t : Set α) :
graphOn f (s t) = graphOn f s graphOn f t
@[simp]
theorem Set.graphOn_singleton {α : Type u_1} {β : Type u_2} (f : αβ) (x : α) :
graphOn f {x} = {(x, f x)}
@[simp]
theorem Set.graphOn_insert {α : Type u_1} {β : Type u_2} (f : αβ) (x : α) (s : Set α) :
graphOn f (insert x s) = insert (x, f x) (graphOn f s)
@[simp]
theorem Set.image_fst_graphOn {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
@[simp]
theorem Set.image_snd_graphOn {α : Type u_1} {β : Type u_2} {s : Set α} (f : αβ) :
theorem Set.fst_injOn_graph {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} :
theorem Set.graphOn_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : Set α) (f : αβ) (g : βγ) :
graphOn (g f) s = (fun (x : α × β) => (x.1, g x.2)) '' graphOn f s
theorem Set.graphOn_univ_eq_range {α : Type u_1} {β : Type u_2} {f : αβ} :
graphOn f univ = range fun (x : α) => (x, f x)
@[simp]
theorem Set.graphOn_inj {α : Type u_1} {β : Type u_2} {s : Set α} {f g : αβ} :
graphOn f s = graphOn g s EqOn f g s
theorem Set.graphOn_univ_inj {α : Type u_1} {β : Type u_2} {f g : αβ} :
theorem Set.graphOn_univ_injective {α : Type u_1} {β : Type u_2} :
Function.Injective fun (f : αβ) => graphOn f univ
theorem Set.exists_eq_graphOn_image_fst {α : Type u_1} {β : Type u_2} [Nonempty β] {s : Set (α × β)} :
(∃ (f : αβ), s = graphOn f (Prod.fst '' s)) InjOn Prod.fst s
theorem Set.exists_eq_graphOn {α : Type u_1} {β : Type u_2} [Nonempty β] {s : Set (α × β)} :
(∃ (f : αβ) (t : Set α), s = graphOn f t) InjOn Prod.fst s
theorem Set.graphOn_prod_graphOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (s : Set α) (t : Set β) (f : αγ) (g : βδ) :
graphOn f s ×ˢ graphOn g t = (Equiv.prodProdProdComm α γ β δ) ⁻¹' graphOn (Prod.map f g) (s ×ˢ t)
theorem Set.graphOn_prod_prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (s : Set α) (t : Set β) (f : αγ) (g : βδ) :
graphOn (Prod.map f g) (s ×ˢ t) = (Equiv.prodProdProdComm α β γ δ) ⁻¹' graphOn f s ×ˢ graphOn g t

Surjectivity on a set #

theorem Set.SurjOn.subset_range {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : SurjOn f s t) :
theorem Set.surjOn_iff_exists_map_subtype {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} :
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 : β} :
SurjOn f s {b} b f '' s
theorem Set.surjOn_image {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
SurjOn f s (f '' s)
theorem Set.SurjOn.comap_nonempty {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : SurjOn f s t) (ht : t.Nonempty) :
theorem Set.SurjOn.congr {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f₁ f₂ : αβ} (h : SurjOn f₁ s t) (H : EqOn f₁ f₂ s) :
SurjOn f₂ s t
theorem Set.EqOn.surjOn_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f₁ f₂ : αβ} (h : EqOn f₁ f₂ s) :
SurjOn f₁ s t SurjOn f₂ s t
theorem Set.SurjOn.mono {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : αβ} (hs : s₁ s₂) (ht : t₁ t₂) (hf : SurjOn f s₁ t₂) :
SurjOn f s₂ t₁
theorem Set.SurjOn.union {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ t₂ : Set β} {f : αβ} (h₁ : SurjOn f s t₁) (h₂ : SurjOn f s t₂) :
SurjOn f s (t₁ t₂)
theorem Set.SurjOn.union_union {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : αβ} (h₁ : SurjOn f s₁ t₁) (h₂ : SurjOn f s₂ t₂) :
SurjOn f (s₁ s₂) (t₁ t₂)
theorem Set.SurjOn.inter_inter {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : αβ} (h₁ : SurjOn f s₁ t₁) (h₂ : SurjOn f s₂ t₂) (h : InjOn f (s₁ s₂)) :
SurjOn f (s₁ s₂) (t₁ t₂)
theorem Set.SurjOn.inter {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t : Set β} {f : αβ} (h₁ : SurjOn f s₁ t) (h₂ : SurjOn f s₂ t) (h : InjOn f (s₁ s₂)) :
SurjOn f (s₁ s₂) t
theorem Set.surjOn_id {α : Type u_1} (s : Set α) :
theorem Set.SurjOn.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {p : Set γ} {f : αβ} {g : βγ} (hg : SurjOn g t p) (hf : SurjOn f s t) :
SurjOn (g f) s p
theorem Set.SurjOn.of_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {p : Set γ} {f : αβ} {g : βγ} (h : SurjOn (g f) s p) (hr : MapsTo f s t) :
SurjOn g t p
theorem Set.SurjOn.iterate {α : Type u_1} {f : αα} {s : Set α} (h : SurjOn f s s) (n : ) :
SurjOn f^[n] s s
theorem Set.SurjOn.comp_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : αβ} (hf : SurjOn f s t) (g : βγ) :
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 : SurjOn g s t) :
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) :
SurjOn f s t
theorem Set.surjOn_of_subsingleton {α : Type u_1} [Subsingleton α] (f : αα) (s : Set α) :
SurjOn f s s
theorem Set.surjective_iff_surjOn_univ {α : Type u_1} {β : Type u_2} {f : αβ} :
theorem Set.surjOn_iff_surjective {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} :
@[simp]
theorem Set.MapsTo.restrict_surjective_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : MapsTo f s t) :
theorem Set.SurjOn.image_eq_of_mapsTo {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h₁ : SurjOn f s t) (h₂ : 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 SurjOn f s t MapsTo f s t
theorem Set.SurjOn.image_preimage {α : Type u_1} {β : Type u_2} {s : Set α} {t t₁ : Set β} {f : αβ} (h : 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 : 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 : 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 : EqOn (g₁ f) (g₂ f) s) (hf' : SurjOn f s t) :
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 : SurjOn f s t) (hf' : MapsTo f s t) :
EqOn (g₁ f) (g₂ f) s EqOn g₁ g₂ t
theorem Set.eqOn_comp_right_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {f : αβ} {g₁ g₂ : βγ} :
EqOn (g₁ f) (g₂ f) s EqOn g₁ g₂ (f '' s)
theorem Set.SurjOn.forall {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {p : βProp} (hf : SurjOn f s t) (hf' : 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 : BijOn f s t) :
MapsTo f s t
theorem Set.BijOn.injOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : BijOn f s t) :
InjOn f s
theorem Set.BijOn.surjOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : BijOn f s t) :
SurjOn f s t
theorem Set.BijOn.mk {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h₁ : MapsTo f s t) (h₂ : InjOn f s) (h₃ : SurjOn f s t) :
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 : αβ} :
BijOn f s s =
@[simp]
theorem Set.bijOn_empty_iff_right {α : Type u_1} {β : Type u_2} {t : Set β} {f : αβ} :
BijOn f t t =
@[simp]
theorem Set.bijOn_singleton {α : Type u_1} {β : Type u_2} {f : αβ} {a : α} {b : β} :
BijOn f {a} {b} f a = b
theorem Set.BijOn.inter_mapsTo {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : αβ} (h₁ : BijOn f s₁ t₁) (h₂ : MapsTo f s₂ t₂) (h₃ : s₁ f ⁻¹' t₂ s₂) :
BijOn f (s₁ s₂) (t₁ t₂)
theorem Set.MapsTo.inter_bijOn {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : αβ} (h₁ : MapsTo f s₁ t₁) (h₂ : BijOn f s₂ t₂) (h₃ : s₂ f ⁻¹' t₁ s₁) :
BijOn f (s₁ s₂) (t₁ t₂)
theorem Set.BijOn.inter {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : αβ} (h₁ : BijOn f s₁ t₁) (h₂ : BijOn f s₂ t₂) (h : InjOn f (s₁ s₂)) :
BijOn f (s₁ s₂) (t₁ t₂)
theorem Set.BijOn.union {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : αβ} (h₁ : BijOn f s₁ t₁) (h₂ : BijOn f s₂ t₂) (h : InjOn f (s₁ s₂)) :
BijOn f (s₁ s₂) (t₁ t₂)
theorem Set.BijOn.subset_range {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : BijOn f s t) :
theorem Set.InjOn.bijOn_image {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} (h : InjOn f s) :
BijOn f s (f '' s)
theorem Set.BijOn.congr {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f₁ f₂ : αβ} (h₁ : BijOn f₁ s t) (h : EqOn f₁ f₂ s) :
BijOn f₂ s t
theorem Set.EqOn.bijOn_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f₁ f₂ : αβ} (H : EqOn f₁ f₂ s) :
BijOn f₁ s t BijOn f₂ s t
theorem Set.BijOn.image_eq {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : 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 : 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 : 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 α) :
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 : BijOn g t p) (hf : BijOn f s t) :
BijOn (g f) s p
theorem Set.BijOn.iterate {α : Type u_1} {f : αα} {s : Set α} (h : BijOn f s s) (n : ) :
BijOn f^[n] s s
theorem Set.bijOn_of_subsingleton' {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} [Subsingleton α] [Subsingleton β] (f : αβ) (h : s.Nonempty t.Nonempty) :
BijOn f s t
theorem Set.bijOn_of_subsingleton {α : Type u_1} [Subsingleton α] (f : αα) (s : Set α) :
BijOn f s s
theorem Set.BijOn.bijective {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : BijOn f s t) :
theorem Set.bijective_iff_bijOn_univ {α : Type u_1} {β : Type u_2} {f : αβ} :
theorem Function.Bijective.bijOn_univ {α : Type u_1} {β : Type u_2} {f : αβ} :

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 : 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 : BijOn f s t) (hrt : r t) :
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 : BijOn f s t) (hrs : r s) :
BijOn f r (f '' r)
theorem Set.BijOn.insert_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {a : α} (ha : as) (hfa : f at) :
BijOn f (Insert.insert a s) (Insert.insert (f a) t) BijOn f s t
theorem Set.BijOn.insert {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {a : α} (h₁ : BijOn f s t) (h₂ : f at) :
theorem Set.BijOn.sdiff_singleton {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {a : α} (h₁ : BijOn f s t) (h₂ : a s) :
BijOn f (s \ {a}) (t \ {f a})

left inverse #

theorem Set.LeftInvOn.eqOn {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {f' : βα} (h : LeftInvOn f' f s) :
EqOn (f' f) id s
theorem Set.LeftInvOn.eq {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {f' : βα} (h : 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₁ : LeftInvOn f₁' f s) {t : Set β} (h₁' : MapsTo f s t) (heq : EqOn f₁' f₂' t) :
LeftInvOn f₂' f s
theorem Set.LeftInvOn.congr_right {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : αβ} {f₁' : βα} (h₁ : LeftInvOn f₁' f₁ s) (heq : EqOn f₁ f₂ s) :
LeftInvOn f₁' f₂ s
theorem Set.LeftInvOn.injOn {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {f₁' : βα} (h : LeftInvOn f₁' f s) :
InjOn f s
theorem Set.LeftInvOn.surjOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {f' : βα} (h : LeftInvOn f' f s) (hf : MapsTo f s t) :
SurjOn f' t s
theorem Set.LeftInvOn.mapsTo {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {f' : βα} (h : LeftInvOn f' f s) (hf : SurjOn f s t) :
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' : LeftInvOn f' f s) (hg' : LeftInvOn g' g t) (hf : MapsTo f s t) :
LeftInvOn (f' g') (g f) s
theorem Set.LeftInvOn.mono {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {f : αβ} {f' : βα} (hf : LeftInvOn f' f s) (ht : s₁ s) :
LeftInvOn f' f s₁
theorem Set.LeftInvOn.image_inter' {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {f : αβ} {f' : βα} (hf : LeftInvOn f' f s) :
f '' (s₁ s) = f' ⁻¹' s₁ f '' s
theorem Set.LeftInvOn.image_inter {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {f : αβ} {f' : βα} (hf : 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 : LeftInvOn f' f s) :
f' '' (f '' s) = s
theorem Set.LeftInvOn.image_image' {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {f : αβ} {f' : βα} (hf : 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 : RightInvOn f' f t) :
EqOn (f f') id t
theorem Set.RightInvOn.eq {α : Type u_1} {β : Type u_2} {t : Set β} {f : αβ} {f' : βα} (h : 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 : LeftInvOn f' f s) :
RightInvOn f' f (f '' s)
theorem Set.RightInvOn.congr_left {α : Type u_1} {β : Type u_2} {t : Set β} {f : αβ} {f₁' f₂' : βα} (h₁ : RightInvOn f₁' f t) (heq : EqOn f₁' f₂' t) :
RightInvOn f₂' f t
theorem Set.RightInvOn.congr_right {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f₁ f₂ : αβ} {f' : βα} (h₁ : RightInvOn f' f₁ t) (hg : MapsTo f' t s) (heq : EqOn f₁ f₂ s) :
RightInvOn f' f₂ t
theorem Set.RightInvOn.surjOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {f' : βα} (hf : RightInvOn f' f t) (hf' : MapsTo f' t s) :
SurjOn f s t
theorem Set.RightInvOn.mapsTo {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {f' : βα} (h : RightInvOn f' f t) (hf : SurjOn f' t s) :
MapsTo f s t
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 : RightInvOn f' f t) (hg : RightInvOn g' g p) (g'pt : MapsTo g' p t) :
RightInvOn (f' g') (g f) p
theorem Set.RightInvOn.mono {α : Type u_1} {β : Type u_2} {t t₁ : Set β} {f : αβ} {f' : βα} (hf : RightInvOn f' f t) (ht : t₁ t) :
RightInvOn f' f t₁
theorem Set.InjOn.rightInvOn_of_leftInvOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {f' : βα} (hf : InjOn f s) (hf' : LeftInvOn f f' t) (h₁ : MapsTo f s t) (h₂ : MapsTo f' t s) :
RightInvOn f f' s
theorem Set.eqOn_of_leftInvOn_of_rightInvOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {f₁' f₂' : βα} (h₁ : LeftInvOn f₁' f s) (h₂ : RightInvOn f₂' f t) (h : MapsTo f₂' t s) :
EqOn f₁' f₂' t
theorem Set.SurjOn.leftInvOn_of_rightInvOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {f' : βα} (hf : SurjOn f s t) (hf' : RightInvOn f f' s) :
LeftInvOn f f' t

Two-side inverses #

theorem Set.invOn_id {α : Type u_1} (s : 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 : InvOn f' f s t) (hg : InvOn g' g t p) (fst : MapsTo f s t) (g'pt : MapsTo g' p t) :
InvOn (f' g') (g f) s p
theorem Set.InvOn.symm {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {f' : βα} (h : InvOn f' f s t) :
InvOn f f' t s
theorem Set.InvOn.mono {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t t₁ : Set β} {f : αβ} {f' : βα} (h : InvOn f' f s t) (hs : s₁ s) (ht : t₁ t) :
InvOn f' f s₁ t₁
theorem Set.InvOn.bijOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {f' : βα} (h : InvOn f' f s t) (hf : MapsTo f s t) (hf' : MapsTo f' t s) :
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
theorem Function.invFunOn_pos {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {b : β} [Nonempty α] (h : as, f a = b) :
invFunOn f s b s f (invFunOn f s b) = b
theorem Function.invFunOn_mem {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {b : β} [Nonempty α] (h : as, f a = b) :
invFunOn f s b s
theorem Function.invFunOn_eq {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {b : β} [Nonempty α] (h : as, f a = b) :
f (invFunOn f s b) = b
theorem Function.invFunOn_neg {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {b : β} [Nonempty α] (h : ¬as, f a = b) :
@[simp]
theorem Function.invFunOn_apply_mem {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {a : α} [Nonempty α] (h : a s) :
invFunOn f s (f a) s
theorem Function.invFunOn_apply_eq {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {a : α} [Nonempty α] (h : a s) :
f (invFunOn f s (f a)) = f a
theorem Set.InjOn.leftInvOn_invFunOn {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} [Nonempty α] (h : InjOn f s) :
theorem Set.InjOn.invFunOn_image {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {f : αβ} [Nonempty α] (h : 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 invFunOn f s '' (f '' s)) :
theorem Set.injOn_iff_invFunOn_image_image_eq_self {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} [Nonempty α] :
InjOn f s Function.invFunOn f s '' (f '' s) = s
theorem Function.invFunOn_injOn_image {α : Type u_1} {β : Type u_2} [Nonempty α] (f : αβ) (s : Set α) :
Set.InjOn (invFunOn f s) (f '' s)
theorem Function.invFunOn_image_image_subset {α : Type u_1} {β : Type u_2} [Nonempty α] (f : αβ) (s : Set α) :
invFunOn f s '' (f '' s) s
theorem Set.SurjOn.rightInvOn_invFunOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} [Nonempty α] (h : SurjOn f s t) :
theorem Set.BijOn.invOn_invFunOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} [Nonempty α] (h : BijOn f s t) :
theorem Set.SurjOn.invOn_invFunOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} [Nonempty α] (h : SurjOn f s t) :
theorem Set.SurjOn.mapsTo_invFunOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} [Nonempty α] (h : 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 : 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 : 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 : SurjOn f s t) :
theorem Set.surjOn_iff_exists_bijOn_subset {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} :
SurjOn f s t s's, BijOn f s' t
theorem Set.SurjOn.exists_bijOn_subset {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} :
SurjOn f s ts's, 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, 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 InjOn f u
theorem Set.exists_image_eq_injOn_of_subset_range {α : Type u_1} {β : Type u_2} {t : Set β} {f : αβ} (ht : t range f) :
∃ (s : Set α), f '' s = t InjOn f s
theorem Set.BijOn.exists_extend_of_subset {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t : Set β} {f : αβ} {t' : Set β} (h : BijOn f s t) (hss₁ : s s₁) (htt' : t t') (ht' : SurjOn f s₁ t') :
∃ (s' : Set α), s s' s' s₁ 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 : BijOn f s t) (htt' : t t') (ht' : t' range f) :
∃ (s' : Set α), s s' 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 : InjOn f r) (hrs : r s) :
∃ (u : Set α), r u u s f '' u = f '' s 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 : InvOn f g t s) (hf : BijOn f s t) :
BijOn g t s
theorem Set.bijOn_comm {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} {g : βα} (h : InvOn f g t s) :
BijOn f s t BijOn g t s

Piecewise defined function #

@[simp]
theorem Set.piecewise_empty {α : Type u_1} {δ : αSort u_7} (f g : (i : α) → δ i) [(i : α) → Decidable (i )] :
@[simp]
theorem Set.piecewise_univ {α : Type u_1} {δ : αSort u_7} (f g : (i : α) → δ i) [(i : α) → Decidable (i univ)] :
theorem Set.piecewise_insert_self {α : Type u_1} {δ : αSort u_7} (s : Set α) (f g : (i : α) → δ i) {j : α} [(i : α) → Decidable (i insert j s)] :
(insert j s).piecewise f g j = f j
theorem Set.piecewise_insert {α : Type u_1} {δ : αSort u_7} (s : Set α) (f 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_7} (s : Set α) (f 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_7} (s : Set α) (f 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 : αβ) :
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 : αβ) :
EqOn (s.piecewise f g) g s
theorem Set.piecewise_le {α : Type u_1} {δ : αType u_8} [(i : α) → Preorder (δ i)] {s : Set α} [(j : α) → Decidable (j s)] {f₁ f₂ 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_8} [(i : α) → Preorder (δ i)] {s : Set α} [(j : α) → Decidable (j s)] {f₁ f₂ g : (i : α) → δ i} (h₁ : is, g i f₁ i) (h₂ : is, g i f₂ i) :
g s.piecewise f₁ f₂
theorem Set.piecewise_mono {α : Type u_1} {δ : αType u_8} [(i : α) → Preorder (δ i)] {s : Set α} [(j : α) → Decidable (j s)] {f₁ f₂ g₁ g₂ : (i : α) → δ i} (h₁ : is, f₁ i g₁ i) (h₂ : is, f₂ i g₂ i) :
s.piecewise f₁ f₂ s.piecewise g₁ g₂
@[deprecated Set.piecewise_mono (since := "2024-10-06")]
theorem Set.piecewise_le_piecewise {α : Type u_1} {δ : αType u_8} [(i : α) → Preorder (δ i)] {s : Set α} [(j : α) → Decidable (j s)] {f₁ f₂ g₁ g₂ : (i : α) → δ i} (h₁ : is, f₁ i g₁ i) (h₂ : is, f₂ i g₂ i) :
s.piecewise f₁ f₂ s.piecewise g₁ g₂

Alias of Set.piecewise_mono.

@[simp]
theorem Set.piecewise_insert_of_ne {α : Type u_1} {δ : αSort u_7} (s : Set α) (f 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_7} (s : Set α) (f g : (i : α) → δ i) [(j : α) → Decidable (j s)] [(i : α) → Decidable (i s)] :
@[simp]
theorem Set.piecewise_range_comp {α : Type u_1} {β : Type u_2} {ι : Sort u_8} (f : ια) [(j : α) → Decidable (j range f)] (g₁ g₂ : αβ) :
(range f).piecewise g₁ g₂ f = g₁ f
theorem Set.MapsTo.piecewise_ite {α : Type u_1} {β : Type u_2} {s s₁ s₂ : Set α} {t t₁ t₂ : Set β} {f₁ f₂ : αβ} [(i : α) → Decidable (i s)] (h₁ : MapsTo f₁ (s₁ s) (t₁ t)) (h₂ : MapsTo f₂ (s₂ s) (t₂ t)) :
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 α} :
EqOn (s.piecewise f f') g t EqOn f g (t s) 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 t' : Set α} (h : EqOn f g (t s)) (h' : EqOn f' g (t' s)) :
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 t' : Set α} (h : EqOn f g t) (h' : EqOn f' g t') :
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_7} (s : Set α) (f g : (i : α) → δ i) [(j : α) → Decidable (j s)] {δ' : αSort u_8} (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_7} (s : Set α) (f g : (i : α) → δ i) [(j : α) → Decidable (j s)] {δ' : αSort u_8} {δ'' : αSort u_9} (f' 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_7} (s : Set α) (f g : (i : α) → δ i) [(j : α) → Decidable (j s)] {δ' : αSort u_8} (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_7} (s : Set α) (f g : (i : α) → δ i) [(j : α) → Decidable (j s)] {δ' : αSort u_8} {δ'' : αSort u_9} (f' 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_7} (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 : αβ) :
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) InjOn f s 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_8} {t : Set α} {t' : (i : α) → Set (δ i)} {f 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_8} {α : ιType u_9} (s s' : Set ι) (t 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_8} {α : ιType u_9} (s : Set ι) (t t' : (i : ι) → Set (α i)) [(x : ι) → Decidable (x s)] :
univ.pi (s.piecewise t t') = s.pi t s.pi t'
theorem Set.univ_pi_piecewise_univ {ι : Type u_8} {α : ιType u_9} (s : Set ι) (t : (i : ι) → Set (α i)) [(x : ι) → Decidable (x s)] :
univ.pi (s.piecewise t fun (x : ι) => univ) = s.pi t
theorem Function.Injective.comp_injOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ} {g : βγ} {s : Set α} (hg : Injective g) (hf : Set.InjOn f s) :
Set.InjOn (g f) s
theorem Function.Surjective.surjOn {α : Type u_1} {β : Type u_2} {f : αβ} (hf : Surjective f) (s : Set β) :
theorem Function.LeftInverse.leftInvOn {α : Type u_1} {β : Type u_2} {f : αβ} {g : βα} (h : LeftInverse f g) (s : Set β) :
theorem Function.RightInverse.rightInvOn {α : Type u_1} {β : Type u_2} {f : αβ} {g : βα} (h : RightInverse f g) (s : Set α) :
theorem Function.LeftInverse.rightInvOn_range {α : Type u_1} {β : Type u_2} {f : αβ} {g : βα} (h : LeftInverse f g) :
theorem Function.Semiconj.mapsTo_image {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {f : αβ} {s t : Set α} (h : Semiconj f fa fb) (ha : Set.MapsTo fa s t) :
Set.MapsTo fb (f '' s) (f '' t)
theorem Function.Semiconj.mapsTo_image_right {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {f : αβ} {s : Set α} {t : Set β} (h : Semiconj f fa fb) (hst : Set.MapsTo f s t) :
Set.MapsTo f (fa '' s) (fb '' t)
theorem Function.Semiconj.mapsTo_range {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {f : αβ} (h : Semiconj f fa fb) :
theorem Function.Semiconj.surjOn_image {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {f : αβ} {s t : Set α} (h : 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 : Semiconj f fa fb) (ha : Surjective fa) :
theorem Function.Semiconj.injOn_image {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {f : αβ} {s : Set α} (h : 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 : Semiconj f fa fb) (ha : Injective fa) (hf : Set.InjOn f (Set.range fa)) :
theorem Function.Semiconj.bijOn_image {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {f : αβ} {s t : Set α} (h : 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 : Semiconj f fa fb) (ha : Bijective fa) (hf : Injective f) :
theorem Function.Semiconj.mapsTo_preimage {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {f : αβ} (h : Semiconj f fa fb) {s 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 : Semiconj f fa fb) {s : Set β} (hb : Set.InjOn fb s) (hf : Set.InjOn f (f ⁻¹' s)) :
Set.InjOn fa (f ⁻¹' s)
theorem Function.update_comp_eq_of_not_mem_range' {α : Sort u_7} {β : Type u_8} {γ : βSort u_9} [DecidableEq β] (g : (b : β) → γ b) {f : αβ} {i : β} (a : γ i) (h : iSet.range f) :
(fun (j : α) => update g i a (f j)) = fun (j : α) => g (f j)
theorem Function.update_comp_eq_of_not_mem_range {α : Sort u_7} {β : Type u_8} {γ : Sort u_9} [DecidableEq β] (g : βγ) {f : αβ} {i : β} (a : γ) (h : iSet.range f) :
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.apply_eq_of_range_eq_singleton {α : Type u_1} {β : Type u_2} {f : αβ} {b : β} (h : Set.range f = {b}) (a : α) :
f a = b

Equivalences, permutations #

theorem Set.MapsTo.extendDomain {α : Type u_1} {β : Type u_2} {p : βProp} [DecidablePred p] {f : α Subtype p} {g : Equiv.Perm α} {s t : Set α} (h : MapsTo (⇑g) s t) :
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 t : Set α} (h : SurjOn (⇑g) s t) :
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 t : Set α} (h : BijOn (⇑g) s t) :
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₁ g₂ : Equiv.Perm α} {s : Set α} (h : LeftInvOn (⇑g₁) (⇑g₂) s) :
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₁ g₂ : Equiv.Perm α} {t : Set α} (h : RightInvOn (⇑g₁) (⇑g₂) t) :
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₁ g₂ : Equiv.Perm α} {s t : Set α} (h : InvOn (⇑g₁) (⇑g₂) s t) :
InvOn (⇑(g₁.extendDomain f)) (⇑(g₂.extendDomain f)) (Subtype.val f '' s) (Subtype.val f '' t)
theorem Set.InjOn.prodMap {α₁ : Type u_7} {α₂ : Type u_8} {β₁ : Type u_9} {β₂ : Type u_10} {s₁ : Set α₁} {s₂ : Set α₂} {f₁ : α₁β₁} {f₂ : α₂β₂} (h₁ : InjOn f₁ s₁) (h₂ : InjOn f₂ s₂) :
InjOn (fun (x : α₁ × α₂) => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂)
theorem Set.SurjOn.prodMap {α₁ : Type u_7} {α₂ : Type u_8} {β₁ : Type u_9} {β₂ : Type u_10} {s₁ : Set α₁} {s₂ : Set α₂} {t₁ : Set β₁} {t₂ : Set β₂} {f₁ : α₁β₁} {f₂ : α₂β₂} (h₁ : SurjOn f₁ s₁ t₁) (h₂ : SurjOn f₂ s₂ t₂) :
SurjOn (fun (x : α₁ × α₂) => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)
theorem Set.MapsTo.prodMap {α₁ : Type u_7} {α₂ : Type u_8} {β₁ : Type u_9} {β₂ : Type u_10} {s₁ : Set α₁} {s₂ : Set α₂} {t₁ : Set β₁} {t₂ : Set β₂} {f₁ : α₁β₁} {f₂ : α₂β₂} (h₁ : MapsTo f₁ s₁ t₁) (h₂ : MapsTo f₂ s₂ t₂) :
MapsTo (fun (x : α₁ × α₂) => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)
theorem Set.BijOn.prodMap {α₁ : Type u_7} {α₂ : Type u_8} {β₁ : Type u_9} {β₂ : Type u_10} {s₁ : Set α₁} {s₂ : Set α₂} {t₁ : Set β₁} {t₂ : Set β₂} {f₁ : α₁β₁} {f₂ : α₂β₂} (h₁ : BijOn f₁ s₁ t₁) (h₂ : BijOn f₂ s₂ t₂) :
BijOn (fun (x : α₁ × α₂) => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)
theorem Set.LeftInvOn.prodMap {α₁ : Type u_7} {α₂ : Type u_8} {β₁ : Type u_9} {β₂ : Type u_10} {s₁ : Set α₁} {s₂ : Set α₂} {f₁ : α₁β₁} {f₂ : α₂β₂} {g₁ : β₁α₁} {g₂ : β₂α₂} (h₁ : LeftInvOn g₁ f₁ s₁) (h₂ : LeftInvOn g₂ f₂ s₂) :
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_7} {α₂ : Type u_8} {β₁ : Type u_9} {β₂ : Type u_10} {t₁ : Set β₁} {t₂ : Set β₂} {f₁ : α₁β₁} {f₂ : α₂β₂} {g₁ : β₁α₁} {g₂ : β₂α₂} (h₁ : RightInvOn g₁ f₁ t₁) (h₂ : RightInvOn g₂ f₂ t₂) :
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_7} {α₂ : Type u_8} {β₁ : Type u_9} {β₂ : Type u_10} {s₁ : Set α₁} {s₂ : Set α₂} {t₁ : Set β₁} {t₂ : Set β₂} {f₁ : α₁β₁} {f₂ : α₂β₂} {g₁ : β₁α₁} {g₂ : β₂α₂} (h₁ : InvOn g₁ f₁ s₁ t₁) (h₂ : InvOn g₂ f₂ s₂ t₂) :
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.equiv_symm {α : Type u_1} {β : Type u_2} {e : α β} {s : Set α} {t : Set β} :
BijOn (⇑e) s tBijOn (⇑e.symm) t s

Alias of the reverse direction of Equiv.bijOn_symm.

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

Alias of the forward direction of Equiv.bijOn_symm.

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

Vertical line test #

theorem Set.exists_range_eq_graphOn_univ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ × γ} (hf₁ : Function.Surjective (Prod.fst f)) (hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1(f g₁).2 = (f g₂).2) :
∃ (f' : βγ), range f = graphOn f' univ

Vertical line test for functions.

Let f : α → β × γ be a function to a product. Assume that f is surjective on the first factor and that the image of f intersects every "vertical line" {(b, c) | c : γ} at most once. Then the image of f is the graph of some monoid homomorphism f' : β → γ.

theorem Set.exists_equiv_range_eq_graphOn_univ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ × γ} (hf₁ : Function.Surjective (Prod.fst f)) (hf₂ : Function.Surjective (Prod.snd f)) (hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 (f g₁).2 = (f g₂).2) :
∃ (e : β γ), range f = graphOn (⇑e) univ

Line test for equivalences.

Let f : α → β × γ be a homomorphism to a product of monoids. Assume that f is surjective on both factors and that the image of f intersects every "vertical line" {(b, c) | c : γ} and every "horizontal line" {(b, c) | b : β} at most once. Then the image of f is the graph of some equivalence f' : β ≃ γ.

theorem Set.exists_eq_mgraphOn_univ {β : Type u_2} {γ : Type u_3} {s : Set (β × γ)} (hs₁ : Function.Bijective (Prod.fst Subtype.val)) :
∃ (f : βγ), s = graphOn f univ

Vertical line test for functions.

Let s : Set (β × γ) be a set in a product. Assume that s maps bijectively to the first factor. Then s is the graph of some function f : β → γ.