Documentation

Mathlib.Data.Set.Function

Functions over sets #

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

Equality on a set #

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

source
@[simp]
theorem Set.eqOn_empty {α : Type u_1} {β : Type u_2} (f₁ f₂ : α → β) :
EqOn f₁ f₂ ∅
source
@[simp]
theorem Set.eqOn_singleton {α : Type u_1} {β : Type u_2} {f₁ f₂ : α → β} {a : α} :
EqOn f₁ f₂ {a} ↔ f₁ a = f₂ a
source
@[simp]
theorem Set.eqOn_univ {α : Type u_1} {β : Type u_2} (f₁ f₂ : α → β) :
EqOn f₁ f₂ univ ↔ f₁ = f₂
source
theorem Set.EqOn.symm {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} (h : EqOn f₁ f₂ s) :
EqOn f₂ f₁ s
source
theorem Set.eqOn_comm {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} :
EqOn f₁ f₂ s ↔ EqOn f₂ f₁ s
source
theorem Set.eqOn_refl {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) :
EqOn f f s
source
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
source
theorem Set.EqOn.image_eq {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} (heq : EqOn f₁ f₂ s) :
f₁ '' s = f₂ '' s
source
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.

source
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
source
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₁
source
@[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₂
source
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₂)
source
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
source
@[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
source
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.

source
theorem Set.mapsTo_iff_image_subset {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} :
MapsTo f s t ↔ f '' s ⊆ t
source
@[deprecated Set.mapsTo_iff_image_subset (since := "2025-08-30")]
theorem Set.mapsTo' {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} :
MapsTo f s t ↔ f '' s ⊆ t

Alias of Set.mapsTo_iff_image_subset.

source
theorem Set.mapsTo_prodMap_diagonal {α : Type u_1} {β : Type u_2} {f : α → β} :
MapsTo (Prod.map f f) (diagonal α) (diagonal β)
source
@[deprecated Set.mapsTo_prodMap_diagonal (since := "2025-04-18")]
theorem Set.mapsTo_prod_map_diagonal {α : Type u_1} {β : Type u_2} {f : α → β} :
MapsTo (Prod.map f f) (diagonal α) (diagonal β)

Alias of Set.mapsTo_prodMap_diagonal.

source
theorem Set.MapsTo.subset_preimage {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (hf : MapsTo f s t) :
s ⊆ f ⁻¹' t
source
theorem Set.mapsTo_iff_subset_preimage {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} :
MapsTo f s t ↔ s ⊆ f ⁻¹' t
source
@[simp]
theorem Set.mapsTo_singleton {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β} {x : α} :
MapsTo f {x} t ↔ f x ∈ t
source
theorem Set.mapsTo_empty {α : Type u_1} {β : Type u_2} (f : α → β) (t : Set β) :
MapsTo f ∅ t
source
@[simp]
theorem Set.mapsTo_empty_iff {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} :
MapsTo f s ∅ ↔ s = ∅
source
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.

source
theorem Set.MapsTo.image_subset {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : MapsTo f s t) :
f '' s ⊆ t
source
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
source
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
source
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
source
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
source
theorem Set.mapsTo_id {α : Type u_1} (s : Set α) :
MapsTo id s s
source
theorem Set.MapsTo.iterate {α : Type u_1} {f : α → α} {s : Set α} (h : MapsTo f s s) (n : ℕ) :
MapsTo f^[n] s s
source
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 ⋯
source
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
source
theorem Set.mapsTo_of_subsingleton {α : Type u_1} [Subsingleton α] (f : α → α) (s : Set α) :
MapsTo f s s
source
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₂
source
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
source
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₂
source
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₂)
source
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
source
@[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
source
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₂)
source
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)
source
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₂)
source
@[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₂
source
theorem Set.mapsTo_univ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) :
MapsTo f s univ
source
theorem Set.mapsTo_range {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) :
MapsTo f s (range f)
source
@[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
source
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)
source
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
source
@[simp]
theorem Set.mapsTo_univ_iff {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β} :
MapsTo f univ t ↔ ∀ (x : α), f x ∈ t
source
@[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
source
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 #

source
theorem Set.Subsingleton.injOn {α : Type u_1} {β : Type u_2} {s : Set α} (hs : s.Subsingleton) (f : α → β) :
InjOn f s
source
@[simp]
theorem Set.injOn_empty {α : Type u_1} {β : Type u_2} (f : α → β) :
InjOn f ∅
source
@[simp]
theorem Set.injOn_singleton {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) :
InjOn f {a}
source
@[simp]
theorem Set.injOn_pair {α : Type u_1} {β : Type u_2} {f : α → β} {a b : α} :
InjOn f {a, b} ↔ f a = f b → a = b
source
@[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
source
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
source
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
source
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.

source
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
source
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
source
theorem Set.InjOn.mono {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {f : α → β} (h : s₁ ⊆ s₂) (ht : InjOn f s₂) :
InjOn f s₁
source
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 ∈ s₁, ∀ y ∈ s₂, f x ≠ f y
source
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
source
theorem Set.injective_iff_injOn_univ {α : Type u_1} {β : Type u_2} {f : α → β} :
Function.Injective f ↔ InjOn f univ
source
theorem Set.injOn_of_injective {α : Type u_1} {β : Type u_2} {f : α → β} (h : Function.Injective f) {s : Set α} :
InjOn f s
source
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.

source
theorem Set.injOn_subtype_val {γ : Type u_3} {p : Set γ} {s : Set { x : γ // p x }} :
InjOn Subtype.val s
source
theorem Set.injOn_id {α : Type u_1} (s : Set α) :
InjOn id s
source
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
source
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
source
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)
source
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)
source
theorem Set.InjOn.iterate {α : Type u_1} {f : α → α} {s : Set α} (h : InjOn f s) (hf : MapsTo f s s) (n : ℕ) :
InjOn f^[n] s
source
theorem Set.injOn_of_subsingleton {α : Type u_1} {β : Type u_2} [Subsingleton α] (f : α → β) (s : Set α) :
InjOn f s
source
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)
source
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
source
theorem Set.exists_injOn_iff_injective {α : Type u_1} {β : Type u_2} {s : Set α} [Nonempty β] :
(∃ (f : α → β), InjOn f s) ↔ ∃ (f : ↑s → β), Function.Injective f
source
theorem Set.injOn_preimage {α : Type u_1} {β : Type u_2} {f : α → β} {B : Set (Set β)} (hB : B ⊆ 𝒫 range f) :
InjOn (preimage f) B
source
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₁
source
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₁
source
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₁
source
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
source
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
source
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
source
theorem Set.InjOn.image {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} (h : InjOn f s) :
InjOn (Set.image f) (𝒫 s)
source
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₂
source
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₂
source
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₂
source
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)
source
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)
source
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
source
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.

source
theorem Set.InjOn.imageFactorization_injective {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} (h : InjOn f s) :
Function.Injective (imageFactorization f s)
source
@[simp]
theorem Set.imageFactorization_injective_iff {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} :
Function.Injective (imageFactorization f s) ↔ InjOn f s
source
theorem Set.graphOn_univ_inj {α : Type u_1} {β : Type u_2} {f g : α → β} :
graphOn f univ = graphOn g univ ↔ f = g
source
theorem Set.graphOn_univ_injective {α : Type u_1} {β : Type u_2} :
Function.Injective fun (f : α → β) => graphOn f univ
source
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
source
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 #

source
theorem Set.SurjOn.subset_range {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : SurjOn f s t) :
t ⊆ range f
source
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)
source
theorem Set.surjOn_empty {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) :
SurjOn f s ∅
source
@[simp]
theorem Set.surjOn_empty_iff {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β} :
SurjOn f ∅ t ↔ t = ∅
source
@[simp]
theorem Set.surjOn_singleton {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {b : β} :
SurjOn f s {b} ↔ b ∈ f '' s
source
@[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
source
theorem Set.surjOn_image {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) :
SurjOn f s (f '' s)
source
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
source
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
source
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
source
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₁
source
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₂)
source
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₂)
source
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₂)
source
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
source
theorem Set.surjOn_id {α : Type u_1} (s : Set α) :
SurjOn id s s
source
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
source
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
source
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
source
theorem Set.SurjOn.iterate {α : Type u_1} {f : α → α} {s : Set α} (h : SurjOn f s s) (n : ℕ) :
SurjOn f^[n] s s
source
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)
source
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
source
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
source
theorem Set.surjOn_of_subsingleton {α : Type u_1} [Subsingleton α] (f : α → α) (s : Set α) :
SurjOn f s s
source
theorem Set.surjective_iff_surjOn_univ {α : Type u_1} {β : Type u_2} {f : α → β} :
Function.Surjective f ↔ SurjOn f univ univ
source
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
source
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
source
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₁
source
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ᶜ
source
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ᶜ
source
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
source
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
source
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)
source
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 ∈ t, p y) ↔ ∀ x ∈ s, p (f x)

Bijectivity #

source
theorem Set.BijOn.mapsTo {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : BijOn f s t) :
MapsTo f s t
source
theorem Set.BijOn.injOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : BijOn f s t) :
InjOn f s
source
theorem Set.BijOn.surjOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : BijOn f s t) :
SurjOn f s t
source
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
source
theorem Set.bijOn_empty {α : Type u_1} {β : Type u_2} (f : α → β) :
BijOn f ∅ ∅
source
@[simp]
theorem Set.bijOn_empty_iff_left {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} :
BijOn f s ∅ ↔ s = ∅
source
@[simp]
theorem Set.bijOn_empty_iff_right {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β} :
BijOn f ∅ t ↔ t = ∅
source
@[simp]
theorem Set.bijOn_singleton {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} {b : β} :
BijOn f {a} {b} ↔ f a = b
source
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₂)
source
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₂)
source
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₂)
source
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₂)
source
theorem Set.BijOn.subset_range {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : BijOn f s t) :
t ⊆ range f
source
theorem Set.InjOn.bijOn_image {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} (h : InjOn f s) :
BijOn f s (f '' s)
source
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
source
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
source
theorem Set.BijOn.image_eq {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : BijOn f s t) :
f '' s = t
source
theorem Set.BijOn.forall {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {p : β → Prop} (hf : BijOn f s t) :
(∀ b ∈ t, p b) ↔ ∀ a ∈ s, p (f a)
source
theorem Set.BijOn.exists {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {p : β → Prop} (hf : BijOn f s t) :
(∃ b ∈ t, p b) ↔ ∃ a ∈ s, p (f a)
source
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
source
theorem Set.bijOn_id {α : Type u_1} (s : Set α) :
BijOn id s s
source
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
source
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.

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

source
theorem Set.BijOn.iterate {α : Type u_1} {f : α → α} {s : Set α} (h : BijOn f s s) (n : ℕ) :
BijOn f^[n] s s
source
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
source
theorem Set.bijOn_of_subsingleton {α : Type u_1} [Subsingleton α] (f : α → α) (s : Set α) :
BijOn f s s
source
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 ⋯)
source
theorem Set.bijective_iff_bijOn_univ {α : Type u_1} {β : Type u_2} {f : α → β} :
Function.Bijective f ↔ BijOn f univ univ
source
theorem Function.Bijective.bijOn_univ {α : Type u_1} {β : Type u_2} {f : α → β} :
Bijective f → Set.BijOn f Set.univ Set.univ

Alias of the forward direction of Set.bijective_iff_bijOn_univ.

source
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ᶜ
source
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
source
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)
source
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
source
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)
source
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 #

source
theorem Set.LeftInvOn.eqOn {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {f' : β → α} (h : LeftInvOn f' f s) :
EqOn (f' ∘ f) id s
source
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
source
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
source
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
source
theorem Set.LeftInvOn.injOn {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {f₁' : β → α} (h : LeftInvOn f₁' f s) :
InjOn f s
source
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
source
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
source
theorem Set.leftInvOn_id {α : Type u_1} (s : Set α) :
LeftInvOn id id s
source
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
source
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₁
source
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
source
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
source
theorem Set.LeftInvOn.image_image {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {f' : β → α} (hf : LeftInvOn f' f s) :
f' '' (f '' s) = s
source
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 #

source
theorem Set.RightInvOn.eqOn {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β} {f' : β → α} (h : RightInvOn f' f t) :
EqOn (f ∘ f') id t
source
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
source
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)
source
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
source
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
source
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
source
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
source
theorem Set.rightInvOn_id {α : Type u_1} (s : Set α) :
RightInvOn id id s
source
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
source
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₁
source
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
source
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
source
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 #

source
theorem Set.invOn_id {α : Type u_1} (s : Set α) :
InvOn id id s s
source
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
source
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
source
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₁
source
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 #

source
noncomputable def Function.invFunOn {α : Type u_1} {β : Type u_2} [Nonempty α] (f : α → β) (s : Set α) (b : β) :
α

Construct the inverse for a function f on domain s. This function is a right inverse of f on f '' s. For a computable version, see Function.Embedding.invOfMemRange.

Equations
Instances For
    source
    theorem Function.invFunOn_pos {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {b : β} [Nonempty α] (h : ∃ a ∈ s, f a = b) :
    invFunOn f s b ∈ s ∧ f (invFunOn f s b) = b
    source
    theorem Function.invFunOn_mem {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {b : β} [Nonempty α] (h : ∃ a ∈ s, f a = b) :
    invFunOn f s b ∈ s
    source
    theorem Function.invFunOn_eq {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {b : β} [Nonempty α] (h : ∃ a ∈ s, f a = b) :
    f (invFunOn f s b) = b
    source
    theorem Function.invFunOn_neg {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {b : β} [Nonempty α] (h : ¬∃ a ∈ s, f a = b) :
    invFunOn f s b = Classical.choice inst✝
    source
    @[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
    source
    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
    source
    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
    source
    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₁
    source
    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
    source
    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
    source
    theorem Function.invFunOn_injOn_image {α : Type u_1} {β : Type u_2} [Nonempty α] (f : α → β) (s : Set α) :
    Set.InjOn (invFunOn f s) (f '' s)
    source
    theorem Function.invFunOn_image_image_subset {α : Type u_1} {β : Type u_2} [Nonempty α] (f : α → β) (s : Set α) :
    invFunOn f s '' (f '' s) ⊆ s
    source
    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
    source
    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
    source
    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
    source
    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
    source
    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.

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

    source
    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
    source
    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
    source
    theorem Set.SurjOn.exists_bijOn_subset {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} :
    SurjOn f s t → ∃ s' ⊆ s, BijOn f s' t

    Alias of the forward direction of Set.surjOn_iff_exists_bijOn_subset.

    source
    theorem Set.exists_subset_bijOn {α : Type u_1} {β : Type u_2} (s : Set α) (f : α → β) :
    ∃ s' ⊆ s, BijOn f s' (f '' s)
    source
    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
    source
    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
    source
    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'.

    source
    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'.

    source
    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
    source
    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)ᶜ
    source
    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
    source
    @[deprecated Set.preimage_invFun_of_notMem (since := "2025-05-23")]
    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 n ∉ s) :
    Function.invFun f ⁻¹' s = f '' s

    Alias of Set.preimage_invFun_of_notMem.

    source
    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
    source
    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
    source
    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 ⊆ 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.

    source
    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
    source
    theorem Function.Surjective.surjOn {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Surjective f) (s : Set β) :
    Set.SurjOn f Set.univ s
    source
    theorem Function.LeftInverse.leftInvOn {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h : LeftInverse f g) (s : Set β) :
    Set.LeftInvOn f g s
    source
    theorem Function.RightInverse.rightInvOn {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h : RightInverse f g) (s : Set α) :
    Set.RightInvOn f g s
    source
    theorem Function.LeftInverse.rightInvOn_range {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h : LeftInverse f g) :
    Set.RightInvOn f g (Set.range g)
    source
    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)
    source
    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)
    source
    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)
    source
    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)
    source
    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)
    source
    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)
    source
    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)
    source
    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)
    source
    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)
    source
    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)
    source
    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)
    source
    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)
    source
    @[deprecated Function.update_comp_eq_of_notMem_range' (since := "2025-05-23")]
    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 : i ∉ Set.range f) :
    (fun (j : α) => update g i a (f j)) = fun (j : α) => g (f j)

    Alias of Function.update_comp_eq_of_notMem_range'.

    source
    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'

    source
    @[deprecated Function.update_comp_eq_of_notMem_range (since := "2025-05-23")]
    theorem Function.update_comp_eq_of_not_mem_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

    Alias of Function.update_comp_eq_of_notMem_range.

    Non-dependent version of Function.update_comp_eq_of_notMem_range'

    source
    theorem Function.insert_injOn {α : Type u_1} (s : Set α) :
    Set.InjOn (fun (a : α) => insert a s) sᶜ
    source
    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 #

    source
    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)
    source
    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)
    source
    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)
    source
    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)
    source
    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)
    source
    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)
    source
    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₂)
    source
    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₂)
    source
    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₂)
    source
    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₂)
    source
    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₂)
    source
    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₂)
    source
    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₂)
    source
    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
    source
    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
    source
    theorem Equiv.invOn {α : Type u_1} {β : Type u_2} (e : α ≃ β) {s : Set α} {t : Set β} :
    Set.InvOn (⇑e) (⇑e.symm) t s
    source
    theorem Equiv.bijOn_image {α : Type u_1} {β : Type u_2} (e : α ≃ β) {s : Set α} :
    Set.BijOn (⇑e) s (⇑e '' s)
    source
    theorem Equiv.bijOn_symm_image {α : Type u_1} {β : Type u_2} (e : α ≃ β) {s : Set α} :
    Set.BijOn (⇑e.symm) (⇑e '' s) s
    source
    @[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
    source
    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.

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

    source
    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