Mathlib.Data.Set.Image

Set.preimage_empty theorem

: f ⁻¹' ∅ = ∅

Full source

@[simp]
theorem preimage_empty : f ⁻¹' ∅ = ∅ :=
  rfl

Preimage of Empty Set is Empty

Informal description

For any function $f : \alpha \to \beta$, the preimage of the empty set under $f$ is the empty set, i.e., $f^{-1}(\emptyset) = \emptyset$.

Set.preimage_congr theorem

{f g : α → β} {s : Set β} (h : ∀ x : α, f x = g x) : f ⁻¹' s = g ⁻¹' s

Full source

theorem preimage_congr {f g : α → β} {s : Set β} (h : ∀ x : α, f x = g x) : f ⁻¹' s = g ⁻¹' s := by
  congr with x
  simp [h]

Preimage Equality for Pointwise Equal Functions

Informal description

For any functions $f, g : \alpha \to \beta$ and any subset $s \subseteq \beta$, if $f(x) = g(x)$ for all $x \in \alpha$, then the preimages $f^{-1}(s)$ and $g^{-1}(s)$ are equal.

Set.preimage_mono theorem

{s t : Set β} (h : s ⊆ t) : f ⁻¹' s ⊆ f ⁻¹' t

Full source

@[gcongr]
theorem preimage_mono {s t : Set β} (h : s ⊆ t) : f ⁻¹' sf ⁻¹' s ⊆ f ⁻¹' t := fun _ hx => h hx

Monotonicity of Preimage under Subset Inclusion

Informal description

For any function $f : \alpha \to \beta$ and subsets $s, t \subseteq \beta$, if $s \subseteq t$, then the preimage $f^{-1}(s)$ is a subset of the preimage $f^{-1}(t)$.

Set.preimage_univ theorem

: f ⁻¹' univ = univ

Full source

@[simp, mfld_simps]
theorem preimage_univ : f ⁻¹' univ = univ :=
  rfl

Preimage of Universal Set is Universal

Informal description

For any function $f : \alpha \to \beta$, the preimage of the universal set under $f$ is equal to the universal set, i.e., $f^{-1}(\text{univ}) = \text{univ}$.

Set.subset_preimage_univ theorem

{s : Set α} : s ⊆ f ⁻¹' univ

Full source

theorem subset_preimage_univ {s : Set α} : s ⊆ f ⁻¹' univ :=
  subset_univ _

Subset Relation to Preimage of Universal Set

Informal description

For any function $f : \alpha \to \beta$ and any subset $s \subseteq \alpha$, $s$ is a subset of the preimage of the universal set under $f$, i.e., $s \subseteq f^{-1}(\text{univ})$.

Set.preimage_inter theorem

{s t : Set β} : f ⁻¹' (s ∩ t) = f ⁻¹' s ∩ f ⁻¹' t

Full source

@[simp, mfld_simps]
theorem preimage_inter {s t : Set β} : f ⁻¹' (s ∩ t) = f ⁻¹' sf ⁻¹' s ∩ f ⁻¹' t :=
  rfl

Preimage of Intersection Equals Intersection of Preimages

Informal description

For any function $f : \alpha \to \beta$ and any subsets $s, t \subseteq \beta$, the preimage of the intersection $s \cap t$ under $f$ is equal to the intersection of the preimages $f^{-1}(s) \cap f^{-1}(t)$. In symbols: $$ f^{-1}(s \cap t) = f^{-1}(s) \cap f^{-1}(t) $$

Set.preimage_union theorem

{s t : Set β} : f ⁻¹' (s ∪ t) = f ⁻¹' s ∪ f ⁻¹' t

Full source

@[simp]
theorem preimage_union {s t : Set β} : f ⁻¹' (s ∪ t) = f ⁻¹' sf ⁻¹' s ∪ f ⁻¹' t :=
  rfl

Preimage Preserves Union: $f^{-1}(s \cup t) = f^{-1}(s) \cup f^{-1}(t)$

Informal description

For any function $f : \alpha \to \beta$ and any subsets $s, t \subseteq \beta$, the preimage of the union $s \cup t$ under $f$ is equal to the union of the preimages of $s$ and $t$ under $f$. In symbols: $$ f^{-1}(s \cup t) = f^{-1}(s) \cup f^{-1}(t) $$

Set.preimage_compl theorem

{s : Set β} : f ⁻¹' sᶜ = (f ⁻¹' s)ᶜ

Full source

@[simp]
theorem preimage_compl {s : Set β} : f ⁻¹' sᶜ = (f ⁻¹' s)ᶜ :=
  rfl

Preimage of Complement Equals Complement of Preimage

Informal description

For any function $f : \alpha \to \beta$ and any subset $s \subseteq \beta$, the preimage of the complement of $s$ under $f$ is equal to the complement of the preimage of $s$ under $f$. In symbols: $$ f^{-1}(s^c) = (f^{-1}(s))^c $$

Set.preimage_diff theorem

(f : α → β) (s t : Set β) : f ⁻¹' (s \ t) = f ⁻¹' s \ f ⁻¹' t

Full source

@[simp]
theorem preimage_diff (f : α → β) (s t : Set β) : f ⁻¹' (s \ t) = f ⁻¹' sf ⁻¹' s \ f ⁻¹' t :=
  rfl

Preimage of Set Difference Equals Difference of Preimages

Informal description

For any function $f : \alpha \to \beta$ and any subsets $s, t \subseteq \beta$, the preimage of the set difference $s \setminus t$ under $f$ is equal to the set difference of the preimages of $s$ and $t$ under $f$. In symbols: $$ f^{-1}(s \setminus t) = f^{-1}(s) \setminus f^{-1}(t) $$

Set.preimage_symmDiff theorem

{f : α → β} (s t : Set β) : f ⁻¹' (s ∆ t) = (f ⁻¹' s) ∆ (f ⁻¹' t)

Full source

@[simp]
lemma preimage_symmDiff {f : α → β} (s t : Set β) : f ⁻¹' (s ∆ t) = (f ⁻¹' s) ∆ (f ⁻¹' t) :=
  rfl

Preimage of Symmetric Difference Equals Symmetric Difference of Preimages

Informal description

For any function $f : \alpha \to \beta$ and any subsets $s, t \subseteq \beta$, the preimage of the symmetric difference $s \triangle t$ under $f$ is equal to the symmetric difference of the preimages of $s$ and $t$ under $f$. In symbols: $$ f^{-1}(s \triangle t) = f^{-1}(s) \triangle f^{-1}(t) $$

Set.preimage_ite theorem

(f : α → β) (s t₁ t₂ : Set β) : f ⁻¹' s.ite t₁ t₂ = (f ⁻¹' s).ite (f ⁻¹' t₁) (f ⁻¹' t₂)

Full source

@[simp]
theorem preimage_ite (f : α → β) (s t₁ t₂ : Set β) :
    f ⁻¹' s.ite t₁ t₂ = (f ⁻¹' s).ite (f ⁻¹' t₁) (f ⁻¹' t₂) :=
  rfl

Preimage of If-Then-Else Set Operation

Informal description

For any function $f : \alpha \to \beta$ and sets $s, t_1, t_2 \subseteq \beta$, the preimage of the if-then-else set operation $\text{ite}(s, t_1, t_2)$ under $f$ is equal to the if-then-else operation applied to the preimages $f^{-1}(s)$, $f^{-1}(t_1)$, and $f^{-1}(t_2)$. In symbols: $$ f^{-1}(\text{ite}(s, t_1, t_2)) = \text{ite}(f^{-1}(s), f^{-1}(t_1), f^{-1}(t_2)) $$

Set.preimage_setOf_eq theorem

{p : α → Prop} {f : β → α} : f ⁻¹' {a | p a} = {a | p (f a)}

Full source

@[simp]
theorem preimage_setOf_eq {p : α → Prop} {f : β → α} : f ⁻¹' { a | p a } = { a | p (f a) } :=
  rfl

Preimage of a Predicate Set under a Function

Informal description

For any predicate $p : \alpha \to \text{Prop}$ and any function $f : \beta \to \alpha$, the preimage of the set $\{a \mid p a\}$ under $f$ is equal to the set $\{a \mid p (f a)\}$. In other words, $f^{-1}(\{a \mid p a\}) = \{a \mid p (f a)\}$.

Set.preimage_id_eq theorem

: preimage (id : α → α) = id

Full source

@[simp]
theorem preimage_id_eq : preimage (id : α → α) = id :=
  rfl

Preimage of Identity Function Equals Identity

Informal description

The preimage operation under the identity function $\text{id} : \alpha \to \alpha$ is equal to the identity function on sets, i.e., $\text{preimage}(\text{id}) = \text{id}$.

Set.preimage_id theorem

{s : Set α} : id ⁻¹' s = s

Full source

@[mfld_simps]
theorem preimage_id {s : Set α} : idid ⁻¹' s = s :=
  rfl

Preimage of Identity Function

Informal description

For any set $s$ of type $\alpha$, the preimage of $s$ under the identity function $\text{id} : \alpha \to \alpha$ is equal to $s$ itself, i.e., $\text{id}^{-1}(s) = s$.

Set.preimage_id' theorem

{s : Set α} : (fun x => x) ⁻¹' s = s

Full source

@[simp, mfld_simps]
theorem preimage_id' {s : Set α} : (fun x => x) ⁻¹' s = s :=
  rfl

Preimage of Identity Function via Lambda Notation

Informal description

For any set $s$ of type $\alpha$, the preimage of $s$ under the identity function $x \mapsto x$ is equal to $s$ itself, i.e., $(x \mapsto x)^{-1}(s) = s$.

Set.preimage_const_of_mem theorem

{b : β} {s : Set β} (h : b ∈ s) : (fun _ : α => b) ⁻¹' s = univ

Full source

@[simp]
theorem preimage_const_of_mem {b : β} {s : Set β} (h : b ∈ s) : (fun _ : α => b) ⁻¹' s = univ :=
  eq_univ_of_forall fun _ => h

Preimage of a Constant Function with Value in the Target Set is Universal Set

Informal description

For any element $b \in \beta$ and any subset $s \subseteq \beta$ such that $b \in s$, the preimage of $s$ under the constant function $f : \alpha \to \beta$ defined by $f(x) = b$ for all $x \in \alpha$ is equal to the universal set $\text{univ} : \text{Set } \alpha$.

Set.preimage_const_of_not_mem theorem

{b : β} {s : Set β} (h : b ∉ s) : (fun _ : α => b) ⁻¹' s = ∅

Full source

@[simp]
theorem preimage_const_of_not_mem {b : β} {s : Set β} (h : b ∉ s) : (fun _ : α => b) ⁻¹' s = ∅ :=
  eq_empty_of_subset_empty fun _ hx => h hx

Preimage of a Constant Function with Value Outside the Target Set is Empty

Informal description

For any element $b \in \beta$ and any subset $s \subseteq \beta$ such that $b \notin s$, the preimage of $s$ under the constant function $f : \alpha \to \beta$ defined by $f(x) = b$ for all $x \in \alpha$ is equal to the empty set $\emptyset$.

Set.preimage_const theorem

(b : β) (s : Set β) [Decidable (b ∈ s)] : (fun _ : α => b) ⁻¹' s = if b ∈ s then univ else ∅

Full source

theorem preimage_const (b : β) (s : Set β) [Decidable (b ∈ s)] :
    (fun _ : α => b) ⁻¹' s = if b ∈ s then univ else ∅ := by
  split_ifs with hb
  exacts [preimage_const_of_mem hb, preimage_const_of_not_mem hb]

Preimage of a Constant Function is Universal or Empty Depending on Membership

Informal description

For any element $b \in \beta$ and any subset $s \subseteq \beta$, the preimage of $s$ under the constant function $f : \alpha \to \beta$ defined by $f(x) = b$ for all $x \in \alpha$ is equal to the universal set $\text{univ}$ if $b \in s$, and is equal to the empty set $\emptyset$ otherwise.

Set.exists_eq_const_of_preimage_singleton theorem

[Nonempty β] {f : α → β} (hf : ∀ b : β, f ⁻¹' { b } = ∅ ∨ f ⁻¹' { b } = univ) : ∃ b, f = const α b

Full source

/-- If preimage of each singleton under `f : α → β` is either empty or the whole type,
then `f` is a constant. -/
lemma exists_eq_const_of_preimage_singleton [Nonempty β] {f : α → β}
    (hf : ∀ b : β, f ⁻¹' {b}f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = univ) : ∃ b, f = const α b := by
  rcases em (∃ b, f ⁻¹' {b} = univ) with ⟨b, hb⟩ | hf'
  · exact ⟨b, funext fun x ↦ eq_univ_iff_forall.1 hb x⟩
  · have : ∀ x b, f x ≠ b := fun x b ↦
      eq_empty_iff_forall_not_mem.1 ((hf b).resolve_right fun h ↦ hf' ⟨b, h⟩) x
    exact ⟨Classical.arbitrary β, funext fun x ↦ absurd rfl (this x _)⟩

Constant Function Characterization via Preimages of Singletons

Informal description

Let $\beta$ be a nonempty type and $f : \alpha \to \beta$ be a function. If for every $b \in \beta$, the preimage $f^{-1}(\{b\})$ is either empty or the entire type $\alpha$, then there exists some $b \in \beta$ such that $f$ is the constant function with value $b$.

Set.preimage_comp theorem

{s : Set γ} : g ∘ f ⁻¹' s = f ⁻¹' (g ⁻¹' s)

Full source

theorem preimage_comp {s : Set γ} : g ∘ fg ∘ f ⁻¹' s = f ⁻¹' (g ⁻¹' s) :=
  rfl

Preimage of Composition Equals Composition of Preimages

Informal description

For any functions $f : \alpha \to \beta$ and $g : \beta \to \gamma$, and any subset $s \subseteq \gamma$, the preimage of $s$ under the composition $g \circ f$ is equal to the preimage under $f$ of the preimage of $s$ under $g$, i.e., $(g \circ f)^{-1}(s) = f^{-1}(g^{-1}(s))$.

Set.preimage_comp_eq theorem

: preimage (g ∘ f) = preimage f ∘ preimage g

Full source

theorem preimage_comp_eq : preimage (g ∘ f) = preimagepreimage f ∘ preimage g :=
  rfl

Preimage of Composition Equals Composition of Preimages

Informal description

For any functions $f : \alpha \to \beta$ and $g : \beta \to \gamma$, the preimage of the composition $g \circ f$ is equal to the composition of the preimages, i.e., $(g \circ f)^{-1} = f^{-1} \circ g^{-1}$.

Set.preimage_iterate_eq theorem

{f : α → α} {n : ℕ} : Set.preimage f^[n] = (Set.preimage f)^[n]

Full source

theorem preimage_iterate_eq {f : α → α} {n : ℕ} : Set.preimage f^[n] = (Set.preimage f)^[n] := by
  induction n with
  | zero => simp
  | succ n ih => rw [iterate_succ, iterate_succ', preimage_comp_eq, ih]

Iterated Preimage Equals Preimage of Iterate

Informal description

For any function $f \colon \alpha \to \alpha$ and natural number $n$, the preimage of the $n$-th iterate of $f$ is equal to the $n$-th iterate of the preimage of $f$, i.e., $$ (f^{[n]})^{-1} = (f^{-1})^{[n]}. $$

Set.preimage_preimage theorem

{g : β → γ} {f : α → β} {s : Set γ} : f ⁻¹' (g ⁻¹' s) = (fun x => g (f x)) ⁻¹' s

Full source

theorem preimage_preimage {g : β → γ} {f : α → β} {s : Set γ} :
    f ⁻¹' (g ⁻¹' s) = (fun x => g (f x)) ⁻¹' s :=
  preimage_comp.symm

Preimage Composition Identity: $f^{-1}(g^{-1}(s)) = (g \circ f)^{-1}(s)$

Informal description

For any functions $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$, and any subset $s \subseteq \gamma$, the preimage under $f$ of the preimage of $s$ under $g$ is equal to the preimage of $s$ under the composition $g \circ f$, i.e., $$ f^{-1}(g^{-1}(s)) = (g \circ f)^{-1}(s). $$

Set.nonempty_of_nonempty_preimage theorem

{s : Set β} {f : α → β} (hf : (f ⁻¹' s).Nonempty) : s.Nonempty

Full source

theorem nonempty_of_nonempty_preimage {s : Set β} {f : α → β} (hf : (f ⁻¹' s).Nonempty) :
    s.Nonempty :=
  let ⟨x, hx⟩ := hf
  ⟨f x, hx⟩

Nonempty Preimage Implies Nonempty Image

Informal description

For any function $f : \alpha \to \beta$ and any subset $s \subseteq \beta$, if the preimage $f^{-1}(s)$ is nonempty, then $s$ is nonempty.

Set.preimage_singleton_true theorem

(p : α → Prop) : p ⁻¹' { True } = {a | p a}

Full source

@[simp] theorem preimage_singleton_true (p : α → Prop) : p ⁻¹' {True} = {a | p a} := by ext; simp

Preimage of True Singleton is the Predicate's Support

Informal description

For any predicate $p : \alpha \to \mathrm{Prop}$, the preimage of the singleton set $\{\mathrm{True}\}$ under $p$ is equal to the set $\{a \mid p(a)\}$.

Set.preimage_singleton_false theorem

(p : α → Prop) : p ⁻¹' { False } = {a | ¬p a}

Full source

@[simp] theorem preimage_singleton_false (p : α → Prop) : p ⁻¹' {False} = {a | ¬p a} := by ext; simp

Preimage of False Singleton is the Complement of the Predicate

Informal description

For any predicate $p : \alpha \to \mathrm{Prop}$, the preimage of the singleton set $\{\mathrm{False}\}$ under $p$ is equal to the set $\{a \mid \neg p(a)\}$.

Set.preimage_subtype_coe_eq_compl theorem

{s u v : Set α} (hsuv : s ⊆ u ∪ v) (H : s ∩ (u ∩ v) = ∅) : ((↑) : s → α) ⁻¹' u = ((↑) ⁻¹' v)ᶜ

Full source

theorem preimage_subtype_coe_eq_compl {s u v : Set α} (hsuv : s ⊆ u ∪ v)
    (H : s ∩ (u ∩ v) = ∅) : ((↑) : s → α) ⁻¹' u = ((↑) ⁻¹' v)ᶜ := by
  ext ⟨x, x_in_s⟩
  constructor
  · intro x_in_u x_in_v
    exact eq_empty_iff_forall_not_mem.mp H x ⟨x_in_s, ⟨x_in_u, x_in_v⟩⟩
  · intro hx
    exact Or.elim (hsuv x_in_s) id fun hx' => hx.elim hx'

Preimage Complement Relation for Disjoint Subsets under Inclusion

Informal description

Let $s$, $u$, and $v$ be subsets of a type $\alpha$ such that $s$ is contained in the union of $u$ and $v$ (i.e., $s \subseteq u \cup v$) and the intersection of $s$ with the intersection of $u$ and $v$ is empty (i.e., $s \cap (u \cap v) = \emptyset$). Then the preimage of $u$ under the canonical inclusion map from $s$ to $\alpha$ is equal to the complement of the preimage of $v$ under the same inclusion map, i.e., $$ (\uparrow)^{-1}(u) = \left((\uparrow)^{-1}(v)\right)^c. $$

Set.preimage_subset theorem

{s t} (hs : s ⊆ f '' t) (hf : Set.InjOn f (f ⁻¹' s)) : f ⁻¹' s ⊆ t

Full source

lemma preimage_subset {s t} (hs : s ⊆ f '' t) (hf : Set.InjOn f (f ⁻¹' s)) : f ⁻¹' sf ⁻¹' s ⊆ t := by
  rintro a ha
  obtain ⟨b, hb, hba⟩ := hs ha
  rwa [hf ha _ hba.symm]
  simpa [hba]

Preimage Subset under Injectivity Condition

Informal description

Let $f : \alpha \to \beta$ be a function, and let $s \subseteq \beta$ and $t \subseteq \alpha$ be subsets. If $s$ is a subset of the image of $t$ under $f$ (i.e., $s \subseteq f(t)$) and $f$ is injective on the preimage of $s$ (i.e., $f$ is injective on $f^{-1}(s)$), then the preimage of $s$ under $f$ is a subset of $t$ (i.e., $f^{-1}(s) \subseteq t$).

Set.image_eta theorem

(f : α → β) : f '' s = (fun x => f x) '' s

Full source

theorem image_eta (f : α → β) : f '' s = (fun x => f x) '' s :=
  rfl

Image Equivalence under Eta Expansion

Informal description

For any function $f : \alpha \to \beta$ and any subset $s \subseteq \alpha$, the image of $s$ under $f$ is equal to the image of $s$ under the function $\lambda x, f(x)$, i.e., $f(s) = \{f(x) \mid x \in s\}$.

Function.Injective.mem_set_image theorem

{f : α → β} (hf : Injective f) {s : Set α} {a : α} : f a ∈ f '' s ↔ a ∈ s

Full source

theorem _root_.Function.Injective.mem_set_image {f : α → β} (hf : Injective f) {s : Set α} {a : α} :
    f a ∈ f '' sf a ∈ f '' s ↔ a ∈ s :=
  ⟨fun ⟨_, hb, Eq⟩ => hf Eq ▸ hb, mem_image_of_mem f⟩

Injectivity Criterion for Set Membership via Images

Informal description

For an injective function $f \colon \alpha \to \beta$, a subset $s \subseteq \alpha$, and an element $a \in \alpha$, the image $f(a)$ belongs to the image $f(s)$ if and only if $a$ belongs to $s$. In symbols: \[ f(a) \in f(s) \leftrightarrow a \in s. \]

Set.preimage_subset_of_surjOn theorem

{t : Set β} (hf : Injective f) (h : SurjOn f s t) : f ⁻¹' t ⊆ s

Full source

lemma preimage_subset_of_surjOn {t : Set β} (hf : Injective f) (h : SurjOn f s t) :
    f ⁻¹' tf ⁻¹' t ⊆ s := fun _ hx ↦
  hf.mem_set_image.1 <| h hx

Preimage of Surjective Image is Contained in Domain

Informal description

Let $f \colon \alpha \to \beta$ be an injective function, and let $s \subseteq \alpha$ and $t \subseteq \beta$ be sets such that $f$ is surjective from $s$ to $t$ (i.e., $t \subseteq f(s)$). Then the preimage $f^{-1}(t)$ is a subset of $s$.

Set.forall_mem_image theorem

{f : α → β} {s : Set α} {p : β → Prop} : (∀ y ∈ f '' s, p y) ↔ ∀ ⦃x⦄, x ∈ s → p (f x)

Full source

theorem forall_mem_image {f : α → β} {s : Set α} {p : β → Prop} :
    (∀ y ∈ f '' s, p y) ↔ ∀ ⦃x⦄, x ∈ s → p (f x) := by simp

Universal Quantification over Image Equivalence

Informal description

For any function $f \colon \alpha \to \beta$, set $s \subseteq \alpha$, and predicate $p$ on $\beta$, the following are equivalent: 1. For every $y$ in the image $f(s)$, the predicate $p(y)$ holds. 2. For every $x \in s$, the predicate $p(f(x))$ holds. In symbols: \[ (\forall y \in f(s),\, p(y)) \leftrightarrow (\forall x \in s,\, p(f(x))). \]

Set.exists_mem_image theorem

{f : α → β} {s : Set α} {p : β → Prop} : (∃ y ∈ f '' s, p y) ↔ ∃ x ∈ s, p (f x)

Full source

theorem exists_mem_image {f : α → β} {s : Set α} {p : β → Prop} :
    (∃ y ∈ f '' s, p y) ↔ ∃ x ∈ s, p (f x) := by simp

Existence in Image Equivalence

Informal description

For any function $f : \alpha \to \beta$, set $s \subseteq \alpha$, and predicate $p$ on $\beta$, there exists an element $y$ in the image $f(s)$ such that $p(y)$ holds if and only if there exists an element $x \in s$ such that $p(f(x))$ holds.

Set.image_congr theorem

{f g : α → β} {s : Set α} (h : ∀ a ∈ s, f a = g a) : f '' s = g '' s

Full source

@[congr]
theorem image_congr {f g : α → β} {s : Set α} (h : ∀ a ∈ s, f a = g a) : f '' s = g '' s := by
  aesop

Image Equality under Pointwise Function Equality

Informal description

For any functions $f, g : \alpha \to \beta$ and set $s \subseteq \alpha$, if $f(a) = g(a)$ for all $a \in s$, then the images of $s$ under $f$ and $g$ are equal, i.e., $f(s) = g(s)$.

Set.image_congr' theorem

{f g : α → β} {s : Set α} (h : ∀ x : α, f x = g x) : f '' s = g '' s

Full source

/-- A common special case of `image_congr` -/
theorem image_congr' {f g : α → β} {s : Set α} (h : ∀ x : α, f x = g x) : f '' s = g '' s :=
  image_congr fun x _ => h x

Image Equality under Global Function Equality

Informal description

For any functions $f, g : \alpha \to \beta$ and set $s \subseteq \alpha$, if $f(x) = g(x)$ for all $x \in \alpha$, then the images of $s$ under $f$ and $g$ are equal, i.e., $f(s) = g(s)$.

Set.image_mono theorem

(h : s ⊆ t) : f '' s ⊆ f '' t

Full source

@[gcongr]
lemma image_mono (h : s ⊆ t) : f '' sf '' s ⊆ f '' t := by
  rintro - ⟨a, ha, rfl⟩; exact mem_image_of_mem f (h ha)

Monotonicity of Image under Subset Relation

Informal description

For any function $f \colon \alpha \to \beta$ and subsets $s, t \subseteq \alpha$, if $s \subseteq t$, then the image of $s$ under $f$ is a subset of the image of $t$ under $f$, i.e., $f(s) \subseteq f(t)$.

Set.image_comp theorem

(f : β → γ) (g : α → β) (a : Set α) : f ∘ g '' a = f '' (g '' a)

Full source

theorem image_comp (f : β → γ) (g : α → β) (a : Set α) : f ∘ gf ∘ g '' a = f '' (g '' a) := by aesop

Image of Composition Equals Composition of Images

Informal description

For any functions $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, and any subset $a \subseteq \alpha$, the image of $a$ under the composition $f \circ g$ is equal to the image of the image of $a$ under $g$ under $f$. In symbols: $$(f \circ g)(a) = f(g(a)).$$

Set.image_comp_eq theorem

{g : β → γ} : image (g ∘ f) = image g ∘ image f

Full source

theorem image_comp_eq {g : β → γ} : image (g ∘ f) = imageimage g ∘ image f := by ext; simp

Image of Composition Equals Composition of Images

Informal description

For any function $g : \beta \to \gamma$, the image of the composition $g \circ f$ is equal to the composition of the images, i.e., $(g \circ f)(s) = g(f(s))$ for any set $s \subseteq \alpha$.

Set.image_image theorem

(g : β → γ) (f : α → β) (s : Set α) : g '' (f '' s) = (fun x => g (f x)) '' s

Full source

/-- A variant of `image_comp`, useful for rewriting -/
theorem image_image (g : β → γ) (f : α → β) (s : Set α) : g '' (f '' s) = (fun x => g (f x)) '' s :=
  (image_comp g f s).symm

Image of Image Equals Image of Composition

Informal description

For any functions $g \colon \beta \to \gamma$ and $f \colon \alpha \to \beta$, and any subset $s \subseteq \alpha$, the image of the image of $s$ under $f$ under $g$ is equal to the image of $s$ under the composition $g \circ f$. In symbols: $$g(f(s)) = (g \circ f)(s).$$

Set.image_comm theorem

 {β'} {f : β → γ} {g : α → β} {f' : α → β'} {g' : β' → γ} (h_comm : ∀ a, f (g a) = g' (f' a)) :
  (s.image g).image f = (s.image f').image g'

Full source

theorem image_comm {β'} {f : β → γ} {g : α → β} {f' : α → β'} {g' : β' → γ}
    (h_comm : ∀ a, f (g a) = g' (f' a)) : (s.image g).image f = (s.image f').image g' := by
  simp_rw [image_image, h_comm]

Commutativity of Images under Function Composition

Informal description

For any functions $f \colon \beta \to \gamma$, $g \colon \alpha \to \beta$, $f' \colon \alpha \to \beta'$, and $g' \colon \beta' \to \gamma$, and any set $s \subseteq \alpha$, if the functions satisfy the commutation relation $f(g(a)) = g'(f'(a))$ for all $a \in \alpha$, then the images satisfy: $$f(g(s)) = g'(f'(s)).$$

Function.Semiconj.set_image theorem

 {f : α → β} {ga : α → α} {gb : β → β} (h : Function.Semiconj f ga gb) :
  Function.Semiconj (image f) (image ga) (image gb)

Full source

theorem _root_.Function.Semiconj.set_image {f : α → β} {ga : α → α} {gb : β → β}
    (h : Function.Semiconj f ga gb) : Function.Semiconj (image f) (image ga) (image gb) := fun _ =>
  image_comm h

Semiconjugacy of Image Operations under a Semiconjugate Function

Informal description

Let $f \colon \alpha \to \beta$ be a function that semiconjugates functions $g_a \colon \alpha \to \alpha$ and $g_b \colon \beta \to \beta$, i.e., $f \circ g_a = g_b \circ f$. Then the image operation under $f$ semiconjugates the image operations under $g_a$ and $g_b$, i.e., for any subset $s \subseteq \alpha$, we have: $$f(g_a(s)) = g_b(f(s)).$$

Function.Commute.set_image theorem

{f g : α → α} (h : Function.Commute f g) : Function.Commute (image f) (image g)

Full source

theorem _root_.Function.Commute.set_image {f g : α → α} (h : Function.Commute f g) :
    Function.Commute (image f) (image g) :=
  Function.Semiconj.set_image h

Commutation of Image Operations for Commuting Functions

Informal description

For any commuting functions $f, g \colon \alpha \to \alpha$ (i.e., $f \circ g = g \circ f$), the image operations under $f$ and $g$ also commute. That is, for any subset $s \subseteq \alpha$, we have: $$f(g(s)) = g(f(s)).$$

Set.image_subset theorem

{a b : Set α} (f : α → β) (h : a ⊆ b) : f '' a ⊆ f '' b

Full source

/-- Image is monotone with respect to `⊆`. See `Set.monotone_image` for the statement in
terms of `≤`. -/
@[gcongr]
theorem image_subset {a b : Set α} (f : α → β) (h : a ⊆ b) : f '' af '' a ⊆ f '' b := by
  simp only [subset_def, mem_image]
  exact fun x => fun ⟨w, h1, h2⟩ => ⟨w, h h1, h2⟩

Image Preserves Subset Relation

Informal description

For any function $f : \alpha \to \beta$ and any subsets $a, b \subseteq \alpha$ such that $a \subseteq b$, the image of $a$ under $f$ is a subset of the image of $b$ under $f$, i.e., $f(a) \subseteq f(b)$.

Set.monotone_image theorem

{f : α → β} : Monotone (image f)

Full source

/-- `Set.image` is monotone. See `Set.image_subset` for the statement in terms of `⊆`. -/
lemma monotone_image {f : α → β} : Monotone (image f) := fun _ _ => image_subset _

Monotonicity of Image Operation

Informal description

For any function $f : \alpha \to \beta$, the image operation $f$ is monotone with respect to the subset relation. That is, for any subsets $s, t \subseteq \alpha$ with $s \subseteq t$, we have $f(s) \subseteq f(t)$.

Set.image_union theorem

(f : α → β) (s t : Set α) : f '' (s ∪ t) = f '' s ∪ f '' t

Full source

theorem image_union (f : α → β) (s t : Set α) : f '' (s ∪ t) = f '' sf '' s ∪ f '' t :=
  ext fun x =>
    ⟨by rintro ⟨a, h | h, rfl⟩ <;> [left; right] <;> exact ⟨_, h, rfl⟩, by
      rintro (⟨a, h, rfl⟩ | ⟨a, h, rfl⟩) <;> refine ⟨_, ?_, rfl⟩
      · exact mem_union_left t h
      · exact mem_union_right s h⟩

Image of Union Equals Union of Images

Informal description

For any function $f : \alpha \to \beta$ and any sets $s, t \subseteq \alpha$, the image of the union $s \cup t$ under $f$ is equal to the union of the images of $s$ and $t$ under $f$, i.e., $f(s \cup t) = f(s) \cup f(t)$.

Set.image_empty theorem

(f : α → β) : f '' ∅ = ∅

Full source

@[simp]
theorem image_empty (f : α → β) : f '' ∅ = ∅ := by
  ext
  simp

Image of Empty Set is Empty

Informal description

For any function $f : \alpha \to \beta$, the image of the empty set under $f$ is the empty set, i.e., $f(\emptyset) = \emptyset$.

Set.image_inter_subset theorem

(f : α → β) (s t : Set α) : f '' (s ∩ t) ⊆ f '' s ∩ f '' t

Full source

theorem image_inter_subset (f : α → β) (s t : Set α) : f '' (s ∩ t)f '' (s ∩ t) ⊆ f '' s ∩ f '' t :=
  subset_inter (image_subset _ inter_subset_left) (image_subset _ inter_subset_right)

Image of Intersection is Subset of Intersection of Images

Informal description

For any function $f : \alpha \to \beta$ and any subsets $s, t \subseteq \alpha$, the image of the intersection $s \cap t$ under $f$ is a subset of the intersection of the images of $s$ and $t$ under $f$, i.e., $f(s \cap t) \subseteq f(s) \cap f(t)$.

Set.image_inter_on theorem

{f : α → β} {s t : Set α} (h : ∀ x ∈ t, ∀ y ∈ s, f x = f y → x = y) : f '' (s ∩ t) = f '' s ∩ f '' t

Full source

theorem image_inter_on {f : α → β} {s t : Set α} (h : ∀ x ∈ t, ∀ y ∈ s, f x = f y → x = y) :
    f '' (s ∩ t) = f '' sf '' s ∩ f '' t :=
  (image_inter_subset _ _ _).antisymm
    fun b ⟨⟨a₁, ha₁, h₁⟩, ⟨a₂, ha₂, h₂⟩⟩ ↦
      have : a₂ = a₁ := h _ ha₂ _ ha₁ (by simp [*])
      ⟨a₁, ⟨ha₁, this ▸ ha₂⟩, h₁⟩

Image of Intersection Equals Intersection of Images under Injective-like Condition

Informal description

Let $f : \alpha \to \beta$ be a function and let $s, t \subseteq \alpha$ be subsets. If for all $x \in t$ and $y \in s$, the equality $f(x) = f(y)$ implies $x = y$, then the image of the intersection $s \cap t$ under $f$ equals the intersection of the images of $s$ and $t$ under $f$, i.e., $f(s \cap t) = f(s) \cap f(t)$.

Set.image_inter theorem

{f : α → β} {s t : Set α} (H : Injective f) : f '' (s ∩ t) = f '' s ∩ f '' t

Full source

theorem image_inter {f : α → β} {s t : Set α} (H : Injective f) : f '' (s ∩ t) = f '' sf '' s ∩ f '' t :=
  image_inter_on fun _ _ _ _ h => H h

Image of Intersection Equals Intersection of Images for Injective Functions

Informal description

For any injective function $f : \alpha \to \beta$ and any subsets $s, t \subseteq \alpha$, the image of the intersection $s \cap t$ under $f$ equals the intersection of the images of $s$ and $t$ under $f$, i.e., $f(s \cap t) = f(s) \cap f(t)$.

Set.image_univ_of_surjective theorem

{ι : Type*} {f : ι → β} (H : Surjective f) : f '' univ = univ

Full source

theorem image_univ_of_surjective {ι : Type*} {f : ι → β} (H : Surjective f) : f '' univ = univ :=
  eq_univ_of_forall <| by simpa [image]

Image of Universal Set under Surjective Function is Universal Set

Informal description

For any surjective function $f : \alpha \to \beta$, the image of the universal set under $f$ is equal to the universal set, i.e., $f(\alpha) = \beta$.

Set.image_singleton theorem

{f : α → β} {a : α} : f '' { a } = {f a}

Full source

@[simp]
theorem image_singleton {f : α → β} {a : α} : f '' {a} = {f a} := by
  ext
  simp [image, eq_comm]

Image of a Singleton Set under a Function is a Singleton

Informal description

For any function $f : \alpha \to \beta$ and any element $a \in \alpha$, the image of the singleton set $\{a\}$ under $f$ is the singleton set $\{f(a)\}$.

Set.Nonempty.image_const theorem

{s : Set α} (hs : s.Nonempty) (a : β) : (fun _ => a) '' s = { a }

Full source

@[simp]
theorem Nonempty.image_const {s : Set α} (hs : s.Nonempty) (a : β) : (fun _ => a) '' s = {a} :=
  ext fun _ =>
    ⟨fun ⟨_, _, h⟩ => h ▸ mem_singleton _, fun h =>
      (eq_of_mem_singleton h).symm ▸ hs.imp fun _ hy => ⟨hy, rfl⟩⟩

Image of Nonempty Set under Constant Function is Singleton

Informal description

For any nonempty set $s \subseteq \alpha$ and any element $a \in \beta$, the image of $s$ under the constant function $\lambda \_, a$ is the singleton set $\{a\}$.

Set.image_eq_empty theorem

{α β} {f : α → β} {s : Set α} : f '' s = ∅ ↔ s = ∅

Full source

@[simp, mfld_simps]
theorem image_eq_empty {α β} {f : α → β} {s : Set α} : f '' sf '' s = ∅ ↔ s = ∅ := by
  simp only [eq_empty_iff_forall_not_mem]
  exact ⟨fun H a ha => H _ ⟨_, ha, rfl⟩, fun H b ⟨_, ha, _⟩ => H _ ha⟩

Image is Empty iff Domain is Empty

Informal description

For any function $f : \alpha \to \beta$ and any subset $s \subseteq \alpha$, the image of $s$ under $f$ is empty if and only if $s$ is empty. In symbols: $$ f(s) = \emptyset \leftrightarrow s = \emptyset $$

Set.preimage_compl_eq_image_compl theorem

[BooleanAlgebra α] (S : Set α) : HasCompl.compl ⁻¹' S = HasCompl.compl '' S

Full source

theorem preimage_compl_eq_image_compl [BooleanAlgebra α] (S : Set α) :
    HasCompl.complHasCompl.compl ⁻¹' S = HasCompl.complHasCompl.compl '' S :=
  Set.ext fun x =>
    ⟨fun h => ⟨xᶜ, h, compl_compl x⟩, fun h =>
      Exists.elim h fun _ hy => (compl_eq_comm.mp hy.2).symm.subst hy.1⟩

Preimage of Complement Equals Image of Complement in Boolean Algebra

Informal description

Let $\alpha$ be a Boolean algebra. For any subset $S \subseteq \alpha$, the preimage of $S$ under the complement operation is equal to the image of $S$ under the complement operation. In symbols: $$ \overline{S}^{-1} = \overline{S} $$ where $\overline{S}$ denotes the image of $S$ under the complement operation.

Set.mem_compl_image theorem

[BooleanAlgebra α] (t : α) (S : Set α) : t ∈ HasCompl.compl '' S ↔ tᶜ ∈ S

Full source

theorem mem_compl_image [BooleanAlgebra α] (t : α) (S : Set α) :
    t ∈ HasCompl.compl '' St ∈ HasCompl.compl '' S ↔ tᶜ ∈ S := by
  simp [← preimage_compl_eq_image_compl]

Characterization of Elements in Complement Image via Complements

Informal description

Let $\alpha$ be a Boolean algebra. For any element $t \in \alpha$ and any subset $S \subseteq \alpha$, the element $t$ belongs to the image of $S$ under the complement operation if and only if the complement of $t$ belongs to $S$. In symbols: $$ t \in \overline{S} \leftrightarrow t^c \in S $$ where $\overline{S}$ denotes the image of $S$ under the complement operation.

Set.image_id_eq theorem

: image (id : α → α) = id

Full source

@[simp]
theorem image_id_eq : image (id : α → α) = id := by ext; simp

Image of Identity Function Equals Identity on Sets

Informal description

The image operation under the identity function $\mathrm{id} : \alpha \to \alpha$ is equal to the identity function on sets, i.e., $\mathrm{image}(\mathrm{id}) = \mathrm{id}$.

Set.image_id' theorem

(s : Set α) : (fun x => x) '' s = s

Full source

/-- A variant of `image_id` -/
@[simp]
theorem image_id' (s : Set α) : (fun x => x) '' s = s := by
  ext
  simp

Image of Set under Identity Function Equals Itself

Informal description

For any set $s$ of elements of type $\alpha$, the image of $s$ under the identity function $\lambda x \mapsto x$ is equal to $s$ itself, i.e., $\{x \mid x \in s\} = s$.

Set.image_id theorem

(s : Set α) : id '' s = s

Full source

theorem image_id (s : Set α) : idid '' s = s := by simp

Image of Set under Identity Function Equals Itself

Informal description

For any set $s$ of elements of type $\alpha$, the image of $s$ under the identity function $\mathrm{id}$ is equal to $s$ itself, i.e., $\mathrm{id}(s) = s$.

Set.image_iterate_eq theorem

{f : α → α} {n : ℕ} : image (f^[n]) = (image f)^[n]

Full source

lemma image_iterate_eq {f : α → α} {n : ℕ} : image (f^[n]) = (image f)^[n] := by
  induction n with
  | zero => simp
  | succ n ih => rw [iterate_succ', iterate_succ', ← ih, image_comp_eq]

Iterated Image Equals Image of Iterated Function: $f^{[n]}(s) = (f(s))^{[n]}$

Informal description

For any function $f : \alpha \to \alpha$ and natural number $n$, the image of the $n$-th iterate of $f$ is equal to the $n$-th iterate of the image function, i.e., $$ f^{[n]}(s) = (f(s))^{[n]} $$ for any set $s \subseteq \alpha$.

Set.compl_compl_image theorem

[BooleanAlgebra α] (S : Set α) : HasCompl.compl '' (HasCompl.compl '' S) = S

Full source

theorem compl_compl_image [BooleanAlgebra α] (S : Set α) :
    HasCompl.complHasCompl.compl '' (HasCompl.compl '' S) = S := by
  rw [← image_comp, compl_comp_compl, image_id]

Double Complement Law for Sets in Boolean Algebra

Informal description

For any Boolean algebra $\alpha$ and any subset $S \subseteq \alpha$, the double complement of $S$ is equal to $S$ itself, i.e., $S^{\complement\complement} = S$.

Set.image_insert_eq theorem

{f : α → β} {a : α} {s : Set α} : f '' insert a s = insert (f a) (f '' s)

Full source

theorem image_insert_eq {f : α → β} {a : α} {s : Set α} :
    f '' insert a s = insert (f a) (f '' s) := by
  ext
  simp [and_or_left, exists_or, eq_comm, or_comm, and_comm]

Image of Union with Singleton: $f(\{a\} \cup s) = \{f(a)\} \cup f(s)$

Informal description

For any function $f : \alpha \to \beta$, element $a \in \alpha$, and subset $s \subseteq \alpha$, the image of the set $\{a\} \cup s$ under $f$ is equal to $\{f(a)\} \cup f(s)$, where $f(s)$ denotes the image of $s$ under $f$. In other words, $$ f(\{a\} \cup s) = \{f(a)\} \cup f(s). $$

Set.image_pair theorem

(f : α → β) (a b : α) : f '' { a, b } = {f a, f b}

Full source

theorem image_pair (f : α → β) (a b : α) : f '' {a, b} = {f a, f b} := by
  simp only [image_insert_eq, image_singleton]

Image of a Pair Set under a Function is a Pair Set

Informal description

For any function $f : \alpha \to \beta$ and any elements $a, b \in \alpha$, the image of the set $\{a, b\}$ under $f$ is the set $\{f(a), f(b)\}$.

Set.image_subset_preimage_of_inverse theorem

{f : α → β} {g : β → α} (I : LeftInverse g f) (s : Set α) : f '' s ⊆ g ⁻¹' s

Full source

theorem image_subset_preimage_of_inverse {f : α → β} {g : β → α} (I : LeftInverse g f) (s : Set α) :
    f '' sf '' s ⊆ g ⁻¹' s := fun _ ⟨a, h, e⟩ => e ▸ ((I a).symm ▸ h : g (f a) ∈ s)

Image Subset of Preimage under Left Inverse

Informal description

Let $f : \alpha \to \beta$ and $g : \beta \to \alpha$ be functions such that $g$ is a left inverse of $f$, i.e., $g(f(x)) = x$ for all $x \in \alpha$. Then for any subset $s \subseteq \alpha$, the image of $s$ under $f$ is contained in the preimage of $s$ under $g$, i.e., $f(s) \subseteq g^{-1}(s)$.

Set.preimage_subset_image_of_inverse theorem

{f : α → β} {g : β → α} (I : LeftInverse g f) (s : Set β) : f ⁻¹' s ⊆ g '' s

Full source

theorem preimage_subset_image_of_inverse {f : α → β} {g : β → α} (I : LeftInverse g f) (s : Set β) :
    f ⁻¹' sf ⁻¹' s ⊆ g '' s := fun b h => ⟨f b, h, I b⟩

Preimage under $f$ is contained in image under left inverse $g$

Informal description

Let $f : \alpha \to \beta$ and $g : \beta \to \alpha$ be functions such that $g$ is a left inverse of $f$ (i.e., $g(f(x)) = x$ for all $x \in \alpha$). Then for any subset $s \subseteq \beta$, the preimage $f^{-1}(s)$ is contained in the image $g(s)$.

Set.range_inter_ssubset_iff_preimage_ssubset theorem

{f : α → β} {S S' : Set β} : range f ∩ S ⊂ range f ∩ S' ↔ f ⁻¹' S ⊂ f ⁻¹' S'

Full source

theorem range_inter_ssubset_iff_preimage_ssubset {f : α → β} {S S' : Set β} :
  rangerange f ∩ Srange f ∩ S ⊂ range f ∩ S'range f ∩ S ⊂ range f ∩ S' ↔ f ⁻¹' S ⊂ f ⁻¹' S' := by
    simp only [Set.ssubset_iff_exists]
    apply and_congr ?_ (by aesop)
    constructor
    all_goals
      intro r x hx
      simp_all only [subset_inter_iff, inter_subset_left, true_and, mem_preimage,
        mem_inter_iff, mem_range, true_and]
      aesop

Strict Subset Relation between Range Intersections and Preimages

Informal description

For any function $f : \alpha \to \beta$ and subsets $S, S' \subseteq \beta$, the strict subset relation $(\text{range } f) \cap S \subset (\text{range } f) \cap S'$ holds if and only if the preimage $f^{-1}(S)$ is a strict subset of the preimage $f^{-1}(S')$.

Set.image_eq_preimage_of_inverse theorem

{f : α → β} {g : β → α} (h₁ : LeftInverse g f) (h₂ : RightInverse g f) : image f = preimage g

Full source

theorem image_eq_preimage_of_inverse {f : α → β} {g : β → α} (h₁ : LeftInverse g f)
    (h₂ : RightInverse g f) : image f = preimage g :=
  funext fun s =>
    Subset.antisymm (image_subset_preimage_of_inverse h₁ s) (preimage_subset_image_of_inverse h₂ s)

Image Equals Preimage under Bijective Inverse

Informal description

Let $f : \alpha \to \beta$ and $g : \beta \to \alpha$ be functions such that $g$ is both a left and right inverse of $f$ (i.e., $g(f(x)) = x$ for all $x \in \alpha$ and $f(g(y)) = y$ for all $y \in \beta$). Then the image operation under $f$ coincides with the preimage operation under $g$, i.e., for any subset $s \subseteq \alpha$, we have $f(s) = g^{-1}(s)$.

Set.mem_image_iff_of_inverse theorem

 {f : α → β} {g : β → α} {b : β} {s : Set α} (h₁ : LeftInverse g f) (h₂ : RightInverse g f) : b ∈ f '' s ↔ g b ∈ s

Full source

theorem mem_image_iff_of_inverse {f : α → β} {g : β → α} {b : β} {s : Set α} (h₁ : LeftInverse g f)
    (h₂ : RightInverse g f) : b ∈ f '' sb ∈ f '' s ↔ g b ∈ s := by
  rw [image_eq_preimage_of_inverse h₁ h₂]; rfl

Membership in Image under Bijective Inverse

Informal description

Let $f : \alpha \to \beta$ and $g : \beta \to \alpha$ be functions such that $g$ is both a left and right inverse of $f$ (i.e., $g(f(x)) = x$ for all $x \in \alpha$ and $f(g(y)) = y$ for all $y \in \beta$). For any element $b \in \beta$ and any subset $s \subseteq \alpha$, we have $b \in f(s)$ if and only if $g(b) \in s$.

Set.image_compl_subset theorem

{f : α → β} {s : Set α} (H : Injective f) : f '' sᶜ ⊆ (f '' s)ᶜ

Full source

theorem image_compl_subset {f : α → β} {s : Set α} (H : Injective f) : f '' sᶜf '' sᶜ ⊆ (f '' s)ᶜ :=
  Disjoint.subset_compl_left <| by simp [disjoint_iff_inf_le, ← image_inter H]

Image of Complement is Subset of Complement of Image for Injective Functions

Informal description

For any injective function $f : \alpha \to \beta$ and any subset $s \subseteq \alpha$, the image of the complement of $s$ under $f$ is contained in the complement of the image of $s$ under $f$, i.e., $f(s^c) \subseteq (f(s))^c$.

Set.subset_image_compl theorem

{f : α → β} {s : Set α} (H : Surjective f) : (f '' s)ᶜ ⊆ f '' sᶜ

Full source

theorem subset_image_compl {f : α → β} {s : Set α} (H : Surjective f) : (f '' s)ᶜ(f '' s)ᶜ ⊆ f '' sᶜ :=
  compl_subset_iff_union.2 <| by
    rw [← image_union]
    simp [image_univ_of_surjective H]

Complement of Image is Subset of Image of Complement for Surjective Functions

Informal description

For any surjective function $f : \alpha \to \beta$ and any subset $s \subseteq \alpha$, the complement of the image of $s$ under $f$ is a subset of the image of the complement of $s$ under $f$. In symbols: $$ (f(s))^c \subseteq f(s^c). $$

Set.image_compl_eq theorem

{f : α → β} {s : Set α} (H : Bijective f) : f '' sᶜ = (f '' s)ᶜ

Full source

theorem image_compl_eq {f : α → β} {s : Set α} (H : Bijective f) : f '' sᶜ = (f '' s)ᶜ :=
  Subset.antisymm (image_compl_subset H.1) (subset_image_compl H.2)

Image of Complement Equals Complement of Image for Bijective Functions

Informal description

For any bijective function $f : \alpha \to \beta$ and any subset $s \subseteq \alpha$, the image of the complement of $s$ under $f$ equals the complement of the image of $s$ under $f$. In symbols: $$ f(s^c) = (f(s))^c. $$

Set.subset_image_diff theorem

(f : α → β) (s t : Set α) : f '' s \ f '' t ⊆ f '' (s \ t)

Full source

theorem subset_image_diff (f : α → β) (s t : Set α) : f '' sf '' s \ f '' tf '' s \ f '' t ⊆ f '' (s \ t) := by
  rw [diff_subset_iff, ← image_union, union_diff_self]
  exact image_subset f subset_union_right

Image of Set Difference Contains Difference of Images

Informal description

For any function $f : \alpha \to \beta$ and any subsets $s, t \subseteq \alpha$, the set difference of the images $f(s) \setminus f(t)$ is a subset of the image of the set difference $f(s \setminus t)$. In symbols: $$ f(s) \setminus f(t) \subseteq f(s \setminus t). $$

Set.subset_image_symmDiff theorem

: (f '' s) ∆ (f '' t) ⊆ f '' s ∆ t

Full source

theorem subset_image_symmDiff : (f '' s) ∆ (f '' t)(f '' s) ∆ (f '' t) ⊆ f '' s ∆ t :=
  (union_subset_union (subset_image_diff _ _ _) <| subset_image_diff _ _ _).trans
    (superset_of_eq (image_union _ _ _))

Image of Symmetric Difference Contains Symmetric Difference of Images

Informal description

For any function $f : \alpha \to \beta$ and any subsets $s, t \subseteq \alpha$, the symmetric difference of the images $f(s) \triangle f(t)$ is a subset of the image of the symmetric difference $f(s \triangle t)$. In symbols: $$ f(s) \triangle f(t) \subseteq f(s \triangle t). $$

Set.image_diff theorem

{f : α → β} (hf : Injective f) (s t : Set α) : f '' (s \ t) = f '' s \ f '' t

Full source

theorem image_diff {f : α → β} (hf : Injective f) (s t : Set α) : f '' (s \ t) = f '' sf '' s \ f '' t :=
  Subset.antisymm
    (Subset.trans (image_inter_subset _ _ _) <| inter_subset_inter_right _ <| image_compl_subset hf)
    (subset_image_diff f s t)

Image of Set Difference Equals Difference of Images for Injective Functions

Informal description

For any injective function $f : \alpha \to \beta$ and any subsets $s, t \subseteq \alpha$, the image of the set difference $s \setminus t$ under $f$ is equal to the set difference of the images $f(s) \setminus f(t)$. In symbols: $$ f(s \setminus t) = f(s) \setminus f(t). $$

Set.image_symmDiff theorem

(hf : Injective f) (s t : Set α) : f '' s ∆ t = (f '' s) ∆ (f '' t)

Full source

theorem image_symmDiff (hf : Injective f) (s t : Set α) : f '' s ∆ t = (f '' s) ∆ (f '' t) := by
  simp_rw [Set.symmDiff_def, image_union, image_diff hf]

Image of Symmetric Difference Equals Symmetric Difference of Images for Injective Functions

Informal description

For any injective function $f : \alpha \to \beta$ and any subsets $s, t \subseteq \alpha$, the image of the symmetric difference $s \triangle t$ under $f$ is equal to the symmetric difference of the images $f(s)$ and $f(t)$. In symbols: $$ f(s \triangle t) = f(s) \triangle f(t). $$

Set.Nonempty.image theorem

(f : α → β) {s : Set α} : s.Nonempty → (f '' s).Nonempty

Full source

theorem Nonempty.image (f : α → β) {s : Set α} : s.Nonempty → (f '' s).Nonempty
  | ⟨x, hx⟩ => ⟨f x, mem_image_of_mem f hx⟩

Nonempty Image of Nonempty Set

Informal description

For any function $f : \alpha \to \beta$ and any nonempty subset $s \subseteq \alpha$, the image $f(s)$ is nonempty.

Set.Nonempty.of_image theorem

{f : α → β} {s : Set α} : (f '' s).Nonempty → s.Nonempty

Full source

theorem Nonempty.of_image {f : α → β} {s : Set α} : (f '' s).Nonempty → s.Nonempty
  | ⟨_, x, hx, _⟩ => ⟨x, hx⟩

Nonempty Image Implies Nonempty Domain

Informal description

For any function $f : \alpha \to \beta$ and any subset $s \subseteq \alpha$, if the image $f(s)$ is nonempty, then $s$ is nonempty.

Set.image_nonempty theorem

{f : α → β} {s : Set α} : (f '' s).Nonempty ↔ s.Nonempty

Full source

@[simp]
theorem image_nonempty {f : α → β} {s : Set α} : (f '' s).Nonempty ↔ s.Nonempty :=
  ⟨Nonempty.of_image, fun h => h.image f⟩

Nonempty Image Equivalence: $f(s) \neq \emptyset \iff s \neq \emptyset$

Informal description

For any function $f \colon \alpha \to \beta$ and any subset $s \subseteq \alpha$, the image $f(s)$ is nonempty if and only if $s$ is nonempty.

Set.Nonempty.preimage theorem

{s : Set β} (hs : s.Nonempty) {f : α → β} (hf : Surjective f) : (f ⁻¹' s).Nonempty

Full source

theorem Nonempty.preimage {s : Set β} (hs : s.Nonempty) {f : α → β} (hf : Surjective f) :
    (f ⁻¹' s).Nonempty :=
  let ⟨y, hy⟩ := hs
  let ⟨x, hx⟩ := hf y
  ⟨x, mem_preimage.2 <| hx.symm ▸ hy⟩

Nonempty Preimage of Nonempty Set under Surjective Function

Informal description

For any nonempty subset $s \subseteq \beta$ and any surjective function $f \colon \alpha \to \beta$, the preimage $f^{-1}(s)$ is nonempty.

Set.instNonemptyElemImage instance

(f : α → β) (s : Set α) [Nonempty s] : Nonempty (f '' s)

Full source

instance (f : α → β) (s : Set α) [Nonempty s] : Nonempty (f '' s) :=
  (Set.Nonempty.image f .of_subtype).to_subtype

Nonempty Image of Nonempty Set

Informal description

For any function $f : \alpha \to \beta$ and any nonempty subset $s \subseteq \alpha$, the image $f(s)$ is nonempty.

Set.image_subset_iff theorem

{s : Set α} {t : Set β} {f : α → β} : f '' s ⊆ t ↔ s ⊆ f ⁻¹' t

Full source

/-- image and preimage are a Galois connection -/
@[simp]
theorem image_subset_iff {s : Set α} {t : Set β} {f : α → β} : f '' sf '' s ⊆ tf '' s ⊆ t ↔ s ⊆ f ⁻¹' t :=
  forall_mem_image

Image-Preimage Subset Equivalence

Informal description

For any function $f \colon \alpha \to \beta$ and subsets $s \subseteq \alpha$, $t \subseteq \beta$, the image $f(s)$ is a subset of $t$ if and only if $s$ is a subset of the preimage $f^{-1}(t)$. In symbols: \[ f(s) \subseteq t \leftrightarrow s \subseteq f^{-1}(t). \]

Set.image_preimage_subset theorem

(f : α → β) (s : Set β) : f '' (f ⁻¹' s) ⊆ s

Full source

theorem image_preimage_subset (f : α → β) (s : Set β) : f '' (f ⁻¹' s)f '' (f ⁻¹' s) ⊆ s :=
  image_subset_iff.2 Subset.rfl

Image of Preimage is Subset of Original Set

Informal description

For any function $f \colon \alpha \to \beta$ and any subset $s \subseteq \beta$, the image of the preimage of $s$ under $f$ is a subset of $s$, i.e., \[ f(f^{-1}(s)) \subseteq s. \]

Set.subset_preimage_image theorem

(f : α → β) (s : Set α) : s ⊆ f ⁻¹' (f '' s)

Full source

theorem subset_preimage_image (f : α → β) (s : Set α) : s ⊆ f ⁻¹' (f '' s) := fun _ =>
  mem_image_of_mem f

Subset Relation Between Set and Preimage of Its Image

Informal description

For any function $f : \alpha \to \beta$ and any subset $s \subseteq \alpha$, the set $s$ is contained in the preimage of its image under $f$, i.e., $s \subseteq f^{-1}(f(s))$.

Set.preimage_image_univ theorem

{f : α → β} : f ⁻¹' (f '' univ) = univ

Full source

theorem preimage_image_univ {f : α → β} : f ⁻¹' (f '' univ) = univ :=
  Subset.antisymm (fun _ _ => trivial) (subset_preimage_image f univ)

Preimage of Image of Universal Set Equals Universal Set

Informal description

For any function $f : \alpha \to \beta$, the preimage of the image of the universal set under $f$ is equal to the universal set, i.e., $f^{-1}(f(\text{univ})) = \text{univ}$.

Set.preimage_image_eq theorem

{f : α → β} (s : Set α) (h : Injective f) : f ⁻¹' (f '' s) = s

Full source

@[simp]
theorem preimage_image_eq {f : α → β} (s : Set α) (h : Injective f) : f ⁻¹' (f '' s) = s :=
  Subset.antisymm (fun _ ⟨_, hy, e⟩ => h e ▸ hy) (subset_preimage_image f s)

Preimage-Image Equality for Injective Functions: $f^{-1}(f(s)) = s$

Informal description

For any injective function $f : \alpha \to \beta$ and any subset $s \subseteq \alpha$, the preimage of the image of $s$ under $f$ equals $s$ itself, i.e., $f^{-1}(f(s)) = s$.

Set.image_preimage_eq theorem

{f : α → β} (s : Set β) (h : Surjective f) : f '' (f ⁻¹' s) = s

Full source

@[simp]
theorem image_preimage_eq {f : α → β} (s : Set β) (h : Surjective f) : f '' (f ⁻¹' s) = s :=
  Subset.antisymm (image_preimage_subset f s) fun x hx =>
    let ⟨y, e⟩ := h x
    ⟨y, (e.symm ▸ hx : f y ∈ s), e⟩

Image-Preimage Equality for Surjective Functions: $f(f^{-1}(s)) = s$

Informal description

For any surjective function $f \colon \alpha \to \beta$ and any subset $s \subseteq \beta$, the image of the preimage of $s$ under $f$ equals $s$, i.e., \[ f(f^{-1}(s)) = s. \]

Set.Nonempty.subset_preimage_const theorem

{s : Set α} (hs : Set.Nonempty s) (t : Set β) (a : β) : s ⊆ (fun _ => a) ⁻¹' t ↔ a ∈ t

Full source

@[simp]
theorem Nonempty.subset_preimage_const {s : Set α} (hs : Set.Nonempty s) (t : Set β) (a : β) :
    s ⊆ (fun _ => a) ⁻¹' ts ⊆ (fun _ => a) ⁻¹' t ↔ a ∈ t := by
  rw [← image_subset_iff, hs.image_const, singleton_subset_iff]

Nonempty Set Subset of Constant Preimage iff Element in Target Set

Informal description

For any nonempty set $s \subseteq \alpha$, any set $t \subseteq \beta$, and any element $a \in \beta$, the set $s$ is contained in the preimage of $t$ under the constant function $\lambda \_, a$ if and only if $a$ belongs to $t$. In symbols: \[ s \subseteq (\lambda \_, a)^{-1}(t) \leftrightarrow a \in t. \]

Set.preimage_injective theorem

: Injective (preimage f) ↔ Surjective f

Full source

@[simp]
theorem preimage_injective : InjectiveInjective (preimage f) ↔ Surjective f :=
  injective_comp_right_iff_surjective

Injectivity of Preimage Equivalence to Surjectivity of Function

Informal description

The preimage function $f^{-1} : \mathcal{P}(\beta) \to \mathcal{P}(\alpha)$ is injective if and only if the function $f : \alpha \to \beta$ is surjective.

Set.preimage_surjective theorem

: Surjective (preimage f) ↔ Injective f

Full source

@[simp]
theorem preimage_surjective : SurjectiveSurjective (preimage f) ↔ Injective f :=
  surjective_comp_right_iff_injective

Surjectivity of Preimage Equivalence to Injectivity of Function

Informal description

The preimage function $f^{-1} : \mathcal{P}(\beta) \to \mathcal{P}(\alpha)$ is surjective if and only if the function $f : \alpha \to \beta$ is injective.

Set.preimage_eq_preimage theorem

{f : β → α} (hf : Surjective f) : f ⁻¹' s = f ⁻¹' t ↔ s = t

Full source

@[simp]
theorem preimage_eq_preimage {f : β → α} (hf : Surjective f) : f ⁻¹' sf ⁻¹' s = f ⁻¹' t ↔ s = t :=
  (preimage_injective.mpr hf).eq_iff

Preimage Equality under Surjective Function: $f^{-1}(s) = f^{-1}(t) \leftrightarrow s = t$

Informal description

Let $f : \beta \to \alpha$ be a surjective function. For any subsets $s, t \subseteq \alpha$, the preimages $f^{-1}(s)$ and $f^{-1}(t)$ are equal if and only if $s = t$.

Set.image_inter_preimage theorem

(f : α → β) (s : Set α) (t : Set β) : f '' (s ∩ f ⁻¹' t) = f '' s ∩ t

Full source

theorem image_inter_preimage (f : α → β) (s : Set α) (t : Set β) :
    f '' (s ∩ f ⁻¹' t) = f '' sf '' s ∩ t := by
  apply Subset.antisymm
  · calc
      f '' (s ∩ f ⁻¹' t) ⊆ f '' s ∩ f '' (f ⁻¹' t) := image_inter_subset _ _ _
      _ ⊆ f '' s ∩ t := inter_subset_inter_right _ (image_preimage_subset f t)
  · rintro _ ⟨⟨x, h', rfl⟩, h⟩
    exact ⟨x, ⟨h', h⟩, rfl⟩

Image-Intersection-Preimage Identity: $f(s \cap f^{-1}(t)) = f(s) \cap t$

Informal description

For any function $f \colon \alpha \to \beta$ and subsets $s \subseteq \alpha$, $t \subseteq \beta$, the image of the intersection $s \cap f^{-1}(t)$ under $f$ equals the intersection of the image $f(s)$ with $t$, i.e., \[ f(s \cap f^{-1}(t)) = f(s) \cap t. \]

Set.image_preimage_inter theorem

(f : α → β) (s : Set α) (t : Set β) : f '' (f ⁻¹' t ∩ s) = t ∩ f '' s

Full source

theorem image_preimage_inter (f : α → β) (s : Set α) (t : Set β) :
    f '' (f ⁻¹' t ∩ s) = t ∩ f '' s := by simp only [inter_comm, image_inter_preimage]

Image-Preimage-Intersection Identity: $f(f^{-1}(t) \cap s) = t \cap f(s)$

Informal description

For any function $f \colon \alpha \to \beta$ and subsets $s \subseteq \alpha$, $t \subseteq \beta$, the image of the intersection $f^{-1}(t) \cap s$ under $f$ equals the intersection of $t$ with the image $f(s)$, i.e., \[ f(f^{-1}(t) \cap s) = t \cap f(s). \]

Set.image_inter_nonempty_iff theorem

{f : α → β} {s : Set α} {t : Set β} : (f '' s ∩ t).Nonempty ↔ (s ∩ f ⁻¹' t).Nonempty

Full source

@[simp]
theorem image_inter_nonempty_iff {f : α → β} {s : Set α} {t : Set β} :
    (f '' s ∩ t).Nonempty ↔ (s ∩ f ⁻¹' t).Nonempty := by
  rw [← image_inter_preimage, image_nonempty]

Nonempty Intersection of Image and Set Equivalence

Informal description

For any function $f \colon \alpha \to \beta$ and subsets $s \subseteq \alpha$, $t \subseteq \beta$, the intersection of the image $f(s)$ with $t$ is nonempty if and only if the intersection of $s$ with the preimage $f^{-1}(t)$ is nonempty. In other words, \[ f(s) \cap t \neq \emptyset \iff s \cap f^{-1}(t) \neq \emptyset. \]

Set.image_diff_preimage theorem

{f : α → β} {s : Set α} {t : Set β} : f '' (s \ f ⁻¹' t) = f '' s \ t

Full source

theorem image_diff_preimage {f : α → β} {s : Set α} {t : Set β} :
    f '' (s \ f ⁻¹' t) = f '' sf '' s \ t := by simp_rw [diff_eq, ← preimage_compl, image_inter_preimage]

Image of Set Difference Equals Difference of Images: $f(s \setminus f^{-1}(t)) = f(s) \setminus t$

Informal description

For any function $f \colon \alpha \to \beta$ and subsets $s \subseteq \alpha$, $t \subseteq \beta$, the image of the set difference $s \setminus f^{-1}(t)$ under $f$ equals the set difference of the image $f(s)$ and $t$, i.e., \[ f(s \setminus f^{-1}(t)) = f(s) \setminus t. \]

Set.compl_image theorem

: image (compl : Set α → Set α) = preimage compl

Full source

theorem compl_image : image (compl : Set α → Set α) = preimage compl :=
  image_eq_preimage_of_inverse compl_compl compl_compl

Image of Complement Equals Preimage of Complement

Informal description

For any type $\alpha$, the image operation under the complement function $\text{compl} : \text{Set } \alpha \to \text{Set } \alpha$ coincides with the preimage operation under $\text{compl}$. That is, for any subset $s \subseteq \alpha$, we have $\text{compl}(s) = \text{compl}^{-1}(s)$.

Set.compl_image_set_of theorem

{p : Set α → Prop} : compl '' {s | p s} = {s | p sᶜ}

Full source

theorem compl_image_set_of {p : Set α → Prop} : complcompl '' { s | p s } = { s | p sᶜ } :=
  congr_fun compl_image p

Image of Complement under Predicate Equals Predicate of Complement

Informal description

For any predicate $p$ on subsets of a type $\alpha$, the image of the collection $\{s \subseteq \alpha \mid p(s)\}$ under the complement operation equals the collection $\{s \subseteq \alpha \mid p(s^c)\}$. In other words, $\text{compl}(\{s \mid p(s)\}) = \{s \mid p(s^c)\}$.

Set.inter_preimage_subset theorem

(s : Set α) (t : Set β) (f : α → β) : s ∩ f ⁻¹' t ⊆ f ⁻¹' (f '' s ∩ t)

Full source

theorem inter_preimage_subset (s : Set α) (t : Set β) (f : α → β) :
    s ∩ f ⁻¹' ts ∩ f ⁻¹' t ⊆ f ⁻¹' (f '' s ∩ t) := fun _ h => ⟨mem_image_of_mem _ h.left, h.right⟩

Intersection-Preimage Subset Property: $s \cap f^{-1}(t) \subseteq f^{-1}(f(s) \cap t)$

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, and any function $f : \alpha \to \beta$, the intersection $s \cap f^{-1}(t)$ is a subset of the preimage $f^{-1}(f(s) \cap t)$.

Set.union_preimage_subset theorem

(s : Set α) (t : Set β) (f : α → β) : s ∪ f ⁻¹' t ⊆ f ⁻¹' (f '' s ∪ t)

Full source

theorem union_preimage_subset (s : Set α) (t : Set β) (f : α → β) :
    s ∪ f ⁻¹' ts ∪ f ⁻¹' t ⊆ f ⁻¹' (f '' s ∪ t) := fun _ h =>
  Or.elim h (fun l => Or.inl <| mem_image_of_mem _ l) fun r => Or.inr r

Union with Preimage is Subset of Preimage of Union with Image

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, and any function $f : \alpha \to \beta$, the union $s \cup f^{-1}(t)$ is a subset of the preimage $f^{-1}(f(s) \cup t)$.

Set.subset_image_union theorem

(f : α → β) (s : Set α) (t : Set β) : f '' (s ∪ f ⁻¹' t) ⊆ f '' s ∪ t

Full source

theorem subset_image_union (f : α → β) (s : Set α) (t : Set β) : f '' (s ∪ f ⁻¹' t)f '' (s ∪ f ⁻¹' t) ⊆ f '' s ∪ t :=
  image_subset_iff.2 (union_preimage_subset _ _ _)

Image of Union with Preimage is Subset of Union with Image

Informal description

For any function $f \colon \alpha \to \beta$ and subsets $s \subseteq \alpha$, $t \subseteq \beta$, the image of the union $s \cup f^{-1}(t)$ under $f$ is a subset of the union of the image $f(s)$ and $t$. In symbols: \[ f(s \cup f^{-1}(t)) \subseteq f(s) \cup t. \]

Set.preimage_subset_iff theorem

{A : Set α} {B : Set β} {f : α → β} : f ⁻¹' B ⊆ A ↔ ∀ a : α, f a ∈ B → a ∈ A

Full source

theorem preimage_subset_iff {A : Set α} {B : Set β} {f : α → β} :
    f ⁻¹' Bf ⁻¹' B ⊆ Af ⁻¹' B ⊆ A ↔ ∀ a : α, f a ∈ B → a ∈ A :=
  Iff.rfl

Preimage Subset Criterion: $f^{-1}(B) \subseteq A \iff \forall a, f(a) \in B \to a \in A$

Informal description

For any function $f : \alpha \to \beta$ and subsets $A \subseteq \alpha$, $B \subseteq \beta$, the preimage $f^{-1}(B)$ is a subset of $A$ if and only if for every $a \in \alpha$, $f(a) \in B$ implies $a \in A$.

Set.image_eq_image theorem

{f : α → β} (hf : Injective f) : f '' s = f '' t ↔ s = t

Full source

theorem image_eq_image {f : α → β} (hf : Injective f) : f '' sf '' s = f '' t ↔ s = t :=
  Iff.symm <|
    (Iff.intro fun eq => eq ▸ rfl) fun eq => by
      rw [← preimage_image_eq s hf, ← preimage_image_eq t hf, eq]

Image Equality under Injective Function: $f(s) = f(t) \leftrightarrow s = t$

Informal description

For any injective function $f \colon \alpha \to \beta$ and subsets $s, t \subseteq \alpha$, the images $f(s)$ and $f(t)$ are equal if and only if $s = t$.

Set.subset_image_iff theorem

{t : Set β} : t ⊆ f '' s ↔ ∃ u, u ⊆ s ∧ f '' u = t

Full source

theorem subset_image_iff {t : Set β} :
    t ⊆ f '' st ⊆ f '' s ↔ ∃ u, u ⊆ s ∧ f '' u = t := by
  refine ⟨fun h ↦ ⟨f ⁻¹' t ∩ s, inter_subset_right, ?_⟩,
    fun ⟨u, hu, hu'⟩ ↦ hu'.symm ▸ image_mono hu⟩
  rwa [image_preimage_inter, inter_eq_left]

Subset of Image Characterization: $t \subseteq f(s) \leftrightarrow \exists u \subseteq s, f(u) = t$

Informal description

For any function $f \colon \alpha \to \beta$ and subsets $s \subseteq \alpha$, $t \subseteq \beta$, the subset $t$ is contained in the image $f(s)$ if and only if there exists a subset $u \subseteq s$ such that the image of $u$ under $f$ equals $t$, i.e., \[ t \subseteq f(s) \leftrightarrow \exists u \subseteq s, f(u) = t. \]

Set.exists_subset_image_iff theorem

{p : Set β → Prop} : (∃ t ⊆ f '' s, p t) ↔ ∃ t ⊆ s, p (f '' t)

Full source

@[simp]
lemma exists_subset_image_iff {p : Set β → Prop} : (∃ t ⊆ f '' s, p t) ↔ ∃ t ⊆ s, p (f '' t) := by
  simp [subset_image_iff]

Existence of Subset in Image vs Preimage under Predicate

Informal description

For any predicate $p$ on subsets of $\beta$, there exists a subset $t$ of the image $f(s)$ satisfying $p(t)$ if and only if there exists a subset $u$ of $s$ such that $p(f(u))$ holds.

Set.forall_subset_image_iff theorem

{p : Set β → Prop} : (∀ t ⊆ f '' s, p t) ↔ ∀ t ⊆ s, p (f '' t)

Full source

@[simp]
lemma forall_subset_image_iff {p : Set β → Prop} : (∀ t ⊆ f '' s, p t) ↔ ∀ t ⊆ s, p (f '' t) := by
  simp [subset_image_iff]

Universal quantification over subsets of an image versus subsets of the domain

Informal description

For any predicate $p$ on subsets of $\beta$, the following are equivalent: 1. For every subset $t \subseteq f(s)$, the predicate $p(t)$ holds. 2. For every subset $t \subseteq s$, the predicate $p(f(t))$ holds. Here $f(s)$ denotes the image of the set $s$ under the function $f : \alpha \to \beta$.

Set.image_subset_image_iff theorem

{f : α → β} (hf : Injective f) : f '' s ⊆ f '' t ↔ s ⊆ t

Full source

theorem image_subset_image_iff {f : α → β} (hf : Injective f) : f '' sf '' s ⊆ f '' tf '' s ⊆ f '' t ↔ s ⊆ t := by
  refine Iff.symm <| (Iff.intro (image_subset f)) fun h => ?_
  rw [← preimage_image_eq s hf, ← preimage_image_eq t hf]
  exact preimage_mono h

Image Subset Relation under Injective Function: $f(s) \subseteq f(t) \leftrightarrow s \subseteq t$

Informal description

For any injective function $f : \alpha \to \beta$ and subsets $s, t \subseteq \alpha$, the image of $s$ under $f$ is a subset of the image of $t$ under $f$ if and only if $s$ is a subset of $t$. In symbols: $$ f(s) \subseteq f(t) \leftrightarrow s \subseteq t $$

Set.prod_quotient_preimage_eq_image theorem

 [s : Setoid α] (g : Quotient s → β) {h : α → β} (Hh : h = g ∘ Quotient.mk'') (r : Set (β × β)) :
  {x : Quotient s × Quotient s | (g x.1, g x.2) ∈ r} =
    (fun a : α × α => (⟦a.1⟧, ⟦a.2⟧)) '' ((fun a : α × α => (h a.1, h a.2)) ⁻¹' r)

Full source

theorem prod_quotient_preimage_eq_image [s : Setoid α] (g : Quotient s → β) {h : α → β}
    (Hh : h = g ∘ Quotient.mk'') (r : Set (β × β)) :
    { x : Quotient s × Quotient s | (g x.1, g x.2) ∈ r } =
      (fun a : α × α => (⟦a.1⟧, ⟦a.2⟧)) '' ((fun a : α × α => (h a.1, h a.2)) ⁻¹' r) :=
  Hh.symm ▸
    Set.ext fun ⟨a₁, a₂⟩ =>
      ⟨Quot.induction_on₂ a₁ a₂ fun a₁ a₂ h => ⟨(a₁, a₂), h, rfl⟩, fun ⟨⟨b₁, b₂⟩, h₁, h₂⟩ =>
        show (g a₁, g a₂) ∈ r from
          have h₃ : ⟦b₁⟧ = a₁ ∧ ⟦b₂⟧ = a₂ := Prod.ext_iff.1 h₂
          h₃.1 ▸ h₃.2 ▸ h₁⟩

Equality between quotient relation and image of preimage under quotient map

Informal description

Let $s$ be a setoid on a type $\alpha$, and let $g : \text{Quotient } s \to \beta$ be a function. Given a function $h : \alpha \to \beta$ such that $h = g \circ \text{Quotient.mk}$, and a relation $r \subseteq \beta \times \beta$, the set of pairs $(x_1, x_2) \in \text{Quotient } s \times \text{Quotient } s$ satisfying $(g(x_1), g(x_2)) \in r$ is equal to the image under the quotient map of the preimage of $r$ under the function $(a_1, a_2) \mapsto (h(a_1), h(a_2))$. In symbols: $$ \{(x_1, x_2) \in \text{Quotient } s \times \text{Quotient } s \mid (g(x_1), g(x_2)) \in r\} = \text{image } (\lambda (a_1, a_2) \mapsto ([a_1], [a_2])) \left( \text{preimage } (\lambda (a_1, a_2) \mapsto (h(a_1), h(a_2))) r \right) $$ where $[a]$ denotes the equivalence class of $a$ under $s$.

Set.exists_image_iff theorem

(f : α → β) (x : Set α) (P : β → Prop) : (∃ a : f '' x, P a) ↔ ∃ a : x, P (f a)

Full source

theorem exists_image_iff (f : α → β) (x : Set α) (P : β → Prop) :
    (∃ a : f '' x, P a) ↔ ∃ a : x, P (f a) :=
  ⟨fun ⟨a, h⟩ => ⟨⟨_, a.prop.choose_spec.1⟩, a.prop.choose_spec.2.symm ▸ h⟩, fun ⟨a, h⟩ =>
    ⟨⟨_, _, a.prop, rfl⟩, h⟩⟩

Existence in Image iff Existence in Preimage

Informal description

For any function $f : \alpha \to \beta$, subset $x \subseteq \alpha$, and predicate $P$ on $\beta$, there exists an element $a$ in the image $f(x)$ satisfying $P(a)$ if and only if there exists an element $a \in x$ such that $P(f(a))$ holds.

Set.imageFactorization_eq theorem

{f : α → β} {s : Set α} : Subtype.val ∘ imageFactorization f s = f ∘ Subtype.val

Full source

theorem imageFactorization_eq {f : α → β} {s : Set α} :
    Subtype.valSubtype.val ∘ imageFactorization f s = f ∘ Subtype.val :=
  funext fun _ => rfl

Factorization of Image Function via Subtype Projection

Informal description

For any function $f : \alpha \to \beta$ and subset $s \subseteq \alpha$, the composition of the image factorization function with the subtype projection equals the composition of $f$ with the subtype projection. In symbols: $$ \text{val} \circ \text{imageFactorization } f \text{ } s = f \circ \text{val} $$ where $\text{val} : s \to \alpha$ is the subtype inclusion map.

Set.surjective_onto_image theorem

{f : α → β} {s : Set α} : Surjective (imageFactorization f s)

Full source

theorem surjective_onto_image {f : α → β} {s : Set α} : Surjective (imageFactorization f s) :=
  fun ⟨_, ⟨a, ha, rfl⟩⟩ => ⟨⟨a, ha⟩, rfl⟩

Surjectivity of the Image Factorization Function

Informal description

For any function $f : \alpha \to \beta$ and any subset $s \subseteq \alpha$, the image factorization function $f \restriction s : s \to f(s)$ is surjective. That is, for every $y \in f(s)$, there exists an $x \in s$ such that $f(x) = y$.

Set.image_perm theorem

{s : Set α} {σ : Equiv.Perm α} (hs : {a : α | σ a ≠ a} ⊆ s) : σ '' s = s

Full source

/-- If the only elements outside `s` are those left fixed by `σ`, then mapping by `σ` has no effect.
-/
theorem image_perm {s : Set α} {σ : Equiv.Perm α} (hs : { a : α | σ a ≠ a }{ a : α | σ a ≠ a } ⊆ s) : σ '' s = s := by
  ext i
  obtain hi | hi := eq_or_ne (σ i) i
  · refine ⟨?_, fun h => ⟨i, h, hi⟩⟩
    rintro ⟨j, hj, h⟩
    rwa [σ.injective (hi.trans h.symm)]
  · refine iff_of_true ⟨σ.symm i, hs fun h => hi ?_, σ.apply_symm_apply _⟩ (hs hi)
    convert congr_arg σ h <;> exact (σ.apply_symm_apply _).symm

Invariance of Set under Permutation: $\sigma(s) = s$ when $\sigma$ moves only elements in $s$

Informal description

Let $s$ be a subset of a type $\alpha$ and $\sigma : \alpha \simeq \alpha$ be a permutation of $\alpha$. If the set of elements not fixed by $\sigma$ is contained in $s$ (i.e., $\{a \in \alpha \mid \sigma(a) \neq a\} \subseteq s$), then the image of $s$ under $\sigma$ is equal to $s$ itself, i.e., $\sigma(s) = s$.

Set.powerset_insert theorem

(s : Set α) (a : α) : 𝒫 insert a s = 𝒫 s ∪ insert a '' 𝒫 s

Full source

/-- The powerset of `{a} ∪ s` is `𝒫 s` together with `{a} ∪ t` for each `t ∈ 𝒫 s`. -/
theorem powerset_insert (s : Set α) (a : α) : 𝒫 insert a s = 𝒫 s𝒫 s ∪ insert a '' 𝒫 s := by
  ext t
  simp_rw [mem_union, mem_image, mem_powerset_iff]
  constructor
  · intro h
    by_cases hs : a ∈ t
    · right
      refine ⟨t \ {a}, ?_, ?_⟩
      · rw [diff_singleton_subset_iff]
        assumption
      · rw [insert_diff_singleton, insert_eq_of_mem hs]
    · left
      exact (subset_insert_iff_of_not_mem hs).mp h
  · rintro (h | ⟨s', h₁, rfl⟩)
    · exact subset_trans h (subset_insert a s)
    · exact insert_subset_insert h₁

Powerset of Insertion: $\mathcal{P}(\{a\} \cup s) = \mathcal{P}(s) \cup \{ \{a\} \cup t \mid t \in \mathcal{P}(s) \}$

Informal description

For any set $s$ of type $\alpha$ and any element $a \in \alpha$, the powerset of the set $\{a\} \cup s$ is equal to the union of the powerset of $s$ and the image of the powerset of $s$ under the insertion of $a$. That is, \[ \mathcal{P}(\{a\} \cup s) = \mathcal{P}(s) \cup \{ \{a\} \cup t \mid t \in \mathcal{P}(s) \}. \]

Set.forall_mem_range theorem

{p : α → Prop} : (∀ a ∈ range f, p a) ↔ ∀ i, p (f i)

Full source

theorem forall_mem_range {p : α → Prop} : (∀ a ∈ range f, p a) ↔ ∀ i, p (f i) := by simp

Universal Quantification over Range of a Function

Informal description

For any predicate $p$ on elements of type $\alpha$, the statement that $p(a)$ holds for all $a$ in the range of $f$ is equivalent to the statement that $p(f(i))$ holds for all indices $i$ in the domain of $f$.

Set.forall_subtype_range_iff theorem

{p : range f → Prop} : (∀ a : range f, p a) ↔ ∀ i, p ⟨f i, mem_range_self _⟩

Full source

theorem forall_subtype_range_iff {p : range f → Prop} :
    (∀ a : range f, p a) ↔ ∀ i, p ⟨f i, mem_range_self _⟩ :=
  ⟨fun H _ => H _, fun H ⟨y, i, hi⟩ => by
    subst hi
    apply H⟩

Universal Quantification over Range via Domain

Informal description

For any predicate $p$ defined on the range of a function $f : \iota \to \alpha$, the statement that $p(a)$ holds for all $a$ in the range of $f$ is equivalent to the statement that $p(f(i))$ holds for all indices $i$ in the domain of $f$.

Set.exists_range_iff theorem

{p : α → Prop} : (∃ a ∈ range f, p a) ↔ ∃ i, p (f i)

Full source

theorem exists_range_iff {p : α → Prop} : (∃ a ∈ range f, p a) ↔ ∃ i, p (f i) := by simp

Existence in Range of a Function iff Existence in Domain

Informal description

For any predicate $p$ on elements of type $\alpha$, there exists an element $a$ in the range of $f$ such that $p(a)$ holds if and only if there exists an index $i$ in the domain of $f$ such that $p(f(i))$ holds.

Set.exists_subtype_range_iff theorem

{p : range f → Prop} : (∃ a : range f, p a) ↔ ∃ i, p ⟨f i, mem_range_self _⟩

Full source

theorem exists_subtype_range_iff {p : range f → Prop} :
    (∃ a : range f, p a) ↔ ∃ i, p ⟨f i, mem_range_self _⟩ :=
  ⟨fun ⟨⟨a, i, hi⟩, ha⟩ => by
    subst a
    exact ⟨i, ha⟩,
   fun ⟨_, hi⟩ => ⟨_, hi⟩⟩

Existence in Range via Existence in Domain

Informal description

For any predicate $p$ defined on the range of a function $f : \iota \to \alpha$, there exists an element $a$ in the range of $f$ satisfying $p(a)$ if and only if there exists an index $i \in \iota$ such that $p(f(i))$ holds.

Set.range_eq_univ theorem

: range f = univ ↔ Surjective f

Full source

theorem range_eq_univ : rangerange f = univ ↔ Surjective f :=
  eq_univ_iff_forall

Range Equals Universal Set iff Function is Surjective

Informal description

For a function $f : \alpha \to \beta$, the range of $f$ is equal to the universal set $\beta$ if and only if $f$ is surjective. In other words, $\text{range}(f) = \beta \leftrightarrow \text{Surjective}(f)$.

Set.subset_range_of_surjective theorem

{f : α → β} (h : Surjective f) (s : Set β) : s ⊆ range f

Full source

@[simp]
theorem subset_range_of_surjective {f : α → β} (h : Surjective f) (s : Set β) :
    s ⊆ range f := Surjective.range_eq h ▸ subset_univ s

Subset of Codomain Contained in Range for Surjective Functions

Informal description

For any surjective function $f : \alpha \to \beta$ and any subset $s \subseteq \beta$, $s$ is contained in the range of $f$, i.e., $s \subseteq \text{range}(f)$.

Set.image_univ theorem

{f : α → β} : f '' univ = range f

Full source

@[simp]
theorem image_univ {f : α → β} : f '' univ = range f := by
  ext
  simp [image, range]

Image of Universal Set Equals Range of Function

Informal description

For any function $f : \alpha \to \beta$, the image of the universal set under $f$ is equal to the range of $f$, i.e., $f(\text{univ}) = \text{range}(f)$.

Set.image_compl_eq_range_diff_image theorem

{f : α → β} (hf : Injective f) (s : Set α) : f '' sᶜ = range f \ f '' s

Full source

lemma image_compl_eq_range_diff_image {f : α → β} (hf : Injective f) (s : Set α) :
    f '' sᶜ = rangerange f \ f '' s := by rw [← image_univ, ← image_diff hf, compl_eq_univ_diff]

Image of Complement Equals Range Minus Image for Injective Functions

Informal description

For any injective function $f \colon \alpha \to \beta$ and any subset $s \subseteq \alpha$, the image of the complement of $s$ under $f$ equals the difference between the range of $f$ and the image of $s$ under $f$. In symbols: \[ f(s^c) = \text{range}(f) \setminus f(s). \]

Set.range_diff_image theorem

{f : α → β} (hf : Injective f) (s : Set α) : range f \ f '' s = f '' sᶜ

Full source

/-- Alias of `Set.image_compl_eq_range_sdiff_image`. -/
lemma range_diff_image {f : α → β} (hf : Injective f) (s : Set α) : rangerange f \ f '' s = f '' sᶜ := by
  rw [image_compl_eq_range_diff_image hf]

Range Minus Image Equals Image of Complement for Injective Functions

Informal description

For any injective function $f \colon \alpha \to \beta$ and any subset $s \subseteq \alpha$, the difference between the range of $f$ and the image of $s$ under $f$ equals the image of the complement of $s$ under $f$. In symbols: \[ \text{range}(f) \setminus f(s) = f(s^c). \]

Set.preimage_eq_univ_iff theorem

{f : α → β} {s} : f ⁻¹' s = univ ↔ range f ⊆ s

Full source

@[simp]
theorem preimage_eq_univ_iff {f : α → β} {s} : f ⁻¹' sf ⁻¹' s = univ ↔ range f ⊆ s := by
  rw [← univ_subset_iff, ← image_subset_iff, image_univ]

Preimage Equals Universal Set if and only if Range is Subset

Informal description

For any function $f \colon \alpha \to \beta$ and subset $s \subseteq \beta$, the preimage $f^{-1}(s)$ equals the universal set $\text{univ}$ if and only if the range of $f$ is contained in $s$. In symbols: \[ f^{-1}(s) = \text{univ} \leftrightarrow \text{range}(f) \subseteq s. \]

Set.image_subset_range theorem

(f : α → β) (s) : f '' s ⊆ range f

Full source

theorem image_subset_range (f : α → β) (s) : f '' sf '' s ⊆ range f := by
  rw [← image_univ]; exact image_subset _ (subset_univ _)

Image is Subset of Range

Informal description

For any function $f : \alpha \to \beta$ and any subset $s \subseteq \alpha$, the image of $s$ under $f$ is a subset of the range of $f$, i.e., $f(s) \subseteq \text{range}(f)$.

Set.mem_range_of_mem_image theorem

(f : α → β) (s) {x : β} (h : x ∈ f '' s) : x ∈ range f

Full source

theorem mem_range_of_mem_image (f : α → β) (s) {x : β} (h : x ∈ f '' s) : x ∈ range f :=
  image_subset_range f s h

Image Elements Belong to Range

Informal description

For any function $f \colon \alpha \to \beta$, any subset $s \subseteq \alpha$, and any element $x \in \beta$, if $x$ belongs to the image $f(s)$, then $x$ belongs to the range of $f$.

Nat.mem_range_succ theorem

(i : ℕ) : i ∈ range Nat.succ ↔ 0 < i

Full source

theorem _root_.Nat.mem_range_succ (i : ℕ) : i ∈ range Nat.succi ∈ range Nat.succ ↔ 0 < i :=
  ⟨by
    rintro ⟨n, rfl⟩
    exact Nat.succ_pos n, fun h => ⟨_, Nat.succ_pred_eq_of_pos h⟩⟩

Membership in Range of Successor Function for Natural Numbers

Informal description

For any natural number $i$, $i$ belongs to the range of the successor function if and only if $i$ is greater than zero, i.e., $i \in \mathrm{range}(\mathrm{succ}) \leftrightarrow 0 < i$.

Set.Nonempty.preimage' theorem

{s : Set β} (hs : s.Nonempty) {f : α → β} (hf : s ⊆ range f) : (f ⁻¹' s).Nonempty

Full source

theorem Nonempty.preimage' {s : Set β} (hs : s.Nonempty) {f : α → β} (hf : s ⊆ range f) :
    (f ⁻¹' s).Nonempty :=
  let ⟨_, hy⟩ := hs
  let ⟨x, hx⟩ := hf hy
  ⟨x, Set.mem_preimage.2 <| hx.symm ▸ hy⟩

Nonempty Preimage of Nonempty Subset in Range

Informal description

For any nonempty subset $s \subseteq \beta$ and any function $f \colon \alpha \to \beta$, if $s$ is contained in the range of $f$, then the preimage $f^{-1}(s)$ is nonempty.

Set.range_comp theorem

(g : α → β) (f : ι → α) : range (g ∘ f) = g '' range f

Full source

theorem range_comp (g : α → β) (f : ι → α) : range (g ∘ f) = g '' range f := by aesop

Range of Composition Equals Image of Range

Informal description

For any functions $g : \alpha \to \beta$ and $f : \iota \to \alpha$, the range of the composition $g \circ f$ is equal to the image of the range of $f$ under $g$, i.e., $\mathrm{range}(g \circ f) = g(\mathrm{range}(f))$.

Set.range_comp' theorem

(g : α → β) (f : ι → α) : range (fun x => g (f x)) = g '' range f

Full source

/--
Variant of `range_comp` using a lambda instead of function composition.
-/
theorem range_comp' (g : α → β) (f : ι → α) : range (fun x => g (f x)) = g '' range f :=
  range_comp g f

Range of Lambda Composition Equals Image of Range

Informal description

For any functions $g : \alpha \to \beta$ and $f : \iota \to \alpha$, the range of the function $\lambda x, g(f(x))$ is equal to the image of the range of $f$ under $g$, i.e., $\mathrm{range}(\lambda x, g(f(x))) = g(\mathrm{range}(f))$.

Set.range_subset_iff theorem

: range f ⊆ s ↔ ∀ y, f y ∈ s

Full source

theorem range_subset_iff : rangerange f ⊆ srange f ⊆ s ↔ ∀ y, f y ∈ s :=
  forall_mem_range

Range Subset Criterion: $\mathrm{range}(f) \subseteq s \leftrightarrow \forall y, f(y) \in s$

Informal description

For any function $f : \iota \to \alpha$ and any subset $s \subseteq \alpha$, the range of $f$ is contained in $s$ if and only if for every element $y$ in the domain of $f$, the image $f(y)$ belongs to $s$.

Set.range_subset_range_iff_exists_comp theorem

{f : α → γ} {g : β → γ} : range f ⊆ range g ↔ ∃ h : α → β, f = g ∘ h

Full source

theorem range_subset_range_iff_exists_comp {f : α → γ} {g : β → γ} :
    rangerange f ⊆ range grange f ⊆ range g ↔ ∃ h : α → β, f = g ∘ h := by
  simp only [range_subset_iff, mem_range, Classical.skolem, funext_iff, (· ∘ ·), eq_comm]

Range Inclusion Criterion via Function Composition

Informal description

For any functions $f \colon \alpha \to \gamma$ and $g \colon \beta \to \gamma$, the range of $f$ is a subset of the range of $g$ if and only if there exists a function $h \colon \alpha \to \beta$ such that $f = g \circ h$.

Set.range_eq_iff theorem

(f : α → β) (s : Set β) : range f = s ↔ (∀ a, f a ∈ s) ∧ ∀ b ∈ s, ∃ a, f a = b

Full source

theorem range_eq_iff (f : α → β) (s : Set β) :
    rangerange f = s ↔ (∀ a, f a ∈ s) ∧ ∀ b ∈ s, ∃ a, f a = b := by
  rw [← range_subset_iff]
  exact le_antisymm_iff

Characterization of Range Equality: $\mathrm{range}(f) = s \leftrightarrow (\forall a, f(a) \in s) \land (\forall b \in s, \exists a, f(a) = b)$

Informal description

For a function $f \colon \alpha \to \beta$ and a subset $s \subseteq \beta$, the range of $f$ equals $s$ if and only if: 1. For every $a \in \alpha$, $f(a) \in s$, and 2. For every $b \in s$, there exists $a \in \alpha$ such that $f(a) = b$.

Set.range_comp_subset_range theorem

(f : α → β) (g : β → γ) : range (g ∘ f) ⊆ range g

Full source

theorem range_comp_subset_range (f : α → β) (g : β → γ) : rangerange (g ∘ f) ⊆ range g := by
  rw [range_comp]; apply image_subset_range

Range of Composition is Subset of Range of Outer Function

Informal description

For any functions $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$, the range of the composition $g \circ f$ is a subset of the range of $g$, i.e., $\mathrm{range}(g \circ f) \subseteq \mathrm{range}(g)$.

Set.range_nonempty_iff_nonempty theorem

: (range f).Nonempty ↔ Nonempty ι

Full source

theorem range_nonempty_iff_nonempty : (range f).Nonempty ↔ Nonempty ι :=
  ⟨fun ⟨_, x, _⟩ => ⟨x⟩, fun ⟨x⟩ => ⟨f x, mem_range_self x⟩⟩

Nonempty Range iff Nonempty Domain

Informal description

The range of a function $f : \iota \to \alpha$ is nonempty if and only if the domain type $\iota$ is nonempty.

Set.range_nonempty theorem

[h : Nonempty ι] (f : ι → α) : (range f).Nonempty

Full source

theorem range_nonempty [h : Nonempty ι] (f : ι → α) : (range f).Nonempty :=
  range_nonempty_iff_nonempty.2 h

Nonempty Domain Implies Nonempty Range

Informal description

For any nonempty type $\iota$ and any function $f : \iota \to \alpha$, the range of $f$ is nonempty.

Set.range_eq_empty_iff theorem

{f : ι → α} : range f = ∅ ↔ IsEmpty ι

Full source

@[simp]
theorem range_eq_empty_iff {f : ι → α} : rangerange f = ∅ ↔ IsEmpty ι := by
  rw [← not_nonempty_iff, ← range_nonempty_iff_nonempty, not_nonempty_iff_eq_empty]

Range Empty iff Domain Empty

Informal description

For any function $f : \iota \to \alpha$, the range of $f$ is empty if and only if the domain type $\iota$ is empty, i.e., $\text{range } f = \emptyset \leftrightarrow \text{IsEmpty } \iota$.

Set.range_eq_empty theorem

[IsEmpty ι] (f : ι → α) : range f = ∅

Full source

theorem range_eq_empty [IsEmpty ι] (f : ι → α) : range f = ∅ :=
  range_eq_empty_iff.2 ‹_›

Range of Function with Empty Domain is Empty

Informal description

For any function $f : \iota \to \alpha$ where the domain type $\iota$ is empty, the range of $f$ is the empty set, i.e., $\text{range } f = \emptyset$.

Set.instNonemptyRange instance

[Nonempty ι] (f : ι → α) : Nonempty (range f)

Full source

instance instNonemptyRange [Nonempty ι] (f : ι → α) : Nonempty (range f) :=
  (range_nonempty f).to_subtype

Nonempty Range of a Function with Nonempty Domain

Informal description

For any nonempty type $\iota$ and any function $f : \iota \to \alpha$, the range of $f$ is nonempty.

Set.image_union_image_compl_eq_range theorem

(f : α → β) : f '' s ∪ f '' sᶜ = range f

Full source

@[simp]
theorem image_union_image_compl_eq_range (f : α → β) : f '' sf '' s ∪ f '' sᶜ = range f := by
  rw [← image_union, ← image_univ, ← union_compl_self]

Range Decomposition via Image and Complement Image: $f(s) \cup f(s^c) = \mathrm{range}(f)$

Informal description

For any function $f : \alpha \to \beta$ and any subset $s \subseteq \alpha$, the union of the image of $s$ under $f$ and the image of the complement of $s$ under $f$ equals the range of $f$. That is, $$ f(s) \cup f(s^c) = \mathrm{range}(f). $$

Set.insert_image_compl_eq_range theorem

(f : α → β) (x : α) : insert (f x) (f '' { x }ᶜ) = range f

Full source

theorem insert_image_compl_eq_range (f : α → β) (x : α) : insert (f x) (f '' {x}ᶜ) = range f := by
  rw [← image_insert_eq, insert_eq, union_compl_self, image_univ]

Range Decomposition via Singleton and Complement Image: $\{f(x)\} \cup f(\{x\}^c) = \mathrm{range}(f)$

Informal description

For any function $f : \alpha \to \beta$ and any element $x \in \alpha$, the union of the singleton set $\{f(x)\}$ with the image of the complement of $\{x\}$ under $f$ equals the range of $f$. That is, $$ \{f(x)\} \cup f(\{x\}^c) = \mathrm{range}(f). $$

Set.image_preimage_eq_range_inter theorem

{f : α → β} {t : Set β} : f '' (f ⁻¹' t) = range f ∩ t

Full source

theorem image_preimage_eq_range_inter {f : α → β} {t : Set β} : f '' (f ⁻¹' t) = rangerange f ∩ t :=
  ext fun x =>
    ⟨fun ⟨_, hx, HEq⟩ => HEq ▸ ⟨mem_range_self _, hx⟩, fun ⟨⟨y, h_eq⟩, hx⟩ =>
      h_eq ▸ mem_image_of_mem f <| show y ∈ f ⁻¹' t by rw [preimage, mem_setOf, h_eq]; exact hx⟩

Image of Preimage Equals Range Intersection: $f(f^{-1}(t)) = \mathrm{range}(f) \cap t$

Informal description

For any function $f : \alpha \to \beta$ and any subset $t \subseteq \beta$, the image of the preimage of $t$ under $f$ is equal to the intersection of the range of $f$ with $t$. That is, $f(f^{-1}(t)) = \mathrm{range}(f) \cap t$.

Set.image_preimage_eq_inter_range theorem

{f : α → β} {t : Set β} : f '' (f ⁻¹' t) = t ∩ range f

Full source

theorem image_preimage_eq_inter_range {f : α → β} {t : Set β} : f '' (f ⁻¹' t) = t ∩ range f := by
  rw [image_preimage_eq_range_inter, inter_comm]

Image of Preimage Equals Intersection with Range: $f(f^{-1}(t)) = t \cap \mathrm{range}(f)$

Informal description

For any function $f : \alpha \to \beta$ and any subset $t \subseteq \beta$, the image of the preimage of $t$ under $f$ is equal to the intersection of $t$ with the range of $f$. That is, $f(f^{-1}(t)) = t \cap \mathrm{range}(f)$.

Set.image_preimage_eq_of_subset theorem

{f : α → β} {s : Set β} (hs : s ⊆ range f) : f '' (f ⁻¹' s) = s

Full source

theorem image_preimage_eq_of_subset {f : α → β} {s : Set β} (hs : s ⊆ range f) :
    f '' (f ⁻¹' s) = s := by rw [image_preimage_eq_range_inter, inter_eq_self_of_subset_right hs]

Image of Preimage Equals Original Set When Subset of Range: $f(f^{-1}(s)) = s$ for $s \subseteq \mathrm{range}(f)$

Informal description

For any function $f : \alpha \to \beta$ and any subset $s \subseteq \beta$ such that $s$ is contained in the range of $f$, the image of the preimage of $s$ under $f$ equals $s$, i.e., $f(f^{-1}(s)) = s$.

Set.image_preimage_eq_iff theorem

{f : α → β} {s : Set β} : f '' (f ⁻¹' s) = s ↔ s ⊆ range f

Full source

theorem image_preimage_eq_iff {f : α → β} {s : Set β} : f '' (f ⁻¹' s)f '' (f ⁻¹' s) = s ↔ s ⊆ range f :=
  ⟨by
    intro h
    rw [← h]
    apply image_subset_range,
   image_preimage_eq_of_subset⟩

Image of Preimage Equals Set if and only if Subset of Range: $f(f^{-1}(s)) = s \iff s \subseteq \mathrm{range}(f)$

Informal description

For any function $f : \alpha \to \beta$ and any subset $s \subseteq \beta$, the image of the preimage of $s$ under $f$ equals $s$ if and only if $s$ is a subset of the range of $f$. In symbols: $$ f(f^{-1}(s)) = s \iff s \subseteq \mathrm{range}(f). $$

Set.subset_range_iff_exists_image_eq theorem

{f : α → β} {s : Set β} : s ⊆ range f ↔ ∃ t, f '' t = s

Full source

theorem subset_range_iff_exists_image_eq {f : α → β} {s : Set β} : s ⊆ range fs ⊆ range f ↔ ∃ t, f '' t = s :=
  ⟨fun h => ⟨_, image_preimage_eq_iff.2 h⟩, fun ⟨_, ht⟩ => ht ▸ image_subset_range _ _⟩

Subset of Range is Image of Some Set: $s \subseteq \mathrm{range}(f) \iff \exists t, f(t) = s$

Informal description

For any function $f : \alpha \to \beta$ and any subset $s \subseteq \beta$, $s$ is a subset of the range of $f$ if and only if there exists a subset $t \subseteq \alpha$ such that the image of $t$ under $f$ equals $s$. In symbols: $$ s \subseteq \mathrm{range}(f) \iff \exists t \subseteq \alpha, f(t) = s. $$

Set.range_image theorem

(f : α → β) : range (image f) = 𝒫 range f

Full source

theorem range_image (f : α → β) : range (image f) = 𝒫 range f :=
  ext fun _ => subset_range_iff_exists_image_eq.symm

Range of Image Function Equals Powerset of Range: $\mathrm{range}(\mathrm{image}(f)) = \mathcal{P}(\mathrm{range}(f))$

Informal description

For any function $f : \alpha \to \beta$, the range of the image function $\mathrm{image}(f) : \mathcal{P}(\alpha) \to \mathcal{P}(\beta)$ is equal to the powerset of the range of $f$. In symbols: $$ \mathrm{range}(\mathrm{image}(f)) = \mathcal{P}(\mathrm{range}(f)). $$

Set.exists_subset_range_and_iff theorem

{f : α → β} {p : Set β → Prop} : (∃ s, s ⊆ range f ∧ p s) ↔ ∃ s, p (f '' s)

Full source

@[simp]
theorem exists_subset_range_and_iff {f : α → β} {p : Set β → Prop} :
    (∃ s, s ⊆ range f ∧ p s) ↔ ∃ s, p (f '' s) := by
  rw [← exists_range_iff, range_image]; rfl

Existence of Subset in Range Satisfying Predicate iff Existence of Preimage Satisfying Predicate

Informal description

For any function $f : \alpha \to \beta$ and any predicate $p$ on subsets of $\beta$, there exists a subset $s \subseteq \beta$ contained in the range of $f$ that satisfies $p(s)$ if and only if there exists a subset $t \subseteq \alpha$ such that $p(f(t))$ holds, where $f(t)$ denotes the image of $t$ under $f$. In symbols: $$ (\exists s \subseteq \mathrm{range}(f), p(s)) \leftrightarrow (\exists t \subseteq \alpha, p(f(t))). $$

Set.forall_subset_range_iff theorem

{f : α → β} {p : Set β → Prop} : (∀ s, s ⊆ range f → p s) ↔ ∀ s, p (f '' s)

Full source

@[simp]
theorem forall_subset_range_iff {f : α → β} {p : Set β → Prop} :
    (∀ s, s ⊆ range f → p s) ↔ ∀ s, p (f '' s) := by
  rw [← forall_mem_range, range_image]; simp only [mem_powerset_iff]

Universal Quantification over Subsets of Range vs. Images of Subsets: $(\forall s \subseteq \mathrm{range}(f), p(s)) \leftrightarrow (\forall s, p(f''s))$

Informal description

For any function $f : \alpha \to \beta$ and predicate $p$ on subsets of $\beta$, the following are equivalent: 1. For every subset $s \subseteq \mathrm{range}(f)$, the predicate $p(s)$ holds. 2. For every subset $s \subseteq \alpha$, the predicate $p(f '' s)$ holds, where $f '' s$ denotes the image of $s$ under $f$.

Set.preimage_subset_preimage_iff theorem

{s t : Set α} {f : β → α} (hs : s ⊆ range f) : f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t

Full source

@[simp]
theorem preimage_subset_preimage_iff {s t : Set α} {f : β → α} (hs : s ⊆ range f) :
    f ⁻¹' sf ⁻¹' s ⊆ f ⁻¹' tf ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t := by
  constructor
  · intro h x hx
    rcases hs hx with ⟨y, rfl⟩
    exact h hx
  intro h x; apply h

Preimage Subset Relation under Function with Restricted Range

Informal description

Let $f : \beta \to \alpha$ be a function and let $s, t \subseteq \alpha$ be subsets such that $s \subseteq \mathrm{range}(f)$. Then the preimage of $s$ under $f$ is contained in the preimage of $t$ under $f$ if and only if $s$ is contained in $t$, i.e., $$ f^{-1}(s) \subseteq f^{-1}(t) \leftrightarrow s \subseteq t. $$

Set.preimage_eq_preimage' theorem

{s t : Set α} {f : β → α} (hs : s ⊆ range f) (ht : t ⊆ range f) : f ⁻¹' s = f ⁻¹' t ↔ s = t

Full source

theorem preimage_eq_preimage' {s t : Set α} {f : β → α} (hs : s ⊆ range f) (ht : t ⊆ range f) :
    f ⁻¹' sf ⁻¹' s = f ⁻¹' t ↔ s = t := by
  constructor
  · intro h
    apply Subset.antisymm
    · rw [← preimage_subset_preimage_iff hs, h]
    · rw [← preimage_subset_preimage_iff ht, h]
  rintro rfl; rfl

Preimage Equality under Function with Restricted Range Implies Set Equality

Informal description

Let $f : \beta \to \alpha$ be a function and let $s, t \subseteq \alpha$ be subsets such that $s \subseteq \mathrm{range}(f)$ and $t \subseteq \mathrm{range}(f)$. Then the preimages of $s$ and $t$ under $f$ are equal if and only if $s$ and $t$ are equal, i.e., $$ f^{-1}(s) = f^{-1}(t) \leftrightarrow s = t. $$

Set.preimage_inter_range theorem

{f : α → β} {s : Set β} : f ⁻¹' (s ∩ range f) = f ⁻¹' s

Full source

theorem preimage_inter_range {f : α → β} {s : Set β} : f ⁻¹' (s ∩ range f) = f ⁻¹' s :=
  Set.ext fun x => and_iff_left ⟨x, rfl⟩

Preimage of Intersection with Range Equals Preimage

Informal description

For any function $f : \alpha \to \beta$ and subset $s \subseteq \beta$, the preimage of $s \cap \mathrm{range}(f)$ under $f$ is equal to the preimage of $s$ under $f$, i.e., $$ f^{-1}(s \cap \mathrm{range}(f)) = f^{-1}(s). $$

Set.preimage_range_inter theorem

{f : α → β} {s : Set β} : f ⁻¹' (range f ∩ s) = f ⁻¹' s

Full source

theorem preimage_range_inter {f : α → β} {s : Set β} : f ⁻¹' (range f ∩ s) = f ⁻¹' s := by
  rw [inter_comm, preimage_inter_range]

Preimage of Range Intersection Equals Preimage

Informal description

For any function $f \colon \alpha \to \beta$ and any subset $s \subseteq \beta$, the preimage of the intersection of the range of $f$ with $s$ under $f$ is equal to the preimage of $s$ under $f$, i.e., $$ f^{-1}(\mathrm{range}(f) \cap s) = f^{-1}(s). $$

Set.preimage_image_preimage theorem

{f : α → β} {s : Set β} : f ⁻¹' (f '' (f ⁻¹' s)) = f ⁻¹' s

Full source

theorem preimage_image_preimage {f : α → β} {s : Set β} : f ⁻¹' (f '' (f ⁻¹' s)) = f ⁻¹' s := by
  rw [image_preimage_eq_range_inter, preimage_range_inter]

Preimage-Image-Preimage Identity: $f^{-1}(f(f^{-1}(s))) = f^{-1}(s)$

Informal description

For any function $f \colon \alpha \to \beta$ and any subset $s \subseteq \beta$, the preimage of the image of the preimage of $s$ under $f$ equals the preimage of $s$ itself, i.e., $$ f^{-1}(f(f^{-1}(s))) = f^{-1}(s). $$

Set.range_id theorem

: range (@id α) = univ

Full source

@[simp, mfld_simps]
theorem range_id : range (@id α) = univ :=
  range_eq_univ.2 surjective_id

Range of Identity Function is Universal Set

Informal description

The range of the identity function $\mathrm{id} : \alpha \to \alpha$ is equal to the universal set on $\alpha$, i.e., $\mathrm{range}(\mathrm{id}) = \mathrm{univ}$.

Set.range_id' theorem

: (range fun x : α => x) = univ

Full source

@[simp, mfld_simps]
theorem range_id' : (range fun x : α => x) = univ :=
  range_id

Range of Identity Function Equals Universal Set

Informal description

The range of the identity function $\lambda x : \alpha, x$ is equal to the universal set on $\alpha$, i.e., $\mathrm{range}(\lambda x, x) = \mathrm{univ}$.

Prod.range_fst theorem

[Nonempty β] : range (Prod.fst : α × β → α) = univ

Full source

@[simp]
theorem _root_.Prod.range_fst [Nonempty β] : range (Prod.fst : α × β → α) = univ :=
  Prod.fst_surjective.range_eq

Range of First Projection is Universal Set for Nonempty $\beta$

Informal description

For any nonempty type $\beta$, the range of the first projection function $\operatorname{fst} : \alpha \times \beta \to \alpha$ is equal to the universal set on $\alpha$. That is, every element of $\alpha$ is the first component of some pair in $\alpha \times \beta$.

Prod.range_snd theorem

[Nonempty α] : range (Prod.snd : α × β → β) = univ

Full source

@[simp]
theorem _root_.Prod.range_snd [Nonempty α] : range (Prod.snd : α × β → β) = univ :=
  Prod.snd_surjective.range_eq

Range of Second Projection is Universal Set for Nonempty $\alpha$

Informal description

For any nonempty type $\alpha$, the range of the second projection function $\operatorname{snd} : \alpha \times \beta \to \beta$ is equal to the universal set on $\beta$. That is, every element of $\beta$ is the second component of some pair in $\alpha \times \beta$.

Set.range_eval theorem

{α : ι → Sort _} [∀ i, Nonempty (α i)] (i : ι) : range (eval i : (∀ i, α i) → α i) = univ

Full source

@[simp]
theorem range_eval {α : ι → Sort _} [∀ i, Nonempty (α i)] (i : ι) :
    range (eval i : (∀ i, α i) → α i) = univ :=
  (surjective_eval i).range_eq

Range of Dependent Function Evaluation Equals Universal Set

Informal description

For any family of types $\alpha : \iota \to \text{Sort}\, \_$ where each $\alpha i$ is nonempty, and for any index $i \in \iota$, the range of the evaluation function $\text{eval}\, i : (\forall i, \alpha i) \to \alpha i$ is equal to the universal set on $\alpha i$. That is, every element of $\alpha i$ is the evaluation at $i$ of some dependent function $f : \forall i, \alpha i$.

Set.range_inl theorem

: range (@Sum.inl α β) = {x | Sum.isLeft x}

Full source

theorem range_inl : range (@Sum.inl α β) = {x | Sum.isLeft x} := by ext (_|_) <;> simp

Range of Left Injection in Sum Type Equals Left-Projected Elements

Informal description

The range of the left injection function $\text{Sum.inl} : \alpha \to \alpha \oplus \beta$ is equal to the set of all elements $x$ in $\alpha \oplus \beta$ that satisfy $\text{Sum.isLeft}(x)$.

Set.range_inr theorem

: range (@Sum.inr α β) = {x | Sum.isRight x}

Full source

theorem range_inr : range (@Sum.inr α β) = {x | Sum.isRight x} := by ext (_|_) <;> simp

Range of Right Injection in Sum Type Equals Right-Projected Elements

Informal description

The range of the right injection function $\text{Sum.inr} : \beta \to \alpha \oplus \beta$ is equal to the set of all elements $x$ in $\alpha \oplus \beta$ that satisfy $\text{Sum.isRight}(x)$.

Set.isCompl_range_inl_range_inr theorem

: IsCompl (range <| @Sum.inl α β) (range Sum.inr)

Full source

theorem isCompl_range_inl_range_inr : IsCompl (range <| @Sum.inl α β) (range Sum.inr) :=
  IsCompl.of_le
    (by
      rintro y ⟨⟨x₁, rfl⟩, ⟨x₂, h⟩⟩
      exact Sum.noConfusion h)
    (by rintro (x | y) - <;> [left; right] <;> exact mem_range_self _)

Complementarity of Left and Right Injection Ranges in Sum Type

Informal description

The ranges of the left injection $\text{Sum.inl} : \alpha \to \alpha \oplus \beta$ and the right injection $\text{Sum.inr} : \beta \to \alpha \oplus \beta$ are complementary subsets of $\alpha \oplus \beta$. That is, their union is the universal set and their intersection is empty.

Set.range_inl_union_range_inr theorem

: range (Sum.inl : α → α ⊕ β) ∪ range Sum.inr = univ

Full source

@[simp]
theorem range_inl_union_range_inr : rangerange (Sum.inl : α → α ⊕ β) ∪ range Sum.inr = univ :=
  isCompl_range_inl_range_inr.sup_eq_top

Union of Left and Right Injection Ranges Covers Sum Type

Informal description

For any types $\alpha$ and $\beta$, the union of the ranges of the left injection $\text{Sum.inl} : \alpha \to \alpha \oplus \beta$ and the right injection $\text{Sum.inr} : \beta \to \alpha \oplus \beta$ equals the universal set of $\alpha \oplus \beta$.

Set.range_inl_inter_range_inr theorem

: range (Sum.inl : α → α ⊕ β) ∩ range Sum.inr = ∅

Full source

@[simp]
theorem range_inl_inter_range_inr : rangerange (Sum.inl : α → α ⊕ β) ∩ range Sum.inr = ∅ :=
  isCompl_range_inl_range_inr.inf_eq_bot

Disjointness of Left and Right Injection Ranges in Sum Type

Informal description

For any types $\alpha$ and $\beta$, the intersection of the ranges of the left injection $\text{Sum.inl} : \alpha \to \alpha \oplus \beta$ and the right injection $\text{Sum.inr} : \beta \to \alpha \oplus \beta$ is the empty set. In other words, $\text{range}(\text{Sum.inl}) \cap \text{range}(\text{Sum.inr}) = \emptyset$.

Set.range_inr_union_range_inl theorem

: range (Sum.inr : β → α ⊕ β) ∪ range Sum.inl = univ

Full source

@[simp]
theorem range_inr_union_range_inl : rangerange (Sum.inr : β → α ⊕ β) ∪ range Sum.inl = univ :=
  isCompl_range_inl_range_inr.symm.sup_eq_top

Union of Right and Left Injection Ranges Covers Sum Type

Informal description

For any types $\alpha$ and $\beta$, the union of the range of the right injection $\mathrm{inr} : \beta \to \alpha \oplus \beta$ and the range of the left injection $\mathrm{inl} : \alpha \to \alpha \oplus \beta$ equals the universal set of $\alpha \oplus \beta$. That is, $\mathrm{range}(\mathrm{inr}) \cup \mathrm{range}(\mathrm{inl}) = \mathrm{univ}$.

Set.range_inr_inter_range_inl theorem

: range (Sum.inr : β → α ⊕ β) ∩ range Sum.inl = ∅

Full source

@[simp]
theorem range_inr_inter_range_inl : rangerange (Sum.inr : β → α ⊕ β) ∩ range Sum.inl = ∅ :=
  isCompl_range_inl_range_inr.symm.inf_eq_bot

Disjointness of Left and Right Injection Ranges in Sum Type

Informal description

For any types $\alpha$ and $\beta$, the intersection of the ranges of the right injection $\mathrm{inr} : \beta \to \alpha \oplus \beta$ and the left injection $\mathrm{inl} : \alpha \to \alpha \oplus \beta$ is empty, i.e., $\mathrm{range}(\mathrm{inr}) \cap \mathrm{range}(\mathrm{inl}) = \emptyset$.

Set.preimage_inl_image_inr theorem

(s : Set β) : Sum.inl ⁻¹' (@Sum.inr α β '' s) = ∅

Full source

@[simp]
theorem preimage_inl_image_inr (s : Set β) : Sum.inlSum.inl ⁻¹' (@Sum.inr α β '' s) = ∅ := by
  ext
  simp

Preimage of Inr Image under Inl is Empty

Informal description

For any set $s \subseteq \beta$, the preimage of the image of $s$ under the injection $\mathrm{inr} : \beta \to \alpha \oplus \beta$ via the injection $\mathrm{inl} : \alpha \to \alpha \oplus \beta$ is the empty set, i.e., $\mathrm{inl}^{-1}(\mathrm{inr}(s)) = \emptyset$.

Set.preimage_inr_image_inl theorem

(s : Set α) : Sum.inr ⁻¹' (@Sum.inl α β '' s) = ∅

Full source

@[simp]
theorem preimage_inr_image_inl (s : Set α) : Sum.inrSum.inr ⁻¹' (@Sum.inl α β '' s) = ∅ := by
  ext
  simp

Preimage of Inl Image under Inr is Empty

Informal description

For any set $s \subseteq \alpha$, the preimage of the image of $s$ under the injection $\mathrm{inl} : \alpha \to \alpha \oplus \beta$ via the injection $\mathrm{inr} : \beta \to \alpha \oplus \beta$ is the empty set, i.e., $\mathrm{inr}^{-1}(\mathrm{inl}(s)) = \emptyset$.

Set.preimage_inl_range_inr theorem

: Sum.inl ⁻¹' range (Sum.inr : β → α ⊕ β) = ∅

Full source

@[simp]
theorem preimage_inl_range_inr : Sum.inlSum.inl ⁻¹' range (Sum.inr : β → α ⊕ β) = ∅ := by
  rw [← image_univ, preimage_inl_image_inr]

Preimage of Inr Range under Inl is Empty

Informal description

For any types $\alpha$ and $\beta$, the preimage of the range of the injection $\mathrm{inr} : \beta \to \alpha \oplus \beta$ under the injection $\mathrm{inl} : \alpha \to \alpha \oplus \beta$ is the empty set, i.e., $\mathrm{inl}^{-1}(\mathrm{range}(\mathrm{inr})) = \emptyset$.

Set.preimage_inr_range_inl theorem

: Sum.inr ⁻¹' range (Sum.inl : α → α ⊕ β) = ∅

Full source

@[simp]
theorem preimage_inr_range_inl : Sum.inrSum.inr ⁻¹' range (Sum.inl : α → α ⊕ β) = ∅ := by
  rw [← image_univ, preimage_inr_image_inl]

Preimage of Left Injection's Range under Right Injection is Empty

Informal description

For any types $\alpha$ and $\beta$, the preimage of the range of the left injection $\mathrm{inl} : \alpha \to \alpha \oplus \beta$ under the right injection $\mathrm{inr} : \beta \to \alpha \oplus \beta$ is the empty set, i.e., $\mathrm{inr}^{-1}(\mathrm{range}(\mathrm{inl})) = \emptyset$.

Set.compl_range_inl theorem

: (range (Sum.inl : α → α ⊕ β))ᶜ = range (Sum.inr : β → α ⊕ β)

Full source

@[simp]
theorem compl_range_inl : (range (Sum.inl : α → α ⊕ β))ᶜ = range (Sum.inr : β → α ⊕ β) :=
  IsCompl.compl_eq isCompl_range_inl_range_inr

Complement of Left Injection's Range Equals Right Injection's Range in Sum Type

Informal description

For any types $\alpha$ and $\beta$, the complement of the range of the left injection $\mathrm{inl} : \alpha \to \alpha \oplus \beta$ is equal to the range of the right injection $\mathrm{inr} : \beta \to \alpha \oplus \beta$, i.e., $$(\mathrm{range}(\mathrm{inl}))^c = \mathrm{range}(\mathrm{inr}).$$

Set.compl_range_inr theorem

: (range (Sum.inr : β → α ⊕ β))ᶜ = range (Sum.inl : α → α ⊕ β)

Full source

@[simp]
theorem compl_range_inr : (range (Sum.inr : β → α ⊕ β))ᶜ = range (Sum.inl : α → α ⊕ β) :=
  IsCompl.compl_eq isCompl_range_inl_range_inr.symm

Complement of Right Injection Range Equals Left Injection Range in Sum Type

Informal description

For any types $\alpha$ and $\beta$, the complement of the range of the right injection $\mathrm{inr} : \beta \to \alpha \oplus \beta$ is equal to the range of the left injection $\mathrm{inl} : \alpha \to \alpha \oplus \beta$, i.e., $(\mathrm{range}(\mathrm{inr}))^c = \mathrm{range}(\mathrm{inl})$.

Set.image_preimage_inl_union_image_preimage_inr theorem

(s : Set (α ⊕ β)) : Sum.inl '' (Sum.inl ⁻¹' s) ∪ Sum.inr '' (Sum.inr ⁻¹' s) = s

Full source

theorem image_preimage_inl_union_image_preimage_inr (s : Set (α ⊕ β)) :
    Sum.inlSum.inl '' (Sum.inl ⁻¹' s)Sum.inl '' (Sum.inl ⁻¹' s) ∪ Sum.inr '' (Sum.inr ⁻¹' s) = s := by
  rw [image_preimage_eq_inter_range, image_preimage_eq_inter_range, ← inter_union_distrib_left,
    range_inl_union_range_inr, inter_univ]

Decomposition of Sum Set via Left and Right Injections: $\mathrm{inl}(\mathrm{inl}^{-1}(s)) \cup \mathrm{inr}(\mathrm{inr}^{-1}(s)) = s$

Informal description

For any set $s$ in the sum type $\alpha \oplus \beta$, the union of the images of the preimages of $s$ under the left injection $\mathrm{inl} : \alpha \to \alpha \oplus \beta$ and the right injection $\mathrm{inr} : \beta \to \alpha \oplus \beta$ equals $s$ itself. That is, $$ \mathrm{inl}(\mathrm{inl}^{-1}(s)) \cup \mathrm{inr}(\mathrm{inr}^{-1}(s)) = s. $$

Set.range_quot_mk theorem

(r : α → α → Prop) : range (Quot.mk r) = univ

Full source

@[simp]
theorem range_quot_mk (r : α → α → Prop) : range (Quot.mk r) = univ :=
  Quot.mk_surjective.range_eq

Range of Quotient Map is Universal Set

Informal description

For any relation $r$ on a type $\alpha$, the range of the quotient map $\operatorname{Quot.mk}\, r$ is equal to the universal set on the quotient type $\operatorname{Quot}\, r$.

Set.range_quot_lift theorem

{r : ι → ι → Prop} (hf : ∀ x y, r x y → f x = f y) : range (Quot.lift f hf) = range f

Full source

@[simp]
theorem range_quot_lift {r : ι → ι → Prop} (hf : ∀ x y, r x y → f x = f y) :
    range (Quot.lift f hf) = range f :=
  ext fun _ => Quot.mk_surjective.exists

Range Preservation under Quotient Lifting: $\text{range}(\operatorname{Quot.lift}\, f\, hf) = \text{range}(f)$

Informal description

Let $r$ be a binary relation on a type $\iota$ and $f : \iota \to \alpha$ be a function that respects $r$ (i.e., for all $x, y \in \iota$, if $r(x,y)$ holds then $f(x) = f(y)$). Then the range of the lifted function $\operatorname{Quot.lift}\, f\, hf$ (where $hf$ is the proof that $f$ respects $r$) is equal to the range of $f$.

Set.range_quotient_mk theorem

{s : Setoid α} : range (Quotient.mk s) = univ

Full source

@[simp]
theorem range_quotient_mk {s : Setoid α} : range (Quotient.mk s) = univ :=
  range_quot_mk _

Range of Quotient Map Equals Universal Set

Informal description

For any setoid $s$ on a type $\alpha$, the range of the quotient map $\operatorname{Quotient.mk}\, s$ is equal to the universal set on the quotient type $\operatorname{Quotient}\, s$.

Set.range_quotient_lift theorem

[s : Setoid ι] (hf) : range (Quotient.lift f hf : Quotient s → α) = range f

Full source

@[simp]
theorem range_quotient_lift [s : Setoid ι] (hf) :
    range (Quotient.lift f hf : Quotient s → α) = range f :=
  range_quot_lift _

Range Preservation under Quotient Lifting: $\text{range}(\operatorname{Quotient.lift}\, f\, hf) = \text{range}(f)$

Informal description

Let $s$ be a setoid (equivalence relation) on a type $\iota$, and let $f : \iota \to \alpha$ be a function that respects $s$ (i.e., $f$ is constant on equivalence classes of $s$). Then the range of the lifted function $\operatorname{Quotient.lift}\, f\, hf : \operatorname{Quotient}\, s \to \alpha$ (where $hf$ is the proof that $f$ respects $s$) is equal to the range of $f$.

Set.range_quotient_mk' theorem

{s : Setoid α} : range (Quotient.mk' : α → Quotient s) = univ

Full source

@[simp]
theorem range_quotient_mk' {s : Setoid α} : range (Quotient.mk' : α → Quotient s) = univ :=
  range_quot_mk _

Range of Quotient Map Equals Universal Set (variant)

Informal description

For any setoid $s$ on a type $\alpha$, the range of the quotient map $\operatorname{Quotient.mk'}$ from $\alpha$ to the quotient type $\operatorname{Quotient}\, s$ is equal to the universal set on $\operatorname{Quotient}\, s$.

Set.Quotient.range_mk'' theorem

{sa : Setoid α} : range (Quotient.mk'' (s₁ := sa)) = univ

Full source

lemma Quotient.range_mk'' {sa : Setoid α} : range (Quotient.mk'' (s₁ := sa)) = univ :=
  range_quotient_mk

Range of Quotient Map Equals Universal Set (variant)

Informal description

For any setoid $s$ on a type $\alpha$, the range of the quotient map $\operatorname{Quotient.mk''}$ (with respect to $s$) is equal to the universal set on the quotient type $\operatorname{Quotient}\, s$.

Set.range_quotient_lift_on' theorem

{s : Setoid ι} (hf) : (range fun x : Quotient s => Quotient.liftOn' x f hf) = range f

Full source

@[simp]
theorem range_quotient_lift_on' {s : Setoid ι} (hf) :
    (range fun x : Quotient s => Quotient.liftOn' x f hf) = range f :=
  range_quot_lift _

Range Equality for Quotient Lift: $\text{range}(\operatorname{Quotient.liftOn'}\, f\, hf) = \text{range}(f)$

Informal description

Let $s$ be a setoid on $\iota$ and $f : \iota \to \alpha$ be a function that respects the equivalence relation $s$ (i.e., for all $x, y \in \iota$, if $x \sim y$ then $f(x) = f(y)$). Then the range of the function $\operatorname{Quotient.liftOn'}\, x\, f\, hf$ (where $hf$ is the proof that $f$ respects $s$) is equal to the range of $f$.

Set.canLift instance

(c) (p) [CanLift α β c p] : CanLift (Set α) (Set β) (c '' ·) fun s => ∀ x ∈ s, p x

Full source

instance canLift (c) (p) [CanLift α β c p] :
    CanLift (Set α) (Set β) (c '' ·) fun s => ∀ x ∈ s, p x where
  prf _ hs := subset_range_iff_exists_image_eq.mp fun x hx => CanLift.prf _ (hs x hx)

Lifting Condition for Sets via Image

Informal description

For any types $\alpha$ and $\beta$ with a lifting condition `CanLift α β c p` (where $c : \beta \to \alpha$ is the lifting function and $p$ is the condition), there exists a lifting condition for sets `CanLift (Set α) (Set β)` where the lifting function is the image under $c$ (i.e., $c '' \cdot$) and the condition is that for every element $x$ in the set, $p(x)$ holds.

Set.range_const_subset theorem

{c : α} : (range fun _ : ι => c) ⊆ { c }

Full source

theorem range_const_subset {c : α} : (range fun _ : ι => c) ⊆ {c} :=
  range_subset_iff.2 fun _ => rfl

Range of Constant Function is Subset of Singleton

Informal description

For any constant function $f : \iota \to \alpha$ defined by $f(x) = c$ for some fixed $c \in \alpha$, the range of $f$ is a subset of the singleton set $\{c\}$.

Set.range_const theorem

: ∀ [Nonempty ι] {c : α}, (range fun _ : ι => c) = { c }

Full source

@[simp]
theorem range_const : ∀ [Nonempty ι] {c : α}, (range fun _ : ι => c) = {c}
  | ⟨x⟩, _ =>
    (Subset.antisymm range_const_subset) fun _ hy =>
      (mem_singleton_iff.1 hy).symm ▸ mem_range_self x

Range of Constant Function is Singleton Set

Informal description

For any nonempty type $\iota$ and any element $c$ of type $\alpha$, the range of the constant function $f : \iota \to \alpha$ defined by $f(x) = c$ for all $x \in \iota$ is equal to the singleton set $\{c\}$.

Set.range_subtype_map theorem

 {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ x, p x → q (f x)) : range (Subtype.map f h) = (↑) ⁻¹' (f '' {x | p x})

Full source

theorem range_subtype_map {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ x, p x → q (f x)) :
    range (Subtype.map f h) = (↑) ⁻¹' (f '' { x | p x }) := by
  ext ⟨x, hx⟩
  simp_rw [mem_preimage, mem_range, mem_image, Subtype.exists, Subtype.map]
  simp only [Subtype.mk.injEq, exists_prop, mem_setOf_eq]

Range of Subtype Map Equals Preimage of Image

Informal description

Let $p : \alpha \to \mathrm{Prop}$ and $q : \beta \to \mathrm{Prop}$ be predicates, and let $f : \alpha \to \beta$ be a function such that for all $x \in \alpha$, if $p(x)$ holds then $q(f(x))$ holds. Then the range of the restricted map $\mathrm{Subtype.map}\,f\,h$ (where $h$ is the proof of the implication) is equal to the preimage under the inclusion map of the image of $\{x \mid p(x)\}$ under $f$.

Set.image_swap_eq_preimage_swap theorem

: image (@Prod.swap α β) = preimage Prod.swap

Full source

theorem image_swap_eq_preimage_swap : image (@Prod.swap α β) = preimage Prod.swap :=
  image_eq_preimage_of_inverse Prod.swap_leftInverse Prod.swap_rightInverse

Image Equals Preimage under Swap Function

Informal description

For any types $\alpha$ and $\beta$, the image operation under the swap function $\text{swap} : \alpha \times \beta \to \beta \times \alpha$ is equal to the preimage operation under the same swap function. In other words, for any subset $s \subseteq \alpha \times \beta$, we have $\text{swap}(s) = \text{swap}^{-1}(s)$.

Set.preimage_singleton_nonempty theorem

{f : α → β} {y : β} : (f ⁻¹' { y }).Nonempty ↔ y ∈ range f

Full source

theorem preimage_singleton_nonempty {f : α → β} {y : β} : (f ⁻¹' {y}).Nonempty ↔ y ∈ range f :=
  Iff.rfl

Nonempty Preimage of Singleton vs. Membership in Range

Informal description

For any function $f \colon \alpha \to \beta$ and any element $y \in \beta$, the preimage $f^{-1}(\{y\})$ is nonempty if and only if $y$ belongs to the range of $f$.

Set.preimage_singleton_eq_empty theorem

{f : α → β} {y : β} : f ⁻¹' { y } = ∅ ↔ y ∉ range f

Full source

theorem preimage_singleton_eq_empty {f : α → β} {y : β} : f ⁻¹' {y}f ⁻¹' {y} = ∅ ↔ y ∉ range f :=
  not_nonempty_iff_eq_empty.symm.trans preimage_singleton_nonempty.not

Empty Preimage of Singleton vs. Non-membership in Range

Informal description

For any function $f \colon \alpha \to \beta$ and any element $y \in \beta$, the preimage $f^{-1}(\{y\})$ is empty if and only if $y$ does not belong to the range of $f$.

Set.range_subset_singleton theorem

{f : ι → α} {x : α} : range f ⊆ { x } ↔ f = const ι x

Full source

theorem range_subset_singleton {f : ι → α} {x : α} : rangerange f ⊆ {x}range f ⊆ {x} ↔ f = const ι x := by
  simp [range_subset_iff, funext_iff, mem_singleton]

Range Subset of Singleton iff Function is Constant

Informal description

For any function $f \colon \iota \to \alpha$ and any element $x \in \alpha$, the range of $f$ is a subset of the singleton set $\{x\}$ if and only if $f$ is the constant function that maps every element of $\iota$ to $x$.

Set.image_compl_preimage theorem

{f : α → β} {s : Set β} : f '' (f ⁻¹' s)ᶜ = range f \ s

Full source

theorem image_compl_preimage {f : α → β} {s : Set β} : f '' (f ⁻¹' s)ᶜ = rangerange f \ s := by
  rw [compl_eq_univ_diff, image_diff_preimage, image_univ]

Image of Complement of Preimage Equals Range Difference: $f((f^{-1}(s))^c) = \text{range}(f) \setminus s$

Informal description

For any function $f \colon \alpha \to \beta$ and any subset $s \subseteq \beta$, the image of the complement of the preimage $f^{-1}(s)$ under $f$ equals the set difference between the range of $f$ and $s$, i.e., \[ f\big((f^{-1}(s))^c\big) = \text{range}(f) \setminus s. \]

Set.rangeFactorization_eq theorem

{f : ι → β} : Subtype.val ∘ rangeFactorization f = f

Full source

theorem rangeFactorization_eq {f : ι → β} : Subtype.valSubtype.val ∘ rangeFactorization f = f :=
  funext fun _ => rfl

Range Factorization Preserves Original Function

Informal description

For any function $f : \iota \to \beta$, the composition of the range factorization of $f$ with the subtype inclusion map equals $f$ itself. In other words, if we factor $f$ through its range and then project back to $\beta$, we recover the original function $f$.

Set.rangeFactorization_coe theorem

(f : ι → β) (a : ι) : (rangeFactorization f a : β) = f a

Full source

@[simp]
theorem rangeFactorization_coe (f : ι → β) (a : ι) : (rangeFactorization f a : β) = f a :=
  rfl

Range Factorization Preserves Function Values

Informal description

For any function $f : \iota \to \beta$ and any element $a \in \iota$, the value of the range factorization of $f$ at $a$, when coerced back to $\beta$, equals $f(a)$. In other words, if we let $g := \text{rangeFactorization}(f)$, then $g(a) = (f(a), p)$ where $p$ is a proof that $f(a) \in \text{range}(f)$, and thus $(g(a) : \beta) = f(a)$.

Set.coe_comp_rangeFactorization theorem

(f : ι → β) : (↑) ∘ rangeFactorization f = f

Full source

@[simp]
theorem coe_comp_rangeFactorization (f : ι → β) : (↑) ∘ rangeFactorization f = f := rfl

Commutativity of Range Factorization with Inclusion: $(\uparrow \circ \text{rangeFactorization }f) = f$

Informal description

For any function $f : \iota \to \beta$, the composition of the range factorization of $f$ with the inclusion map from $\text{range}(f)$ to $\beta$ equals $f$ itself. In other words, the following diagram commutes: $$ \iota \xrightarrow{\text{rangeFactorization }f} \text{range}(f) \xrightarrow{\subseteq} \beta $$ where the composition along the bottom path is equal to $f$.

Set.surjective_onto_range theorem

: Surjective (rangeFactorization f)

Full source

theorem surjective_onto_range : Surjective (rangeFactorization f) := fun ⟨_, ⟨i, rfl⟩⟩ => ⟨i, rfl⟩

Surjectivity of Range Factorization

Informal description

For any function $f : \iota \to \alpha$, the range factorization of $f$ is surjective. That is, for every element $y$ in the range of $f$, there exists an element $x \in \iota$ such that $f(x) = y$.

Set.image_eq_range theorem

(f : α → β) (s : Set α) : f '' s = range fun x : s => f x

Full source

theorem image_eq_range (f : α → β) (s : Set α) : f '' s = range fun x : s => f x := by
  ext
  constructor
  · rintro ⟨x, h1, h2⟩
    exact ⟨⟨x, h1⟩, h2⟩
  · rintro ⟨⟨x, h1⟩, h2⟩
    exact ⟨x, h1, h2⟩

Image as Range of Restriction: $f(s) = \text{range}(f|_s)$

Informal description

For any function $f : \alpha \to \beta$ and any subset $s \subseteq \alpha$, the image of $s$ under $f$ is equal to the range of the restriction of $f$ to $s$, i.e., $$ f(s) = \{f(x) \mid x \in s\} = \text{range}(f|_s). $$

Sum.range_eq theorem

(f : α ⊕ β → γ) : range f = range (f ∘ Sum.inl) ∪ range (f ∘ Sum.inr)

Full source

theorem _root_.Sum.range_eq (f : α ⊕ β → γ) :
    range f = rangerange (f ∘ Sum.inl) ∪ range (f ∘ Sum.inr) :=
  ext fun _ => Sum.exists

Range Decomposition for Sum Types: $\text{range}(f) = \text{range}(f \circ \text{inl}) \cup \text{range}(f \circ \text{inr})$

Informal description

For any function $f : \alpha \oplus \beta \to \gamma$, the range of $f$ is equal to the union of the ranges of the compositions $f \circ \text{inl}$ and $f \circ \text{inr}$, where $\text{inl} : \alpha \to \alpha \oplus \beta$ and $\text{inr} : \beta \to \alpha \oplus \beta$ are the canonical injections. That is, $$\text{range}(f) = \text{range}(f \circ \text{inl}) \cup \text{range}(f \circ \text{inr}).$$

Set.Sum.elim_range theorem

(f : α → γ) (g : β → γ) : range (Sum.elim f g) = range f ∪ range g

Full source

@[simp]
theorem Sum.elim_range (f : α → γ) (g : β → γ) : range (Sum.elim f g) = rangerange f ∪ range g :=
  Sum.range_eq _

Range of Sum Elimination Equals Union of Ranges

Informal description

For any functions $f \colon \alpha \to \gamma$ and $g \colon \beta \to \gamma$, the range of the function $\mathrm{Sum.elim}\,f\,g \colon \alpha \oplus \beta \to \gamma$ is equal to the union of the ranges of $f$ and $g$, i.e., $$\mathrm{range}(\mathrm{Sum.elim}\,f\,g) = \mathrm{range}(f) \cup \mathrm{range}(g).$$

Set.range_ite_subset' theorem

{p : Prop} [Decidable p] {f g : α → β} : range (if p then f else g) ⊆ range f ∪ range g

Full source

theorem range_ite_subset' {p : Prop} [Decidable p] {f g : α → β} :
    rangerange (if p then f else g) ⊆ range f ∪ range g := by
  by_cases h : p
  · rw [if_pos h]
    exact subset_union_left
  · rw [if_neg h]
    exact subset_union_right

Range of Conditional Function is Subset of Union of Ranges

Informal description

For any proposition $p$ with a decision procedure, and any functions $f, g : \alpha \to \beta$, the range of the function defined by $\text{if } p \text{ then } f \text{ else } g$ is a subset of the union of the ranges of $f$ and $g$, i.e., $$\text{range}(\text{if } p \text{ then } f \text{ else } g) \subseteq \text{range}(f) \cup \text{range}(g).$$

Set.range_ite_subset theorem

 {p : α → Prop} [DecidablePred p] {f g : α → β} : (range fun x => if p x then f x else g x) ⊆ range f ∪ range g

Full source

theorem range_ite_subset {p : α → Prop} [DecidablePred p] {f g : α → β} :
    (range fun x => if p x then f x else g x) ⊆ range f ∪ range g := by
  rw [range_subset_iff]; intro x; by_cases h : p x
  · simp only [if_pos h, mem_union, mem_range, exists_apply_eq_apply, true_or]
  · simp [if_neg h, mem_union, mem_range_self]

Range of Piecewise Function is Subset of Union of Ranges

Informal description

For any predicate $p$ on a type $\alpha$ (with a decidable instance), and any functions $f, g : \alpha \to \beta$, the range of the piecewise function $x \mapsto \text{if } p(x) \text{ then } f(x) \text{ else } g(x)$ is contained in the union of the ranges of $f$ and $g$. That is, $$\mathrm{range}\left(x \mapsto \begin{cases} f(x) & \text{if } p(x) \\ g(x) & \text{otherwise} \end{cases}\right) \subseteq \mathrm{range}(f) \cup \mathrm{range}(g).$$

Set.preimage_range theorem

(f : α → β) : f ⁻¹' range f = univ

Full source

@[simp]
theorem preimage_range (f : α → β) : f ⁻¹' range f = univ :=
  eq_univ_of_forall mem_range_self

Preimage of Range is Universal Set

Informal description

For any function $f : \alpha \to \beta$, the preimage of the range of $f$ under $f$ is equal to the universal set on $\alpha$, i.e., $f^{-1}(\mathrm{range}(f)) = \mathrm{univ}$.

Set.range_unique theorem

[h : Unique ι] : range f = {f default}

Full source

/-- The range of a function from a `Unique` type contains just the
function applied to its single value. -/
theorem range_unique [h : Unique ι] : range f = {f default} := by
  ext x
  rw [mem_range]
  constructor
  · rintro ⟨i, hi⟩
    rw [h.uniq i] at hi
    exact hi ▸ mem_singleton _
  · exact fun h => ⟨default, h.symm⟩

Range of a Function on a Unique Type is a Singleton

Informal description

For a function $f$ from a type $\iota$ with a unique element, the range of $f$ is the singleton set containing the image of the default element of $\iota$ under $f$, i.e., $\mathrm{range}(f) = \{f(\mathrm{default})\}$.

Set.range_diff_image_subset theorem

(f : α → β) (s : Set α) : range f \ f '' s ⊆ f '' sᶜ

Full source

theorem range_diff_image_subset (f : α → β) (s : Set α) : rangerange f \ f '' srange f \ f '' s ⊆ f '' sᶜ :=
  fun _ ⟨⟨x, h₁⟩, h₂⟩ => ⟨x, fun h => h₂ ⟨x, h, h₁⟩, h₁⟩

Range Minus Image is Subset of Complement's Image

Informal description

For any function $f : \alpha \to \beta$ and any subset $s \subseteq \alpha$, the set difference between the range of $f$ and the image of $s$ under $f$ is a subset of the image of the complement of $s$ under $f$. In other words, $\mathrm{range}(f) \setminus f(s) \subseteq f(s^c)$.

Set.range_inclusion theorem

(h : s ⊆ t) : range (inclusion h) = {x : t | (x : α) ∈ s}

Full source

@[simp]
theorem range_inclusion (h : s ⊆ t) : range (inclusion h) = { x : t | (x : α) ∈ s } := by
  ext ⟨x, hx⟩
  simp

Range of Subset Inclusion Equals Subset Viewed in Larger Set

Informal description

For any subsets $s$ and $t$ of a type $\alpha$ with $s \subseteq t$, the range of the canonical inclusion map $\text{inclusion}(h) : s \to t$ is equal to the set $\{x \in t \mid x \in s\}$.

Set.leftInverse_rangeSplitting theorem

(f : α → β) : LeftInverse (rangeFactorization f) (rangeSplitting f)

Full source

theorem leftInverse_rangeSplitting (f : α → β) :
    LeftInverse (rangeFactorization f) (rangeSplitting f) := fun x => by
  ext
  simp only [rangeFactorization_coe]
  apply apply_rangeSplitting

Range Factorization is Left Inverse of Range Splitting

Informal description

For any function $f : \alpha \to \beta$, the range factorization of $f$ is a left inverse of the range splitting function. That is, for every $x$ in the range of $f$, we have $\text{rangeFactorization}\, f\, (\text{rangeSplitting}\, f\, x) = x$.

Set.rangeSplitting_injective theorem

(f : α → β) : Injective (rangeSplitting f)

Full source

theorem rangeSplitting_injective (f : α → β) : Injective (rangeSplitting f) :=
  (leftInverse_rangeSplitting f).injective

Injectivity of the Range Splitting Function

Informal description

For any function $f : \alpha \to \beta$, the range splitting function $\text{rangeSplitting}\, f : \text{range}\, f \to \alpha$ is injective. That is, for any $y_1, y_2$ in the range of $f$, if $\text{rangeSplitting}\, f\, y_1 = \text{rangeSplitting}\, f\, y_2$, then $y_1 = y_2$.

Set.rightInverse_rangeSplitting theorem

{f : α → β} (h : Injective f) : RightInverse (rangeFactorization f) (rangeSplitting f)

Full source

theorem rightInverse_rangeSplitting {f : α → β} (h : Injective f) :
    RightInverse (rangeFactorization f) (rangeSplitting f) :=
  (leftInverse_rangeSplitting f).rightInverse_of_injective fun _ _ hxy =>
    h <| Subtype.ext_iff.1 hxy

Range Factorization is Right Inverse of Range Splitting for Injective Functions

Informal description

For any injective function $f : \alpha \to \beta$, the range factorization of $f$ is a right inverse of the range splitting function. That is, for every $x \in \alpha$, we have $f(\text{rangeSplitting}\, f\, (\text{rangeFactorization}\, f\, x)) = f(x)$.

Set.preimage_rangeSplitting theorem

{f : α → β} (hf : Injective f) : preimage (rangeSplitting f) = image (rangeFactorization f)

Full source

theorem preimage_rangeSplitting {f : α → β} (hf : Injective f) :
    preimage (rangeSplitting f) = image (rangeFactorization f) :=
  (image_eq_preimage_of_inverse (rightInverse_rangeSplitting hf)
      (leftInverse_rangeSplitting f)).symm

Preimage-Image Correspondence for Range Splitting and Factorization of Injective Functions

Informal description

For any injective function $f : \alpha \to \beta$, the preimage operation under the range splitting function $\text{rangeSplitting}\, f$ coincides with the image operation under the range factorization function $\text{rangeFactorization}\, f$. That is, for any subset $s \subseteq \alpha$, we have $(\text{rangeSplitting}\, f)^{-1}(s) = \text{rangeFactorization}\, f(s)$.

Set.isCompl_range_some_none theorem

(α : Type*) : IsCompl (range (some : α → Option α)) { none }

Full source

theorem isCompl_range_some_none (α : Type*) : IsCompl (range (some : α → Option α)) {none} :=
  IsCompl.of_le (fun _ ⟨⟨_, ha⟩, (hn : _ = none)⟩ => Option.some_ne_none _ (ha.trans hn))
    fun x _ => Option.casesOn x (Or.inr rfl) fun _ => Or.inl <| mem_range_self _

Complementarity of `some` Range and `none` in Option Type

Informal description

For any type $\alpha$, the range of the `some` function (which maps elements of $\alpha$ to `Option α`) and the singleton set containing `none` form complementary subsets in `Option α$. That is, they are disjoint and their union is the entire space.

Set.compl_range_some theorem

(α : Type*) : (range (some : α → Option α))ᶜ = { none }

Full source

@[simp]
theorem compl_range_some (α : Type*) : (range (some : α → Option α))ᶜ = {none} :=
  (isCompl_range_some_none α).compl_eq

Complement of Range of `some` is `{none}` in Option Type

Informal description

For any type $\alpha$, the complement of the range of the `some` function (which maps elements of $\alpha$ to `Option α`) is equal to the singleton set containing `none`. In other words, $(range(some : \alpha \to Option \alpha))^c = \{none\}$.

Set.range_some_inter_none theorem

(α : Type*) : range (some : α → Option α) ∩ { none } = ∅

Full source

@[simp]
theorem range_some_inter_none (α : Type*) : rangerange (some : α → Option α) ∩ {none} = ∅ :=
  (isCompl_range_some_none α).inf_eq_bot

Disjointness of `some` Range and `none` in Option Type

Informal description

For any type $\alpha$, the intersection of the range of the `some` function (which maps elements of $\alpha$ to `Option α`) and the singleton set containing `none` is empty. That is, $\text{range}(\text{some}) \cap \{\text{none}\} = \emptyset$.

Set.range_some_union_none theorem

(α : Type*) : range (some : α → Option α) ∪ { none } = univ

Full source

theorem range_some_union_none (α : Type*) : rangerange (some : α → Option α) ∪ {none} = univ :=
  (isCompl_range_some_none α).sup_eq_top

Universal Coverage of `Option α` by `some` and `none`

Informal description

For any type $\alpha$, the union of the range of the `some` function (which maps elements of $\alpha$ to `Option α`) and the singleton set containing `none` equals the universal set of `Option α$. That is, every element in `Option α` is either in the range of `some` or is `none`.

Set.insert_none_range_some theorem

(α : Type*) : insert none (range (some : α → Option α)) = univ

Full source

@[simp]
theorem insert_none_range_some (α : Type*) : insert none (range (some : α → Option α)) = univ :=
  (isCompl_range_some_none α).symm.sup_eq_top

Universal Coverage of Option Type via `none` and `some`

Informal description

For any type $\alpha$, the union of the singleton set containing `none` and the range of the `some` function (which maps elements of $\alpha$ to `Option α`) equals the universal set of `Option α$. That is, $\{\text{none}\} \cup \text{range}(\text{some}) = \text{univ}$.

Set.image_of_range_union_range_eq_univ theorem

 {α β γ γ' δ δ' : Type*} {h : β → α} {f : γ → β} {f₁ : γ' → α} {f₂ : γ → γ'} {g : δ → β} {g₁ : δ' → α} {g₂ : δ → δ'}
  (hf : h ∘ f = f₁ ∘ f₂) (hg : h ∘ g = g₁ ∘ g₂) (hfg : range f ∪ range g = univ) (s : Set β) :
  h '' s = f₁ '' (f₂ '' (f ⁻¹' s)) ∪ g₁ '' (g₂ '' (g ⁻¹' s))

Full source

lemma image_of_range_union_range_eq_univ {α β γ γ' δ δ' : Type*}
    {h : β → α} {f : γ → β} {f₁ : γ' → α} {f₂ : γ → γ'} {g : δ → β} {g₁ : δ' → α} {g₂ : δ → δ'}
    (hf : h ∘ f = f₁ ∘ f₂) (hg : h ∘ g = g₁ ∘ g₂) (hfg : rangerange f ∪ range g = univ) (s : Set β) :
    h '' s = f₁ '' (f₂ '' (f ⁻¹' s))f₁ '' (f₂ '' (f ⁻¹' s)) ∪ g₁ '' (g₂ '' (g ⁻¹' s)) := by
  rw [← image_comp, ← image_comp, ← hf, ← hg, image_comp, image_comp, image_preimage_eq_inter_range,
    image_preimage_eq_inter_range, ← image_union, ← inter_union_distrib_left, hfg, inter_univ]

Decomposition of Image via Range-Covering Functions

Informal description

Let $h : \beta \to \alpha$, $f : \gamma \to \beta$, $f_1 : \gamma' \to \alpha$, $f_2 : \gamma \to \gamma'$, $g : \delta \to \beta$, $g_1 : \delta' \to \alpha$, and $g_2 : \delta \to \delta'$ be functions such that: 1. $h \circ f = f_1 \circ f_2$, 2. $h \circ g = g_1 \circ g_2$, 3. The union of the ranges of $f$ and $g$ is the universal set of $\beta$. Then for any subset $s \subseteq \beta$, the image of $s$ under $h$ satisfies: $$ h(s) = f_1(f_2(f^{-1}(s))) \cup g_1(g_2(g^{-1}(s))). $$

Set.Subsingleton.image theorem

(hs : s.Subsingleton) (f : α → β) : (f '' s).Subsingleton

Full source

/-- The image of a subsingleton is a subsingleton. -/
theorem Subsingleton.image (hs : s.Subsingleton) (f : α → β) : (f '' s).Subsingleton :=
  fun _ ⟨_, hx, Hx⟩ _ ⟨_, hy, Hy⟩ => Hx ▸ Hy ▸ congr_arg f (hs hx hy)

Image of a Subsingleton is Subsingleton

Informal description

If $s$ is a subsingleton set in $\alpha$ (i.e., $s$ contains at most one element), then for any function $f : \alpha \to \beta$, the image $f(s)$ is also a subsingleton set in $\beta$.

Set.Subsingleton.preimage theorem

{s : Set β} (hs : s.Subsingleton) (hf : Function.Injective f) : (f ⁻¹' s).Subsingleton

Full source

/-- The preimage of a subsingleton under an injective map is a subsingleton. -/
theorem Subsingleton.preimage {s : Set β} (hs : s.Subsingleton)
    (hf : Function.Injective f) : (f ⁻¹' s).Subsingleton := fun _ ha _ hb => hf <| hs ha hb

Preimage of a Subsingleton under an Injective Function is Subsingleton

Informal description

Let $f : \alpha \to \beta$ be an injective function and $s \subseteq \beta$ be a subsingleton set. Then the preimage $f^{-1}(s) \subseteq \alpha$ is also a subsingleton set.

Set.subsingleton_of_image theorem

(hf : Function.Injective f) (s : Set α) (hs : (f '' s).Subsingleton) : s.Subsingleton

Full source

/-- If the image of a set under an injective map is a subsingleton, the set is a subsingleton. -/
theorem subsingleton_of_image (hf : Function.Injective f) (s : Set α)
    (hs : (f '' s).Subsingleton) : s.Subsingleton :=
  (hs.preimage hf).anti <| subset_preimage_image _ _

Inverse Image of Subsingleton under Injective Function is Subsingleton

Informal description

Let $f : \alpha \to \beta$ be an injective function and $s \subseteq \alpha$ a subset. If the image $f(s)$ is a subsingleton (i.e., contains at most one element), then $s$ is also a subsingleton.

Set.subsingleton_of_preimage theorem

(hf : Function.Surjective f) (s : Set β) (hs : (f ⁻¹' s).Subsingleton) : s.Subsingleton

Full source

/-- If the preimage of a set under a surjective map is a subsingleton,
the set is a subsingleton. -/
theorem subsingleton_of_preimage (hf : Function.Surjective f) (s : Set β)
    (hs : (f ⁻¹' s).Subsingleton) : s.Subsingleton := fun fx hx fy hy => by
  rcases hf fx, hf fy with ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩
  exact congr_arg f (hs hx hy)

Subsingleton Property of Image under Surjective Function via Preimage Condition

Informal description

Let $f : \alpha \to \beta$ be a surjective function and $s \subseteq \beta$ a subset. If the preimage $f^{-1}(s)$ is a subsingleton (i.e., contains at most one element), then $s$ itself is a subsingleton.

Set.subsingleton_range theorem

{α : Sort*} [Subsingleton α] (f : α → β) : (range f).Subsingleton

Full source

theorem subsingleton_range {α : Sort*} [Subsingleton α] (f : α → β) : (range f).Subsingleton :=
  forall_mem_range.2 fun x => forall_mem_range.2 fun y => congr_arg f (Subsingleton.elim x y)

Range of a Function from a Subsingleton is Subsingleton

Informal description

For any function $f : \alpha \to \beta$ where $\alpha$ is a subsingleton type (i.e., all elements of $\alpha$ are equal), the range of $f$ is a subsingleton set (i.e., contains at most one distinct element).

Set.Nontrivial.preimage theorem

{s : Set β} (hs : s.Nontrivial) (hf : Function.Surjective f) : (f ⁻¹' s).Nontrivial

Full source

/-- The preimage of a nontrivial set under a surjective map is nontrivial. -/
theorem Nontrivial.preimage {s : Set β} (hs : s.Nontrivial)
    (hf : Function.Surjective f) : (f ⁻¹' s).Nontrivial := by
  rcases hs with ⟨fx, hx, fy, hy, hxy⟩
  rcases hf fx, hf fy with ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩
  exact ⟨x, hx, y, hy, mt (congr_arg f) hxy⟩

Nontriviality of Preimage under Surjective Map

Informal description

For any nontrivial subset $s \subseteq \beta$ and any surjective function $f : \alpha \to \beta$, the preimage $f^{-1}(s)$ is also nontrivial. That is, there exist distinct elements $x, y \in \alpha$ such that $f(x), f(y) \in s$.

Set.Nontrivial.image theorem

(hs : s.Nontrivial) (hf : Function.Injective f) : (f '' s).Nontrivial

Full source

/-- The image of a nontrivial set under an injective map is nontrivial. -/
theorem Nontrivial.image (hs : s.Nontrivial) (hf : Function.Injective f) :
    (f '' s).Nontrivial :=
  let ⟨x, hx, y, hy, hxy⟩ := hs
  ⟨f x, mem_image_of_mem f hx, f y, mem_image_of_mem f hy, hf.ne hxy⟩

Injective Maps Preserve Nontriviality of Sets

Informal description

For any nontrivial subset $s \subseteq \alpha$ and any injective function $f : \alpha \to \beta$, the image $f(s)$ is also nontrivial. That is, there exist distinct elements $x, y \in s$ such that $f(x) \neq f(y)$.

Set.Nontrivial.image_of_injOn theorem

(hs : s.Nontrivial) (hf : s.InjOn f) : (f '' s).Nontrivial

Full source

theorem Nontrivial.image_of_injOn (hs : s.Nontrivial) (hf : s.InjOn f) :
    (f '' s).Nontrivial := by
  obtain ⟨x, hx, y, hy, hxy⟩ := hs
  exact ⟨f x, mem_image_of_mem _ hx, f y, mem_image_of_mem _ hy, (hxy <| hf hx hy ·)⟩

Image of Nontrivial Set under Injective-on-Set Function is Nontrivial

Informal description

For any nontrivial subset $s \subseteq \alpha$ and any function $f : \alpha \to \beta$ that is injective on $s$, the image $f(s)$ is also nontrivial. That is, there exist distinct elements $f(x), f(y) \in f(s)$ for some $x, y \in s$.

Set.nontrivial_of_image theorem

(f : α → β) (s : Set α) (hs : (f '' s).Nontrivial) : s.Nontrivial

Full source

/-- If the image of a set is nontrivial, the set is nontrivial. -/
theorem nontrivial_of_image (f : α → β) (s : Set α) (hs : (f '' s).Nontrivial) : s.Nontrivial :=
  let ⟨_, ⟨x, hx, rfl⟩, _, ⟨y, hy, rfl⟩, hxy⟩ := hs
  ⟨x, hx, y, hy, mt (congr_arg f) hxy⟩

Nontriviality of Preimage from Nontrivial Image

Informal description

For any function $f : \alpha \to \beta$ and subset $s \subseteq \alpha$, if the image $f(s)$ is nontrivial (i.e., contains at least two distinct elements), then the set $s$ itself is nontrivial (i.e., contains at least two distinct elements).

Set.image_nontrivial theorem

(hf : f.Injective) : (f '' s).Nontrivial ↔ s.Nontrivial

Full source

@[simp]
theorem image_nontrivial (hf : f.Injective) : (f '' s).Nontrivial ↔ s.Nontrivial :=
  ⟨nontrivial_of_image f s, fun h ↦ h.image hf⟩

Nontriviality of Image under Injective Function: $f(s)$ is Nontrivial $\iff$ $s$ is Nontrivial

Informal description

For any injective function $f : \alpha \to \beta$ and any subset $s \subseteq \alpha$, the image $f(s)$ is nontrivial (i.e., contains at least two distinct elements) if and only if $s$ is nontrivial (i.e., contains at least two distinct elements).

Set.InjOn.image_nontrivial_iff theorem

(hf : s.InjOn f) : (f '' s).Nontrivial ↔ s.Nontrivial

Full source

@[simp]
theorem InjOn.image_nontrivial_iff (hf : s.InjOn f) :
    (f '' s).Nontrivial ↔ s.Nontrivial :=
  ⟨nontrivial_of_image f s, fun h ↦ h.image_of_injOn hf⟩

Nontriviality of Image under Injective-on-Set Function is Equivalent to Nontriviality of Domain

Informal description

For a function $f : \alpha \to \beta$ that is injective on a subset $s \subseteq \alpha$, the image $f(s)$ is nontrivial (contains at least two distinct elements) if and only if the set $s$ itself is nontrivial.

Set.nontrivial_of_preimage theorem

(hf : Function.Injective f) (s : Set β) (hs : (f ⁻¹' s).Nontrivial) : s.Nontrivial

Full source

/-- If the preimage of a set under an injective map is nontrivial, the set is nontrivial. -/
theorem nontrivial_of_preimage (hf : Function.Injective f) (s : Set β)
    (hs : (f ⁻¹' s).Nontrivial) : s.Nontrivial :=
  (hs.image hf).mono <| image_preimage_subset _ _

Nontriviality of Set via Nontrivial Preimage under Injective Function

Informal description

Let $f : \alpha \to \beta$ be an injective function and $s \subseteq \beta$ a subset. If the preimage $f^{-1}(s)$ is nontrivial (i.e., contains at least two distinct elements), then $s$ is also nontrivial.

Function.Surjective.preimage_injective theorem

(hf : Surjective f) : Injective (preimage f)

Full source

theorem Surjective.preimage_injective (hf : Surjective f) : Injective (preimage f) := fun _ _ =>
  (preimage_eq_preimage hf).1

Injectivity of Preimage under Surjective Function: $f^{-1}(s) = f^{-1}(t) \Rightarrow s = t$

Informal description

If a function $f : \alpha \to \beta$ is surjective, then the preimage function $f^{-1} : \mathcal{P}(\beta) \to \mathcal{P}(\alpha)$ is injective. That is, for any subsets $s, t \subseteq \beta$, if $f^{-1}(s) = f^{-1}(t)$, then $s = t$.

Function.Injective.preimage_image theorem

(hf : Injective f) (s : Set α) : f ⁻¹' (f '' s) = s

Full source

theorem Injective.preimage_image (hf : Injective f) (s : Set α) : f ⁻¹' (f '' s) = s :=
  preimage_image_eq s hf

Preimage-Image Equality for Injective Functions: $f^{-1}(f(s)) = s$

Informal description

For any injective function $f : \alpha \to \beta$ and any subset $s \subseteq \alpha$, the preimage of the image of $s$ under $f$ equals $s$ itself, i.e., $f^{-1}(f(s)) = s$.

Function.Injective.preimage_surjective theorem

(hf : Injective f) : Surjective (preimage f)

Full source

theorem Injective.preimage_surjective (hf : Injective f) : Surjective (preimage f) :=
  Set.preimage_surjective.mpr hf

Surjectivity of Preimage for Injective Functions: $f^{-1}(t) = s$ for any $s \subseteq \alpha$

Informal description

If a function $f : \alpha \to \beta$ is injective, then the preimage function $f^{-1} : \mathcal{P}(\beta) \to \mathcal{P}(\alpha)$ is surjective. That is, for every subset $s \subseteq \alpha$, there exists a subset $t \subseteq \beta$ such that $f^{-1}(t) = s$.

Function.Injective.subsingleton_image_iff theorem

(hf : Injective f) {s : Set α} : (f '' s).Subsingleton ↔ s.Subsingleton

Full source

theorem Injective.subsingleton_image_iff (hf : Injective f) {s : Set α} :
    (f '' s).Subsingleton ↔ s.Subsingleton :=
  ⟨subsingleton_of_image hf s, fun h => h.image f⟩

Subsingleton Image Equivalence for Injective Functions

Informal description

Let $f : \alpha \to \beta$ be an injective function and $s \subseteq \alpha$ a subset. Then the image $f(s)$ is a subsingleton (i.e., contains at most one element) if and only if $s$ is a subsingleton.

Function.Surjective.image_preimage theorem

(hf : Surjective f) (s : Set β) : f '' (f ⁻¹' s) = s

Full source

theorem Surjective.image_preimage (hf : Surjective f) (s : Set β) : f '' (f ⁻¹' s) = s :=
  image_preimage_eq s hf

Image-Preimage Equality for Surjective Functions: $f(f^{-1}(s)) = s$

Informal description

For any surjective function $f \colon \alpha \to \beta$ and any subset $s \subseteq \beta$, the image of the preimage of $s$ under $f$ equals $s$, i.e., \[ f(f^{-1}(s)) = s. \]

Function.Surjective.image_surjective theorem

(hf : Surjective f) : Surjective (image f)

Full source

theorem Surjective.image_surjective (hf : Surjective f) : Surjective (image f) := by
  intro s
  use f ⁻¹' s
  rw [hf.image_preimage]

Surjectivity of Image Function for Surjective Maps

Informal description

If a function $f \colon \alpha \to \beta$ is surjective, then the image function $f '' \colon \mathcal{P}(\alpha) \to \mathcal{P}(\beta)$ is also surjective, where $\mathcal{P}(\alpha)$ denotes the power set of $\alpha$.

Function.Surjective.nonempty_preimage theorem

(hf : Surjective f) {s : Set β} : (f ⁻¹' s).Nonempty ↔ s.Nonempty

Full source

@[simp]
theorem Surjective.nonempty_preimage (hf : Surjective f) {s : Set β} :
    (f ⁻¹' s).Nonempty ↔ s.Nonempty := by rw [← image_nonempty, hf.image_preimage]

Nonempty Preimage Characterization for Surjective Functions: $f^{-1}(s) \neq \emptyset \iff s \neq \emptyset$

Informal description

For any surjective function $f \colon \alpha \to \beta$ and any subset $s \subseteq \beta$, the preimage $f^{-1}(s)$ is nonempty if and only if $s$ is nonempty. In other words: \[ f^{-1}(s) \neq \emptyset \iff s \neq \emptyset. \]

Function.Injective.image_injective theorem

(hf : Injective f) : Injective (image f)

Full source

theorem Injective.image_injective (hf : Injective f) : Injective (image f) := by
  intro s t h
  rw [← preimage_image_eq s hf, ← preimage_image_eq t hf, h]

Injectivity of Image Function for Injective Maps

Informal description

If a function $f : \alpha \to \beta$ is injective, then the induced image function $f '' : \mathcal{P}(\alpha) \to \mathcal{P}(\beta)$ is also injective, where $\mathcal{P}(\alpha)$ denotes the power set of $\alpha$.

Function.Injective.image_strictMono theorem

(inj : Function.Injective f) : StrictMono (image f)

Full source

lemma Injective.image_strictMono (inj : Function.Injective f) : StrictMono (image f) :=
  monotone_image.strictMono_of_injective inj.image_injective

Strict Monotonicity of Image Operation for Injective Functions

Informal description

If a function $f : \alpha \to \beta$ is injective, then the image operation $f$ is strictly monotone with respect to the subset relation. That is, for any subsets $s, t \subseteq \alpha$ with $s \subsetneq t$, we have $f(s) \subsetneq f(t)$.

Function.Surjective.preimage_subset_preimage_iff theorem

{s t : Set β} (hf : Surjective f) : f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t

Full source

theorem Surjective.preimage_subset_preimage_iff {s t : Set β} (hf : Surjective f) :
    f ⁻¹' sf ⁻¹' s ⊆ f ⁻¹' tf ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t := by
  apply Set.preimage_subset_preimage_iff
  rw [hf.range_eq]
  apply subset_univ

Preimage Subset Relation under Surjective Function

Informal description

For a surjective function $f : \alpha \to \beta$ and subsets $s, t \subseteq \beta$, the preimage of $s$ under $f$ is contained in the preimage of $t$ under $f$ if and only if $s$ is contained in $t$, i.e., $$ f^{-1}(s) \subseteq f^{-1}(t) \leftrightarrow s \subseteq t. $$

Function.Surjective.range_comp theorem

{ι' : Sort*} {f : ι → ι'} (hf : Surjective f) (g : ι' → α) : range (g ∘ f) = range g

Full source

theorem Surjective.range_comp {ι' : Sort*} {f : ι → ι'} (hf : Surjective f) (g : ι' → α) :
    range (g ∘ f) = range g :=
  ext fun y => (@Surjective.exists _ _ _ hf fun x => g x = y).symm

Range Preservation under Composition with Surjective Function

Informal description

Let $f : \iota \to \iota'$ be a surjective function and $g : \iota' \to \alpha$ be any function. Then the range of the composition $g \circ f$ is equal to the range of $g$, i.e., $\text{range}(g \circ f) = \text{range}(g)$.

Function.Injective.mem_range_iff_existsUnique theorem

(hf : Injective f) {b : β} : b ∈ range f ↔ ∃! a, f a = b

Full source

theorem Injective.mem_range_iff_existsUnique (hf : Injective f) {b : β} :
    b ∈ range fb ∈ range f ↔ ∃! a, f a = b :=
  ⟨fun ⟨a, h⟩ => ⟨a, h, fun _ ha => hf (ha.trans h.symm)⟩, ExistsUnique.exists⟩

Injective Function Range Characterization via Unique Preimage

Informal description

For an injective function $f : \alpha \to \beta$ and an element $b \in \beta$, the following are equivalent: 1. $b$ is in the range of $f$, i.e., $b \in \text{range}(f)$. 2. There exists a unique $a \in \alpha$ such that $f(a) = b$.

Function.Injective.compl_image_eq theorem

(hf : Injective f) (s : Set α) : (f '' s)ᶜ = f '' sᶜ ∪ (range f)ᶜ

Full source

theorem Injective.compl_image_eq (hf : Injective f) (s : Set α) :
    (f '' s)ᶜ = f '' sᶜf '' sᶜ ∪ (range f)ᶜ := by
  ext y
  rcases em (y ∈ range f) with (⟨x, rfl⟩ | hx)
  · simp [hf.eq_iff]
  · rw [mem_range, not_exists] at hx
    simp [hx]

Complement of Image Equals Image of Complement Union Range Complement for Injective Functions

Informal description

Let $f : \alpha \to \beta$ be an injective function and $s \subseteq \alpha$ be a subset. Then the complement of the image of $s$ under $f$ is equal to the union of the image of the complement of $s$ under $f$ and the complement of the range of $f$. In symbols: $$(f(s))^c = f(s^c) \cup (\text{range}(f))^c.$$

Function.LeftInverse.image_image theorem

{g : β → α} (h : LeftInverse g f) (s : Set α) : g '' (f '' s) = s

Full source

theorem LeftInverse.image_image {g : β → α} (h : LeftInverse g f) (s : Set α) :
    g '' (f '' s) = s := by rw [← image_comp, h.comp_eq_id, image_id]

Left Inverse Property for Images: $g(f(s)) = s$

Informal description

Let $f \colon \alpha \to \beta$ and $g \colon \beta \to \alpha$ be functions such that $g$ is a left inverse of $f$ (i.e., $g(f(x)) = x$ for all $x \in \alpha$). Then for any subset $s \subseteq \alpha$, the image of the image of $s$ under $f$ under $g$ equals $s$, i.e., $g(f(s)) = s$.

Function.LeftInverse.preimage_preimage theorem

{g : β → α} (h : LeftInverse g f) (s : Set α) : f ⁻¹' (g ⁻¹' s) = s

Full source

theorem LeftInverse.preimage_preimage {g : β → α} (h : LeftInverse g f) (s : Set α) :
    f ⁻¹' (g ⁻¹' s) = s := by rw [← preimage_comp, h.comp_eq_id, preimage_id]

Preimage of Preimage Equals Original Set for Left Inverse Functions

Informal description

Let $f : \alpha \to \beta$ and $g : \beta \to \alpha$ be functions such that $g$ is a left inverse of $f$ (i.e., $g \circ f = \text{id}_\alpha$). Then for any subset $s \subseteq \alpha$, the preimage of $g^{-1}(s)$ under $f$ equals $s$, i.e., $f^{-1}(g^{-1}(s)) = s$.

Function.Involutive.preimage theorem

{f : α → α} (hf : Involutive f) : Involutive (preimage f)

Full source

protected theorem Involutive.preimage {f : α → α} (hf : Involutive f) : Involutive (preimage f) :=
  hf.rightInverse.preimage_preimage

Preimage Operation of an Involutive Function is Involutive

Informal description

For any involutive function $f \colon \alpha \to \alpha$, the preimage operation $f^{-1} \colon \mathcal{P}(\alpha) \to \mathcal{P}(\alpha)$ is also involutive, i.e., $f^{-1}(f^{-1}(s)) = s$ for any subset $s \subseteq \alpha$.

EquivLike.range_comp theorem

{α : Type*} (f : ι' → α) (e : E) : range (f ∘ e) = range f

Full source

@[simp] lemma range_comp {α : Type*} (f : ι' → α) (e : E) : range (f ∘ e) = range f :=
  (EquivLike.surjective _).range_comp _

Range Preservation under Composition with EquivLike Element: $\text{range}(f \circ e) = \text{range}(f)$

Informal description

For any function $f \colon \iota' \to \alpha$ and any element $e$ of type $E$ (where $E$ is an instance of `EquivLike`), the range of the composition $f \circ e$ is equal to the range of $f$, i.e., $\text{range}(f \circ e) = \text{range}(f)$.

Subtype.coe_image theorem

{p : α → Prop} {s : Set (Subtype p)} : (↑) '' s = {x | ∃ h : p x, (⟨x, h⟩ : Subtype p) ∈ s}

Full source

theorem coe_image {p : α → Prop} {s : Set (Subtype p)} :
    (↑) '' s = { x | ∃ h : p x, (⟨x, h⟩ : Subtype p) ∈ s } :=
  Set.ext fun a =>
    ⟨fun ⟨⟨_, ha'⟩, in_s, h_eq⟩ => h_eq ▸ ⟨ha', in_s⟩, fun ⟨ha, in_s⟩ => ⟨⟨a, ha⟩, in_s, rfl⟩⟩

Image of Subtype Under Canonical Inclusion Equals Set of Base Elements

Informal description

For a predicate $p : \alpha \to \text{Prop}$ and a set $s$ of elements of the subtype $\{x \mid p x\}$, the image of $s$ under the canonical inclusion map $\uparrow : \{x \mid p x\} \to \alpha$ is equal to the set $\{x \mid \exists h : p x, \langle x, h \rangle \in s\}$.

Subtype.coe_image_of_subset theorem

{s t : Set α} (h : t ⊆ s) : (↑) '' {x : ↥s | ↑x ∈ t} = t

Full source

@[simp]
theorem coe_image_of_subset {s t : Set α} (h : t ⊆ s) : (↑) '' { x : ↥s | ↑x ∈ t } = t := by
  ext x
  rw [mem_image]
  exact ⟨fun ⟨_, hx', hx⟩ => hx ▸ hx', fun hx => ⟨⟨x, h hx⟩, hx, rfl⟩⟩

Image of Subset under Canonical Inclusion Equals Subset

Informal description

For any subsets $s$ and $t$ of a type $\alpha$ such that $t \subseteq s$, the image of the set $\{x \in s \mid x \in t\}$ under the canonical inclusion map $\uparrow : s \to \alpha$ is equal to $t$.

Subtype.range_coe theorem

{s : Set α} : range ((↑) : s → α) = s

Full source

theorem range_coe {s : Set α} : range ((↑) : s → α) = s := by
  rw [← image_univ]
  simp [-image_univ, coe_image]

Range of Canonical Inclusion Equals Subset

Informal description

For any subset $s$ of a type $\alpha$, the range of the canonical inclusion map $\uparrow : s \to \alpha$ is equal to $s$ itself. In other words, $\text{range}(\uparrow) = s$.

Subtype.range_val theorem

{s : Set α} : range (Subtype.val : s → α) = s

Full source

/-- A variant of `range_coe`. Try to use `range_coe` if possible.
  This version is useful when defining a new type that is defined as the subtype of something.
  In that case, the coercion doesn't fire anymore. -/
theorem range_val {s : Set α} : range (Subtype.val : s → α) = s :=
  range_coe

Range of Subtype Projection Equals Subset

Informal description

For any subset $s$ of a type $\alpha$, the range of the canonical projection map $\text{val} : s \to \alpha$ (which extracts the underlying element from a term of the subtype) is equal to $s$ itself. In other words, $\text{range}(\text{val}) = s$.

Subtype.range_coe_subtype theorem

{p : α → Prop} : range ((↑) : Subtype p → α) = {x | p x}

Full source

/-- We make this the simp lemma instead of `range_coe`. The reason is that if we write
  for `s : Set α` the function `(↑) : s → α`, then the inferred implicit arguments of `(↑)` are
  `↑α (fun x ↦ x ∈ s)`. -/
@[simp]
theorem range_coe_subtype {p : α → Prop} : range ((↑) : Subtype p → α) = { x | p x } :=
  range_coe

Range of Subtype Inclusion Equals Predicate Set

Informal description

For any predicate $p : \alpha \to \text{Prop}$, the range of the canonical inclusion map $\uparrow : \{x \mid p x\} \to \alpha$ is equal to the set $\{x \mid p x\}$.

Subtype.coe_preimage_self theorem

(s : Set α) : ((↑) : s → α) ⁻¹' s = univ

Full source

@[simp]
theorem coe_preimage_self (s : Set α) : ((↑) : s → α) ⁻¹' s = univ := by
  rw [← preimage_range, range_coe]

Preimage of Subset under Canonical Inclusion is Universal Set

Informal description

For any subset $s$ of a type $\alpha$, the preimage of $s$ under the canonical inclusion map $\uparrow : s \to \alpha$ is equal to the universal set on $s$, i.e., $\uparrow^{-1}(s) = \mathrm{univ}$.

Subtype.range_val_subtype theorem

{p : α → Prop} : range (Subtype.val : Subtype p → α) = {x | p x}

Full source

theorem range_val_subtype {p : α → Prop} : range (Subtype.val : Subtype p → α) = { x | p x } :=
  range_coe

Range of Subtype Value Function Equals Predicate Set

Informal description

For any predicate $p : \alpha \to \text{Prop}$, the range of the value function $\text{Subtype.val} : \{x \mid p x\} \to \alpha$ is equal to the set $\{x \mid p x\}$.

Subtype.coe_image_subset theorem

(s : Set α) (t : Set s) : ((↑) : s → α) '' t ⊆ s

Full source

theorem coe_image_subset (s : Set α) (t : Set s) : ((↑) : s → α) '' t((↑) : s → α) '' t ⊆ s :=
  fun x ⟨y, _, yvaleq⟩ => by
  rw [← yvaleq]; exact y.property

Image of Subset under Inclusion is Contained in Original Set

Informal description

For any set $s \subseteq \alpha$ and any subset $t$ of $s$, the image of $t$ under the canonical inclusion map $\iota : s \to \alpha$ (where $\iota(x) = x$) is a subset of $s$.

Subtype.coe_image_univ theorem

(s : Set α) : ((↑) : s → α) '' Set.univ = s

Full source

theorem coe_image_univ (s : Set α) : ((↑) : s → α) '' Set.univ = s :=
  image_univ.trans range_coe

Image of Universal Set under Inclusion Equals Subset

Informal description

For any subset $s$ of a type $\alpha$, the image of the universal set under the canonical inclusion map $\iota : s \to \alpha$ (where $\iota(x) = x$) is equal to $s$ itself, i.e., $\iota(\text{univ}) = s$.

Subtype.image_preimage_coe theorem

(s t : Set α) : ((↑) : s → α) '' (((↑) : s → α) ⁻¹' t) = s ∩ t

Full source

@[simp]
theorem image_preimage_coe (s t : Set α) : ((↑) : s → α) '' (((↑) : s → α) ⁻¹' t) = s ∩ t :=
  image_preimage_eq_range_inter.trans <| congr_arg (· ∩ t) range_coe

Image of Preimage under Inclusion Equals Intersection: $\uparrow(\uparrow^{-1}(t)) = s \cap t$

Informal description

For any subsets $s, t \subseteq \alpha$, the image under the canonical inclusion map $\uparrow : s \to \alpha$ of the preimage of $t$ under $\uparrow$ equals the intersection of $s$ with $t$. That is, $\uparrow(\uparrow^{-1}(t)) = s \cap t$.

Subtype.image_preimage_val theorem

(s t : Set α) : (Subtype.val : s → α) '' (Subtype.val ⁻¹' t) = s ∩ t

Full source

theorem image_preimage_val (s t : Set α) : (Subtype.val : s → α) '' (Subtype.val ⁻¹' t) = s ∩ t :=
  image_preimage_coe s t

Image-Preimage Identity for Subtypes: $\text{val}(\text{val}^{-1}(t)) = s \cap t$

Informal description

For any subsets $s, t \subseteq \alpha$, the image under the canonical inclusion map $\text{val} : s \to \alpha$ of the preimage of $t$ under $\text{val}$ equals the intersection of $s$ with $t$. That is, $\text{val}(\text{val}^{-1}(t)) = s \cap t$.

Subtype.preimage_coe_eq_preimage_coe_iff theorem

{s t u : Set α} : ((↑) : s → α) ⁻¹' t = ((↑) : s → α) ⁻¹' u ↔ s ∩ t = s ∩ u

Full source

theorem preimage_coe_eq_preimage_coe_iff {s t u : Set α} :
    ((↑) : s → α) ⁻¹' t((↑) : s → α) ⁻¹' t = ((↑) : s → α) ⁻¹' u ↔ s ∩ t = s ∩ u := by
  rw [← image_preimage_coe, ← image_preimage_coe, coe_injective.image_injective.eq_iff]

Equality of Preimages under Inclusion is Equivalent to Equality of Intersections

Informal description

For any subsets $s, t, u \subseteq \alpha$, the preimages of $t$ and $u$ under the canonical inclusion map $\uparrow : s \to \alpha$ are equal if and only if the intersections $s \cap t$ and $s \cap u$ are equal. That is, $\uparrow^{-1}(t) = \uparrow^{-1}(u) \leftrightarrow s \cap t = s \cap u$.

Subtype.preimage_coe_self_inter theorem

(s t : Set α) : ((↑) : s → α) ⁻¹' (s ∩ t) = ((↑) : s → α) ⁻¹' t

Full source

theorem preimage_coe_self_inter (s t : Set α) :
    ((↑) : s → α) ⁻¹' (s ∩ t) = ((↑) : s → α) ⁻¹' t := by
  rw [preimage_coe_eq_preimage_coe_iff, ← inter_assoc, inter_self]

Preimage of Intersection with Subset Domain Equals Preimage

Informal description

For any subsets $s, t \subseteq \alpha$, the preimage of $s \cap t$ under the canonical inclusion map $\uparrow : s \to \alpha$ is equal to the preimage of $t$ under the same map. That is, $\uparrow^{-1}(s \cap t) = \uparrow^{-1}(t)$.

Subtype.preimage_coe_inter_self theorem

(s t : Set α) : ((↑) : s → α) ⁻¹' (t ∩ s) = ((↑) : s → α) ⁻¹' t

Full source

theorem preimage_coe_inter_self (s t : Set α) :
    ((↑) : s → α) ⁻¹' (t ∩ s) = ((↑) : s → α) ⁻¹' t := by
  rw [inter_comm, preimage_coe_self_inter]

Preimage of Intersection with Subset Domain Equals Preimage (Symmetric Version)

Informal description

For any subsets $s, t \subseteq \alpha$, the preimage of $t \cap s$ under the canonical inclusion map $\uparrow : s \to \alpha$ is equal to the preimage of $t$ under the same map. That is, $\uparrow^{-1}(t \cap s) = \uparrow^{-1}(t)$.

Subtype.preimage_val_eq_preimage_val_iff theorem

(s t u : Set α) : (Subtype.val : s → α) ⁻¹' t = Subtype.val ⁻¹' u ↔ s ∩ t = s ∩ u

Full source

theorem preimage_val_eq_preimage_val_iff (s t u : Set α) :
    (Subtype.val : s → α) ⁻¹' t(Subtype.val : s → α) ⁻¹' t = Subtype.val ⁻¹' u ↔ s ∩ t = s ∩ u :=
  preimage_coe_eq_preimage_coe_iff

Equality of Preimages under Inclusion is Equivalent to Equality of Intersections

Informal description

For any subsets $s, t, u$ of a type $\alpha$, the preimages of $t$ and $u$ under the canonical inclusion map $\text{val} : s \to \alpha$ are equal if and only if the intersections $s \cap t$ and $s \cap u$ are equal. In symbols: \[ \text{val}^{-1}(t) = \text{val}^{-1}(u) \leftrightarrow s \cap t = s \cap u. \]

Subtype.preimage_val_subset_preimage_val_iff theorem

(s t u : Set α) : (Subtype.val ⁻¹' t : Set s) ⊆ Subtype.val ⁻¹' u ↔ s ∩ t ⊆ s ∩ u

Full source

lemma preimage_val_subset_preimage_val_iff (s t u : Set α) :
    (Subtype.val ⁻¹' t : Set s) ⊆ Subtype.val ⁻¹' u(Subtype.val ⁻¹' t : Set s) ⊆ Subtype.val ⁻¹' u ↔ s ∩ t ⊆ s ∩ u := by
  constructor
  · rw [← image_preimage_coe, ← image_preimage_coe]
    exact image_subset _
  · intro h x a
    exact (h ⟨x.2, a⟩).2

Preimage Subset Condition via Intersection: $\text{val}^{-1}(t) \subseteq \text{val}^{-1}(u) \leftrightarrow s \cap t \subseteq s \cap u$

Informal description

For any subsets $s, t, u \subseteq \alpha$, the preimage of $t$ under the canonical inclusion map $\text{val} : s \to \alpha$ is a subset of the preimage of $u$ under $\text{val}$ if and only if the intersection of $s$ with $t$ is a subset of the intersection of $s$ with $u$. In symbols: \[ \text{val}^{-1}(t) \subseteq \text{val}^{-1}(u) \leftrightarrow s \cap t \subseteq s \cap u. \]

Subtype.exists_set_subtype theorem

{t : Set α} (p : Set α → Prop) : (∃ s : Set t, p (((↑) : t → α) '' s)) ↔ ∃ s : Set α, s ⊆ t ∧ p s

Full source

theorem exists_set_subtype {t : Set α} (p : Set α → Prop) :
    (∃ s : Set t, p (((↑) : t → α) '' s)) ↔ ∃ s : Set α, s ⊆ t ∧ p s := by
  rw [← exists_subset_range_and_iff, range_coe]

Existence of Subset in Subtype Image Satisfying Predicate iff Existence of Subset in Base Type Satisfying Predicate

Informal description

For any subset $t$ of a type $\alpha$ and any predicate $p$ on subsets of $\alpha$, there exists a subset $s$ of $t$ (viewed as a subtype) such that $p$ holds for the image of $s$ under the canonical inclusion map $\uparrow : t \to \alpha$ if and only if there exists a subset $s \subseteq \alpha$ with $s \subseteq t$ and $p(s)$.

Subtype.forall_set_subtype theorem

{t : Set α} (p : Set α → Prop) : (∀ s : Set t, p (((↑) : t → α) '' s)) ↔ ∀ s : Set α, s ⊆ t → p s

Full source

theorem forall_set_subtype {t : Set α} (p : Set α → Prop) :
    (∀ s : Set t, p (((↑) : t → α) '' s)) ↔ ∀ s : Set α, s ⊆ t → p s := by
  rw [← forall_subset_range_iff, range_coe]

Universal Quantification over Subsets of a Subtype vs. Subsets of the Original Type

Informal description

For any subset $t \subseteq \alpha$ and predicate $p$ on subsets of $\alpha$, the following are equivalent: 1. For every subset $s \subseteq t$ (viewed as a subtype), the predicate $p$ holds for the image of $s$ under the canonical inclusion map $\uparrow : t \to \alpha$. 2. For every subset $s \subseteq \alpha$ such that $s \subseteq t$, the predicate $p$ holds for $s$. In symbols: \[ \left(\forall s \subseteq t, p(\uparrow''s)\right) \leftrightarrow \left(\forall s \subseteq \alpha, s \subseteq t \to p(s)\right). \]

Subtype.preimage_coe_nonempty theorem

{s t : Set α} : (((↑) : s → α) ⁻¹' t).Nonempty ↔ (s ∩ t).Nonempty

Full source

theorem preimage_coe_nonempty {s t : Set α} :
    (((↑) : s → α) ⁻¹' t).Nonempty ↔ (s ∩ t).Nonempty := by
  rw [← image_preimage_coe, image_nonempty]

Nonempty Preimage Under Inclusion iff Nonempty Intersection

Informal description

For any subsets $s$ and $t$ of a type $\alpha$, the preimage of $t$ under the canonical inclusion map $\uparrow : s \to \alpha$ is nonempty if and only if the intersection $s \cap t$ is nonempty. In other words, $\uparrow^{-1}(t) \neq \emptyset \leftrightarrow s \cap t \neq \emptyset$.

Subtype.preimage_coe_eq_empty theorem

{s t : Set α} : ((↑) : s → α) ⁻¹' t = ∅ ↔ s ∩ t = ∅

Full source

theorem preimage_coe_eq_empty {s t : Set α} : ((↑) : s → α) ⁻¹' t((↑) : s → α) ⁻¹' t = ∅ ↔ s ∩ t = ∅ := by
  simp [← not_nonempty_iff_eq_empty, preimage_coe_nonempty]

Preimage of Set Under Inclusion is Empty iff Intersection is Empty

Informal description

For any sets $s$ and $t$ of type $\alpha$, the preimage of $t$ under the canonical inclusion map $\uparrow : s \to \alpha$ is empty if and only if the intersection of $s$ and $t$ is empty. In other words, $\uparrow^{-1}(t) = \emptyset \leftrightarrow s \cap t = \emptyset$.

Subtype.preimage_coe_compl theorem

(s : Set α) : ((↑) : s → α) ⁻¹' sᶜ = ∅

Full source

theorem preimage_coe_compl (s : Set α) : ((↑) : s → α) ⁻¹' sᶜ = ∅ :=
  preimage_coe_eq_empty.2 (inter_compl_self s)

Empty Preimage of Complement Under Inclusion

Informal description

For any set $s$ of type $\alpha$, the preimage of the complement $s^c$ under the canonical inclusion map $\uparrow : s \to \alpha$ is empty. In other words, $\uparrow^{-1}(s^c) = \emptyset$.

Subtype.preimage_coe_compl' theorem

(s : Set α) : (fun x : (sᶜ : Set α) => (x : α)) ⁻¹' s = ∅

Full source

@[simp]
theorem preimage_coe_compl' (s : Set α) :
    (fun x : (sᶜ : Set α) => (x : α)) ⁻¹' s = ∅ :=
  preimage_coe_eq_empty.2 (compl_inter_self s)

Preimage of Set Under Complement Inclusion is Empty

Informal description

For any set $s$ of type $\alpha$, the preimage of $s$ under the canonical inclusion map from the complement of $s$ to $\alpha$ is empty. In other words, if $f : s^c \to \alpha$ is defined by $f(x) = x$, then $f^{-1}(s) = \emptyset$.

Option.injective_iff theorem

{α β} {f : Option α → β} : Injective f ↔ Injective (f ∘ some) ∧ f none ∉ range (f ∘ some)

Full source

theorem injective_iff {α β} {f : Option α → β} :
    InjectiveInjective f ↔ Injective (f ∘ some) ∧ f none ∉ range (f ∘ some) := by
  simp only [mem_range, not_exists, (· ∘ ·)]
  refine
    ⟨fun hf => ⟨hf.comp (Option.some_injective _), fun x => hf.ne <| Option.some_ne_none _⟩, ?_⟩
  rintro ⟨h_some, h_none⟩ (_ | a) (_ | b) hab
  exacts [rfl, (h_none _ hab.symm).elim, (h_none _ hab).elim, congr_arg some (h_some hab)]

Characterization of Injectivity for Functions on Option Types

Informal description

A function $f \colon \operatorname{Option} \alpha \to \beta$ is injective if and only if the composition $f \circ \operatorname{some} \colon \alpha \to \beta$ is injective and the image of $\operatorname{none}$ under $f$ is not in the range of $f \circ \operatorname{some}$.

Option.range_eq theorem

{α β} (f : Option α → β) : range f = insert (f none) (range (f ∘ some))

Full source

theorem range_eq {α β} (f : Option α → β) : range f = insert (f none) (range (f ∘ some)) :=
  Set.ext fun _ => Option.exists.trans <| eq_comm.or Iff.rfl

Range Decomposition for Functions on Option Types: $\operatorname{range} f = \{f(\operatorname{none})\} \cup \operatorname{range} (f \circ \operatorname{some})$

Informal description

For any function $f \colon \operatorname{Option} \alpha \to \beta$, the range of $f$ is equal to the union of $\{f(\operatorname{none})\}$ and the range of $f \circ \operatorname{some}$.

Set.image_surjective theorem

: Surjective (image f) ↔ Surjective f

Full source

@[simp]
theorem image_surjective : SurjectiveSurjective (image f) ↔ Surjective f := by
  refine ⟨fun h y => ?_, Surjective.image_surjective⟩
  rcases h {y} with ⟨s, hs⟩
  have := mem_singleton y; rw [← hs] at this; rcases this with ⟨x, _, hx⟩
  exact ⟨x, hx⟩

Surjectivity of Image Function is Equivalent to Surjectivity of Original Function

Informal description

The image function $f '' \colon \mathcal{P}(\alpha) \to \mathcal{P}(\beta)$ is surjective if and only if the original function $f \colon \alpha \to \beta$ is surjective, where $\mathcal{P}(\alpha)$ denotes the power set of $\alpha$.

Set.image_injective theorem

: Injective (image f) ↔ Injective f

Full source

@[simp]
theorem image_injective : InjectiveInjective (image f) ↔ Injective f := by
  refine ⟨fun h x x' hx => ?_, Injective.image_injective⟩
  rw [← singleton_eq_singleton_iff]; apply h
  rw [image_singleton, image_singleton, hx]

Injectivity of $f$ is Equivalent to Injectivity of its Image Function

Informal description

A function $f : \alpha \to \beta$ is injective if and only if the induced image function $f '' : \mathcal{P}(\alpha) \to \mathcal{P}(\beta)$ is injective, where $\mathcal{P}(\alpha)$ denotes the power set of $\alpha$.

Set.preimage_eq_iff_eq_image theorem

{f : α → β} (hf : Bijective f) {s t} : f ⁻¹' s = t ↔ s = f '' t

Full source

theorem preimage_eq_iff_eq_image {f : α → β} (hf : Bijective f) {s t} :
    f ⁻¹' sf ⁻¹' s = t ↔ s = f '' t := by rw [← image_eq_image hf.1, hf.2.image_preimage]

Preimage-Image Equivalence for Bijective Functions: $f^{-1}(s) = t \leftrightarrow s = f(t)$

Informal description

For a bijective function $f \colon \alpha \to \beta$ and subsets $s \subseteq \beta$, $t \subseteq \alpha$, the preimage $f^{-1}(s)$ equals $t$ if and only if $s$ equals the image $f(t)$.

Disjoint.preimage theorem

(f : α → β) {s t : Set β} (h : Disjoint s t) : Disjoint (f ⁻¹' s) (f ⁻¹' t)

Full source

theorem Disjoint.preimage (f : α → β) {s t : Set β} (h : Disjoint s t) :
    Disjoint (f ⁻¹' s) (f ⁻¹' t) :=
  disjoint_iff_inf_le.mpr fun _ hx => h.le_bot hx

Preimage Preserves Disjointness

Informal description

For any function $f : \alpha \to \beta$ and disjoint sets $s, t \subseteq \beta$, the preimages $f^{-1}(s)$ and $f^{-1}(t)$ are also disjoint.

Codisjoint.preimage theorem

(f : α → β) {s t : Set β} (h : Codisjoint s t) : Codisjoint (f ⁻¹' s) (f ⁻¹' t)

Full source

lemma Codisjoint.preimage (f : α → β) {s t : Set β} (h : Codisjoint s t) :
    Codisjoint (f ⁻¹' s) (f ⁻¹' t) := by
  simp only [codisjoint_iff_le_sup, Set.sup_eq_union, top_le_iff, ← Set.preimage_union] at h ⊢
  rw [h]; rfl

Preimage Preserves Codisjointness

Informal description

For any function $f : \alpha \to \beta$ and subsets $s, t \subseteq \beta$, if $s$ and $t$ are codisjoint (i.e., $s \cup t = \beta$), then their preimages $f^{-1}(s)$ and $f^{-1}(t)$ under $f$ are also codisjoint (i.e., $f^{-1}(s) \cup f^{-1}(t) = \alpha$).

IsCompl.preimage theorem

(f : α → β) {s t : Set β} (h : IsCompl s t) : IsCompl (f ⁻¹' s) (f ⁻¹' t)

Full source

lemma IsCompl.preimage (f : α → β) {s t : Set β} (h : IsCompl s t) :
    IsCompl (f ⁻¹' s) (f ⁻¹' t) :=
  ⟨h.1.preimage f, h.2.preimage f⟩

Preimage Preserves Complementedness

Informal description

For any function $f : \alpha \to \beta$ and subsets $s, t \subseteq \beta$ that are complements (i.e., $s \cap t = \emptyset$ and $s \cup t = \beta$), their preimages $f^{-1}(s)$ and $f^{-1}(t)$ under $f$ are also complements in $\alpha$ (i.e., $f^{-1}(s) \cap f^{-1}(t) = \emptyset$ and $f^{-1}(s) \cup f^{-1}(t) = \alpha$).

Set.disjoint_image_image theorem

 {f : β → α} {g : γ → α} {s : Set β} {t : Set γ} (h : ∀ b ∈ s, ∀ c ∈ t, f b ≠ g c) : Disjoint (f '' s) (g '' t)

Full source

theorem disjoint_image_image {f : β → α} {g : γ → α} {s : Set β} {t : Set γ}
    (h : ∀ b ∈ s, ∀ c ∈ t, f b ≠ g c) : Disjoint (f '' s) (g '' t) :=
  disjoint_iff_inf_le.mpr <| by rintro a ⟨⟨b, hb, eq⟩, c, hc, rfl⟩; exact h b hb c hc eq

Disjointness of Images under Distinct Mappings

Informal description

For any functions $f : \beta \to \alpha$ and $g : \gamma \to \alpha$, and any subsets $s \subseteq \beta$ and $t \subseteq \gamma$, if for all $b \in s$ and $c \in t$ we have $f(b) \neq g(c)$, then the images $f(s)$ and $g(t)$ are disjoint subsets of $\alpha$.

Set.disjoint_image_of_injective theorem

(hf : Injective f) {s t : Set α} (hd : Disjoint s t) : Disjoint (f '' s) (f '' t)

Full source

theorem disjoint_image_of_injective (hf : Injective f) {s t : Set α} (hd : Disjoint s t) :
    Disjoint (f '' s) (f '' t) :=
  disjoint_image_image fun _ hx _ hy => hf.ne fun H => Set.disjoint_iff.1 hd ⟨hx, H.symm ▸ hy⟩

Injective Functions Preserve Disjointness of Images

Informal description

For any injective function $f : \alpha \to \beta$ and any disjoint subsets $s, t \subseteq \alpha$, the images $f(s)$ and $f(t)$ are also disjoint subsets of $\beta$.

Disjoint.of_image theorem

(h : Disjoint (f '' s) (f '' t)) : Disjoint s t

Full source

theorem _root_.Disjoint.of_image (h : Disjoint (f '' s) (f '' t)) : Disjoint s t :=
  disjoint_iff_inf_le.mpr fun _ hx =>
    disjoint_left.1 h (mem_image_of_mem _ hx.1) (mem_image_of_mem _ hx.2)

Disjointness of Preimages from Disjoint Images

Informal description

For any function $f : \alpha \to \beta$ and sets $s, t \subseteq \alpha$, if the images $f(s)$ and $f(t)$ are disjoint, then $s$ and $t$ are disjoint.

Set.disjoint_image_iff theorem

(hf : Injective f) : Disjoint (f '' s) (f '' t) ↔ Disjoint s t

Full source

@[simp]
theorem disjoint_image_iff (hf : Injective f) : DisjointDisjoint (f '' s) (f '' t) ↔ Disjoint s t :=
  ⟨Disjoint.of_image, disjoint_image_of_injective hf⟩

Disjointness of Images under Injective Function is Equivalent to Disjointness of Preimages

Informal description

For any injective function $f : \alpha \to \beta$ and subsets $s, t \subseteq \alpha$, the images $f(s)$ and $f(t)$ are disjoint if and only if $s$ and $t$ are disjoint. In other words, $f(s) \cap f(t) = \emptyset \leftrightarrow s \cap t = \emptyset$.

Disjoint.of_preimage theorem

(hf : Surjective f) {s t : Set β} (h : Disjoint (f ⁻¹' s) (f ⁻¹' t)) : Disjoint s t

Full source

theorem _root_.Disjoint.of_preimage (hf : Surjective f) {s t : Set β}
    (h : Disjoint (f ⁻¹' s) (f ⁻¹' t)) : Disjoint s t := by
  rw [disjoint_iff_inter_eq_empty, ← image_preimage_eq (_ ∩ _) hf, preimage_inter, h.inter_eq,
    image_empty]

Disjointness of Sets via Disjoint Preimages under Surjective Function

Informal description

For any surjective function $f \colon \alpha \to \beta$ and any subsets $s, t \subseteq \beta$, if the preimages $f^{-1}(s)$ and $f^{-1}(t)$ are disjoint, then $s$ and $t$ are disjoint. In other words, if $f^{-1}(s) \cap f^{-1}(t) = \emptyset$, then $s \cap t = \emptyset$.

Set.disjoint_preimage_iff theorem

(hf : Surjective f) {s t : Set β} : Disjoint (f ⁻¹' s) (f ⁻¹' t) ↔ Disjoint s t

Full source

@[simp]
theorem disjoint_preimage_iff (hf : Surjective f) {s t : Set β} :
    DisjointDisjoint (f ⁻¹' s) (f ⁻¹' t) ↔ Disjoint s t :=
  ⟨Disjoint.of_preimage hf, Disjoint.preimage _⟩

Disjointness of Preimages under Surjective Function is Equivalent to Disjointness of Sets

Informal description

For a surjective function $f \colon \alpha \to \beta$ and subsets $s, t \subseteq \beta$, the preimages $f^{-1}(s)$ and $f^{-1}(t)$ are disjoint if and only if $s$ and $t$ are disjoint. In other words: $$ f^{-1}(s) \cap f^{-1}(t) = \emptyset \iff s \cap t = \emptyset $$

Set.preimage_eq_empty theorem

{s : Set β} (h : Disjoint s (range f)) : f ⁻¹' s = ∅

Full source

theorem preimage_eq_empty {s : Set β} (h : Disjoint s (range f)) :
    f ⁻¹' s = ∅ := by
  simpa using h.preimage f

Preimage of Disjoint Set is Empty

Informal description

For any set $s \subseteq \beta$ that is disjoint from the range of a function $f : \alpha \to \beta$, the preimage $f^{-1}(s)$ is the empty set.

Set.preimage_eq_empty_iff theorem

{s : Set β} : f ⁻¹' s = ∅ ↔ Disjoint s (range f)

Full source

theorem preimage_eq_empty_iff {s : Set β} : f ⁻¹' sf ⁻¹' s = ∅ ↔ Disjoint s (range f) :=
  ⟨fun h => by
    simp only [eq_empty_iff_forall_not_mem, disjoint_iff_inter_eq_empty, not_exists, mem_inter_iff,
      not_and, mem_range, mem_preimage] at h ⊢
    intro y hy x hx
    rw [← hx] at hy
    exact h x hy,
  preimage_eq_empty⟩

Empty Preimage Characterization via Range Disjointness

Informal description

For any set $s \subseteq \beta$, the preimage $f^{-1}(s)$ is empty if and only if $s$ is disjoint from the range of $f$. In other words: $$ f^{-1}(s) = \emptyset \iff s \cap \mathrm{range}(f) = \emptyset $$

sigma_mk_preimage_image' theorem

(h : i ≠ j) : Sigma.mk j ⁻¹' (Sigma.mk i '' s) = ∅

Full source

lemma sigma_mk_preimage_image' (h : i ≠ j) : Sigma.mkSigma.mk j ⁻¹' (Sigma.mk i '' s) = ∅ := by
  simp [image, h]

Preimage of Sigma Injection Image is Empty for Distinct Indices

Informal description

For any distinct indices $i \neq j$ and any set $s$, the preimage of the image of $s$ under the map $\Sigma.mk\ i$ (the injection into the $\Sigma$-type at index $i$) under the map $\Sigma.mk\ j$ is the empty set. In other words, $(\Sigma.mk\ j)^{-1}(\Sigma.mk\ i(s)) = \emptyset$.

sigma_mk_preimage_image_eq_self theorem

: Sigma.mk i ⁻¹' (Sigma.mk i '' s) = s

Full source

lemma sigma_mk_preimage_image_eq_self : Sigma.mkSigma.mk i ⁻¹' (Sigma.mk i '' s) = s := by
  simp [image]

Preimage of Sigma Injection Image is Original Set

Informal description

For any set $s$ and index $i$, the preimage of the image of $s$ under the injection map $\Sigma.mk\ i$ (the map sending $x$ to $(i, x)$) is equal to $s$ itself. In other words, $(\Sigma.mk\ i)^{-1}(\Sigma.mk\ i(s)) = s$.

Mathlib.Data.Set.Image

Main definitions

Notation

Tags