Functions over sets

This file contains basic results on the following predicates of functions and sets:

• 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.

Equality on a set

theorem Set.EqOn.eq_of_mem {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} {a : α} (h : EqOn f₁ f₂ s) (ha : a ∈ s) : f₁ a = f₂ a

This lemma exists for use by grind/aesop as a forward rule.

@[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₂

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

theorem Set.EqOn.comp_left₂ {α : Type u_7} {β : Type u_8} {δ : Type u_9} {γ : Type u_10} {op : α → β → δ} {a₁ a₂ : γ → α} {b₁ b₂ : γ → β} {s : Set γ} (ha : EqOn a₁ a₂ s) (hb : EqOn b₁ b₂ s) : EqOn (fun (x : γ) => op (a₁ x) (b₁ x)) (fun (x : γ) => op (a₂ x) (b₂ x)) 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_iff_image_subset {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} : MapsTo f s t ↔ f '' s ⊆ t

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

theorem Set.mapsTo_prodMap_diagonal {α : Type u_1} {β : Type u_2} {f : α → β} : MapsTo (Prod.map f f) (diagonal α) (diagonal β)

@[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 β) : MapsTo f ∅ t

@[simp]

theorem Set.mapsTo_empty_iff {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} : MapsTo f s ∅ ↔ s = ∅

theorem Set.MapsTo.nonempty {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : 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 : 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 α) : MapsTo id s s

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.Nonempty → t.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 : α) : MapsTo f (Insert.insert x s) (Insert.insert (f x) t)

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 α) : MapsTo f s univ

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

theorem Set.mapsTo_univ_iff_range_subset {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β} : MapsTo f univ t ↔ range f ⊆ 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.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

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 : α → β) : InjOn f ∅

@[simp]

theorem Set.injOn_singleton {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) : InjOn f {a}

@[simp]

theorem Set.injOn_pair {α : Type u_1} {β : Type u_2} {f : α → β} {a b : α} : InjOn f {a, b} ↔ f a = f b → a = b

@[simp]

theorem Set.injOn_of_eq_iff_eq {α : Type u_1} {β : Type u_2} {f : α → β} (s : Set α) (h : ∀ (x y : α), f x = f y ↔ x = y) : InjOn f s

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 ≠ y → f 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₂ ∧ ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y

theorem Set.injOn_insert {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {a : α} (has : ¬a ∈ s) : InjOn f (insert a s) ↔ InjOn f s ∧ ¬f a ∈ f '' s

@[simp]

theorem Set.injOn_univ {α : Type u_1} {β : Type u_2} {f : α → β} : InjOn f univ ↔ Function.Injective f

@[deprecated Set.injOn_univ (since := "2025-10-27")]

theorem Set.injective_iff_injOn_univ {α : Type u_1} {β : Type u_2} {f : α → β} : Function.Injective f ↔ InjOn f univ

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 α} : Set.InjOn f s

Alias of Set.injOn_of_injective.

theorem Set.injOn_subtype_val {α : Type u_1} {p : α → Prop} {s : Set { x : α // p x }} : InjOn Subtype.val s

theorem Set.injOn_id {α : Type u_1} (s : Set α) : InjOn id s

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.comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {f : α → β} {g : β → γ} (hf : InjOn f s) : 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 : ℕ) : InjOn f^[n] s

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)) : Set.InjOn g (Set.range 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) : Function.Injective (g ∘ f) ↔ Function.Injective f

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) : InjOn (preimage f) B

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) : InjOn (Set.image 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) : Function.Injective (imageFactorization f s)

@[simp]

theorem Set.imageFactorization_injective_iff {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} : Function.Injective (imageFactorization f s) ↔ InjOn f s

theorem Set.graphOn_univ_inj {α : Type u_1} {β : Type u_2} {f g : α → β} : graphOn f univ = graphOn g univ ↔ 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

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) : t ⊆ range f

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 : ↑s → ↑t'), t ⊆ t' ∧ Function.Surjective g ∧ ∀ (x : ↑s), f ↑x = ↑(g x)

theorem Set.surjOn_empty {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) : SurjOn f s ∅

@[simp]

theorem Set.surjOn_empty_iff {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β} : SurjOn f ∅ t ↔ t = ∅

@[simp]

theorem Set.surjOn_singleton {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {b : β} : SurjOn f s {b} ↔ b ∈ f '' s

@[simp]

theorem Set.surjOn_univ_of_subsingleton_nonempty {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} [Subsingleton β] [Nonempty β] : SurjOn f s univ ↔ s.Nonempty

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) : s.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 α) : 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 : 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_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {p : Set γ} {f : α → β} {g : β → γ} : SurjOn (g ∘ f) s p ↔ SurjOn g (f '' s) 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.Nonempty → s.Nonempty) : SurjOn f s t

theorem Set.surjOn_of_subsingleton {α : Type u_1} [Subsingleton α] (f : α → α) (s : Set α) : SurjOn f s s

@[simp]

theorem Set.surjOn_univ {α : Type u_1} {β : Type u_2} {f : α → β} : SurjOn f univ univ ↔ Function.Surjective f

theorem Function.Surjective.surjOn {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β} (hf : Surjective f) : Set.SurjOn f Set.univ t

theorem Set.SurjOn.surjective {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} (hf : SurjOn f s univ) : Function.Surjective f

@[deprecated Set.surjOn_univ (since := "2025-10-31")]

theorem Set.surjective_iff_surjOn_univ {α : Type u_1} {β : Type u_2} {f : α → β} : Function.Surjective f ↔ SurjOn f univ univ

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) : MapsTo f sᶜ tᶜ

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) : SurjOn f sᶜ tᶜ

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) : (∀ (y : β), y ∈ t → p y) ↔ ∀ (x : α), x ∈ s → p (f x)

theorem Subtype.coind_surjective {α : Type u_7} {β : Type u_8} {f : α → β} {p : Set β} (h : ∀ (a : α), f a ∈ p) (hf : Set.SurjOn f Set.univ p) : Function.Surjective (coind f h)

theorem Subtype.coind_bijective {α : Type u_7} {β : Type u_8} {f : α → β} {p : Set β} (h : ∀ (a : α), f a ∈ p) (hf_inj : Function.Injective f) (hf_surj : Set.SurjOn f Set.univ p) : Function.Bijective (coind f h)

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 : α → β) : BijOn 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) : t ⊆ range f

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) : (∀ (b : β), b ∈ t → p b) ↔ ∀ (a : α), a ∈ s → 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) : (∃ (b : β), b ∈ t ∧ p b) ↔ ∃ (a : α), a ∈ s ∧ 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_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {p : Set γ} {f : α → β} {g : β → γ} (hf : InjOn f s) : BijOn (g ∘ f) s p ↔ BijOn g (f '' s) p

If f : α → β and g : β → γ and if f is injective on s, then f ∘ g is a bijection on s iff g is a bijection on f '' s.

theorem Set.bijOn_image_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {s : Set α} {t : Set β} {f : α → β} {p₁ : α → γ} {p₂ : β → δ} {g : γ → δ} (comm : ∀ (a : α), p₂ (f a) = g (p₁ a)) (hbij : BijOn f s t) (hinj : InjOn g (p₁ '' s)) : BijOn g (p₁ '' s) (p₂ '' t)

If we have a commutative square

α --f--> β
|        |
p₁       p₂
|        |
\/       \/
γ --g--> δ

and f induces a bijection from s : Set α to t : Set β, then g induces a bijection from the image of s to the image of t, as long as g is is injective on the image of s.

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) : Function.Bijective (MapsTo.restrict f s t ⋯)

@[simp]

theorem Set.bijOn_univ {α : Type u_1} {β : Type u_2} {f : α → β} : BijOn f univ univ ↔ Function.Bijective f

theorem Function.Bijective.bijOn_univ {α : Type u_1} {β : Type u_2} {f : α → β} : Bijective f → Set.BijOn f Set.univ Set.univ

Alias of the reverse direction of Set.bijOn_univ.

@[deprecated Set.bijOn_univ (since := "2025-10-31")]

theorem Set.bijective_iff_bijOn_univ {α : Type u_1} {β : Type u_2} {f : α → β} : Function.Bijective f ↔ BijOn f univ 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) : BijOn f sᶜ tᶜ

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 : ¬a ∈ s) (hfa : ¬f a ∈ t) : 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 a ∈ t) : BijOn f (Insert.insert a s) (Insert.insert (f a) t)

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 α) : LeftInvOn id id s

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 α) : RightInvOn id id s

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

theorem Set.image_eq_preimage_of_leftInvOn_injOn {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} {s : Set α} (hgf : LeftInvOn g f s) (ginj : InjOn g (g ⁻¹' s)) : f '' s = g ⁻¹' s

@[deprecated Set.image_eq_preimage_of_leftInvOn_injOn (since := "2026-03-27")]

theorem Set.image_eq_preimage_of_leftInvOn_injOn_mapsTo {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} {s : Set α} (hgf : LeftInvOn g f s) (ginj : InjOn g (g ⁻¹' s)) : f '' s = g ⁻¹' s

Alias of Set.image_eq_preimage_of_leftInvOn_injOn.

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

• Function.invFunOn f s b = if h : ∃ (a : α), a ∈ s ∧ f a = b then Classical.choose h else Classical.choice inst✝

theorem Function.invFunOn_pos {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {b : β} [Nonempty α] (h : ∃ (a : α), a ∈ s ∧ 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 : ∃ (a : α), a ∈ s ∧ f a = b) : invFunOn f s b ∈ s

theorem Function.invFunOn_eq {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {b : β} [Nonempty α] (h : ∃ (a : α), a ∈ s ∧ 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 : ¬∃ (a : α), a ∈ s ∧ f a = b) : invFunOn f s b = Classical.choice inst✝

@[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) : LeftInvOn (Function.invFunOn f s) 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)) : Set.LeftInvOn (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) : RightInvOn (Function.invFunOn f s) f t

theorem Set.BijOn.invOn_invFunOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} [Nonempty α] (h : BijOn f s t) : InvOn (Function.invFunOn f s) 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) : InvOn (Function.invFunOn f s) f (Function.invFunOn f s '' t) t

theorem Set.SurjOn.mapsTo_invFunOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} [Nonempty α] (h : SurjOn f s t) : MapsTo (Function.invFunOn f s) t s

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) : BijOn f (Function.invFunOn f s '' t) t

theorem Set.surjOn_iff_exists_bijOn_subset {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} : SurjOn f s t ↔ ∃ (s' : Set α), 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 t → ∃ (s' : Set α), s' ⊆ 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' : Set α), 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) : Function.invFun f ⁻¹' s = f '' s ∪ (range f)ᶜ

theorem Set.preimage_invFun_of_notMem {α : Type u_1} {β : Type u_2} [n : Nonempty α] {f : α → β} (hf : Function.Injective f) {s : Set α} (h : ¬Classical.choice n ∈ s) : Function.invFun f ⁻¹' s = f '' s

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

theorem Set.SurjOn.exists_subset_injOn_image_eq {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (hfs : SurjOn f s t) : ∃ (u : Set α), u ⊆ s ∧ InjOn f u ∧ f '' u = t

If t ⊆ f '' s, there exists a preimage of t under f contained in s such that f restricted to u is injective.

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.LeftInverse.leftInvOn {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h : LeftInverse f g) (s : Set β) : Set.LeftInvOn f g s

theorem Function.RightInverse.rightInvOn {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h : RightInverse f g) (s : Set α) : Set.RightInvOn f g s

theorem Function.LeftInverse.rightInvOn_range {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h : LeftInverse f g) : Set.RightInvOn f g (Set.range 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) : Set.MapsTo fb (Set.range f) (Set.range f)

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) : Set.SurjOn fb (Set.range f) (Set.range f)

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)) : Set.InjOn fb (Set.range f)

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) : Set.BijOn fb (Set.range f) (Set.range 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_notMem_range' {α : Sort u_7} {β : Type u_8} {γ : β → Sort u_9} [DecidableEq β] (g : (b : β) → γ b) {f : α → β} {i : β} (a : γ i) (h : ¬i ∈ Set.range f) : (fun (j : α) => update g i a (f j)) = fun (j : α) => g (f j)

theorem Function.update_comp_eq_of_notMem_range {α : Sort u_7} {β : Type u_8} {γ : Sort u_9} [DecidableEq β] (g : β → γ) {f : α → β} {i : β} (a : γ) (h : ¬i ∈ Set.range f) : update g i a ∘ f = g ∘ f

Non-dependent version of Function.update_comp_eq_of_notMem_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 t → BijOn (⇑e.symm) t s

Alias of the reverse direction of Equiv.bijOn_symm.

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

Alias of the forward direction of Equiv.bijOn_symm.

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