Mathlib.Data.Set.Subset

Module docstring

{"# Sets in subtypes

This file is about sets in Set A when A is a set.

It defines notation ↓∩ for sets in a type pulled down to sets in a subtype, as an inverse operation to the coercion that lifts sets in a subtype up to sets in the ambient type.

This module also provides lemmas for ↓∩ and this coercion.

Notation

Let α be a Type, A B : Set α two sets in α, and C : Set A a set in the subtype ↑A.

A ↓∩ B denotes (Subtype.val ⁻¹' B : Set A) (that is, {x : ↑A | ↑x ∈ B}).
↑C denotes Subtype.val '' C (that is, {x : α | ∃ y ∈ C, ↑y = x}).

This notation, (together with the ↑ notation for Set.CoeHead) is defined in Mathlib.Data.Set.Notation and is scoped to the Set.Notation namespace. To enable it, use open Set.Notation.

Naming conventions

Theorem names refer to ↓∩ as preimage_val.

Tags

subsets ","The following simp lemmas try to transform operations in the subtype into operations in the ambient type, if possible. ","Relations between restriction and coercion. "}

Set.preimage_val_eq_univ_of_subset theorem

(h : A ⊆ B) : A ↓∩ B = univ

Full source

lemma preimage_val_eq_univ_of_subset (h : A ⊆ B) : A ↓∩ B = univ := by
  rw [eq_univ_iff_forall, Subtype.forall]
  exact h

Preimage of Superset is Universal Set in Subtype

Informal description

For any sets $A$ and $B$ in a type $\alpha$, if $A$ is a subset of $B$, then the preimage of $B$ under the inclusion map from $A$ to $\alpha$ is equal to the universal set on $A$, i.e., $\{x \in A \mid x \in B\} = \text{univ}$.

Set.preimage_val_sUnion theorem

: A ↓∩ (⋃₀ S) = ⋃₀ {(A ↓∩ B) | B ∈ S}

Full source

lemma preimage_val_sUnion : A ↓∩ (⋃₀ S) = ⋃₀ { (A ↓∩ B) | B ∈ S } := by
  rw [← Set.image, sUnion_image]
  simp_rw [sUnion_eq_biUnion, preimage_iUnion]

Preimage of Union Equals Union of Preimages in Subtype

Informal description

For a set $A \subseteq \alpha$ and a family of sets $S \subseteq \mathcal{P}(\alpha)$, the preimage under the inclusion map of the union $\bigcup₀ S$ equals the union of the preimages: \[ \{x \in A \mid x \in \bigcup₀ S\} = \bigcup_{B \in S} \{x \in A \mid x \in B\}. \]

Set.preimage_val_iInter theorem

: A ↓∩ (⋂ i, s i) = ⋂ i, A ↓∩ s i

Full source

@[simp]
lemma preimage_val_iInter : A ↓∩ (⋂ i, s i) = ⋂ i, A ↓∩ s i := preimage_iInter

Preimage of Indexed Intersection Equals Indexed Intersection of Preimages in Subtype

Informal description

For a set $A \subseteq \alpha$ and an indexed family of sets $\{s_i\}_{i \in \iota}$ in $\alpha$, the preimage under the inclusion map of the intersection $\bigcap_i s_i$ equals the intersection of the preimages: \[ \{x \in A \mid x \in \bigcap_i s_i\} = \bigcap_i \{x \in A \mid x \in s_i\}. \]

Set.preimage_val_sInter theorem

: A ↓∩ (⋂₀ S) = ⋂₀ {(A ↓∩ B) | B ∈ S}

Full source

lemma preimage_val_sInter : A ↓∩ (⋂₀ S) = ⋂₀ { (A ↓∩ B) | B ∈ S } := by
  rw [← Set.image, sInter_image]
  simp_rw [sInter_eq_biInter, preimage_iInter]

Preimage of Set Intersection Equals Intersection of Preimages in Subtype

Informal description

For a set $A \subseteq \alpha$ and a collection of sets $S \subseteq \mathcal{P}(\alpha)$, the preimage under the inclusion map of the intersection $\bigcap₀ S$ equals the intersection of the preimages: \[ \{x \in A \mid x \in \bigcap₀ S\} = \bigcap_{B \in S} \{x \in A \mid x \in B\}. \]

Set.preimage_val_sInter_eq_sInter theorem

: A ↓∩ (⋂₀ S) = ⋂₀ ((A ↓∩ ·) '' S)

Full source

lemma preimage_val_sInter_eq_sInter : A ↓∩ (⋂₀ S) = ⋂₀ ((A ↓∩ ·) '' S) := by
  simp only [preimage_sInter, sInter_image]

Preimage of Intersection Equals Intersection of Preimages in Subtype

Informal description

For a set $A \subseteq \alpha$ and a collection of sets $S \subseteq \mathcal{P}(\alpha)$, the preimage under the inclusion map of the intersection $\bigcap_{B \in S} B$ equals the intersection of the images of the preimages: \[ \{x \in A \mid x \in \bigcap_{B \in S} B\} = \bigcap_{B \in S} \{x \in A \mid x \in B\}. \]

Set.image_val_union theorem

: (↑(D ∪ E) : Set α) = ↑D ∪ ↑E

Full source

@[simp]
lemma image_val_union : (↑(D ∪ E) : Set α) = ↑D ∪ ↑E := image_union _ _ _

Image of Union under Inclusion Equals Union of Images

Informal description

For any sets $D, E \subseteq A$ in the subtype corresponding to a set $A \subseteq \alpha$, the image under the inclusion map of their union equals the union of their images: \[ \text{val}(D \cup E) = \text{val}(D) \cup \text{val}(E), \] where $\text{val} : A \to \alpha$ is the inclusion map.

Set.image_val_inter theorem

: (↑(D ∩ E) : Set α) = ↑D ∩ ↑E

Full source

@[simp]
lemma image_val_inter : (↑(D ∩ E) : Set α) = ↑D ∩ ↑E := image_inter Subtype.val_injective

Image of Intersection under Inclusion Equals Intersection of Images

Informal description

For any sets $D, E \subseteq A$ in the subtype corresponding to a set $A \subseteq \alpha$, the image under the inclusion map of their intersection equals the intersection of their images: \[ \text{val}(D \cap E) = \text{val}(D) \cap \text{val}(E), \] where $\text{val} : A \to \alpha$ is the inclusion map.

Set.image_val_diff theorem

: (↑(D \ E) : Set α) = ↑D \ ↑E

Full source

@[simp]
lemma image_val_diff : (↑(D \ E) : Set α) = ↑D \ ↑E := image_diff Subtype.val_injective _ _

Image of Set Difference under Inclusion Equals Difference of Images

Informal description

For any sets $D, E \subseteq A$ in the subtype corresponding to a set $A \subseteq \alpha$, the image under the inclusion map of their set difference equals the set difference of their images: \[ \text{val}(D \setminus E) = \text{val}(D) \setminus \text{val}(E), \] where $\text{val} : A \to \alpha$ is the inclusion map.

Set.image_val_compl theorem

: ↑(Dᶜ) = A \ ↑D

Full source

@[simp]
lemma image_val_compl : ↑(Dᶜ) = A \ ↑D := by
  rw [compl_eq_univ_diff, image_val_diff, image_univ, Subtype.range_coe_subtype, setOf_mem_eq]

Image of Complement in Subtype Equals Set Difference with Ambient Set

Informal description

For any set $D$ in the subtype corresponding to a set $A \subseteq \alpha$, the image under the inclusion map of the complement of $D$ equals the set difference between $A$ and the image of $D$: \[ \text{val}(D^c) = A \setminus \text{val}(D), \] where $\text{val} : A \to \alpha$ is the inclusion map.

Set.image_val_sUnion theorem

: ↑(⋃₀ T) = ⋃₀ {(B : Set α) | B ∈ T}

Full source

@[simp]
lemma image_val_sUnion : ↑(⋃₀ T) = ⋃₀ { (B : Set α) | B ∈ T} := by
  rw [image_sUnion, image]

Image of Union in Subtype Equals Union of Images

Informal description

For any family of sets $T$ in the subtype $\mathrm{Elem}\, A$, the image under the canonical embedding $\mathrm{val} : \mathrm{Elem}\, A \to \alpha$ of their union equals the union of their images in $\alpha$. In symbols: $$ \mathrm{val}\left(\bigcup_{B \in T} B\right) = \bigcup_{B \in T} \mathrm{val}(B). $$

Set.image_val_iUnion theorem

: ↑(⋃ i, t i) = ⋃ i, (t i : Set α)

Full source

@[simp]
lemma image_val_iUnion : ↑(⋃ i, t i) = ⋃ i, (t i : Set α) := image_iUnion

Image of Union in Subtype Equals Union of Images

Informal description

For any family of sets $\{t_i\}_{i \in \iota}$ in the subtype $\mathrm{Elem}\, A$, the image under the canonical embedding $\mathrm{val} : \mathrm{Elem}\, A \to \alpha$ of their union equals the union of their images in $\alpha$. In symbols: $$ \mathrm{val}\left(\bigcup_{i} t_i\right) = \bigcup_{i} \mathrm{val}(t_i). $$

Set.image_val_sInter theorem

(hT : T.Nonempty) : (↑(⋂₀ T) : Set α) = ⋂₀ {(↑B : Set α) | B ∈ T}

Full source

@[simp]
lemma image_val_sInter (hT : T.Nonempty) : (↑(⋂₀ T) : Set α) = ⋂₀ { (↑B : Set α) | B ∈ T } := by
  rw [← Set.image, sInter_image, sInter_eq_biInter, Subtype.val_injective.injOn.image_biInter_eq hT]

Image of Intersection in Subtype Equals Intersection of Images under Nonempty Condition

Informal description

Let $T$ be a nonempty family of sets in the subtype $\mathrm{Elem}\, A$ of a type $\alpha$. The image under the canonical embedding $\mathrm{val} : \mathrm{Elem}\, A \to \alpha$ of their intersection equals the intersection of their images in $\alpha$. In symbols: $$ \mathrm{val}\left(\bigcap_{B \in T} B\right) = \bigcap_{B \in T} \mathrm{val}(B). $$

Set.image_val_iInter theorem

[Nonempty ι] : (↑(⋂ i, t i) : Set α) = ⋂ i, (↑(t i) : Set α)

Full source

@[simp]
lemma image_val_iInter [Nonempty ι] : (↑(⋂ i, t i) : Set α) = ⋂ i, (↑(t i) : Set α) :=
  Subtype.val_injective.injOn.image_iInter_eq

Image of Intersection in Subtype Equals Intersection of Images

Informal description

Let $\{t_i\}_{i \in \iota}$ be a nonempty family of sets in the subtype $\mathrm{Elem}\, A$ (where $\iota$ is nonempty). The image under the canonical embedding $\mathrm{val} : \mathrm{Elem}\, A \to \alpha$ of their intersection equals the intersection of their images in $\alpha$. In symbols: $$ \mathrm{val}\left(\bigcap_{i} t_i\right) = \bigcap_{i} \mathrm{val}(t_i). $$

Set.image_val_union_self_right_eq theorem

: A ∪ ↑D = A

Full source

@[simp]
lemma image_val_union_self_right_eq : A ∪ ↑D = A :=
  union_eq_left.2 image_val_subset

Union with Subset Image Equals Original Set

Informal description

For any set $A$ in a type $\alpha$ and any subset $D$ of the subtype $\mathrm{Elem}\, A$, the union of $A$ with the image of $D$ under the canonical embedding $\mathrm{val} : \mathrm{Elem}\, A \to \alpha$ equals $A$. In symbols: $$ A \cup \mathrm{val}(D) = A. $$

Set.image_val_union_self_left_eq theorem

: ↑D ∪ A = A

Full source

@[simp]
lemma image_val_union_self_left_eq : ↑D ∪ A = A :=
  union_eq_right.2 image_val_subset

Union of Subset Image with Ambient Set Equals Ambient Set

Informal description

For any set $A$ in a type $\alpha$ and any subset $D$ of $A$, the union of the image of $D$ under the canonical embedding $\mathrm{val} : \mathrm{Elem}\, A \to \alpha$ with $A$ equals $A$. In symbols: $$ \mathrm{val}(D) \cup A = A. $$

Set.image_val_inter_self_right_eq_coe theorem

: A ∩ ↑D = ↑D

Full source

@[simp]
lemma image_val_inter_self_right_eq_coe : A ∩ ↑D = ↑D :=
  inter_eq_right.2 image_val_subset

Intersection with Coerced Subset Equals Coerced Subset

Informal description

For any set $A$ and any subset $D$ of $A$ (viewed as a set in the subtype $\mathrm{Elem}\, A$), the intersection of $A$ with the image of $D$ under the coercion map equals the image of $D$ under the coercion map. In other words, $A \cap \uparrow D = \uparrow D$.

Set.image_val_inter_self_left_eq_coe theorem

: ↑D ∩ A = ↑D

Full source

@[simp]
lemma image_val_inter_self_left_eq_coe : ↑D ∩ A = ↑D :=
  inter_eq_left.2 image_val_subset

Intersection of Coerced Subset with Ambient Set

Informal description

For any set $D$ in the subtype $\mathrm{Elem}\, A$ (where $A$ is a set in type $\alpha$), the intersection of the coerced set $\uparrow D$ with $A$ equals $\uparrow D$. In other words, $\uparrow D \cap A = \uparrow D$.

Set.subset_preimage_val_image_val_iff theorem

: D ⊆ A ↓∩ ↑E ↔ D ⊆ E

Full source

lemma subset_preimage_val_image_val_iff : D ⊆ A ↓∩ ↑ED ⊆ A ↓∩ ↑E ↔ D ⊆ E := by
  rw [preimage_image_eq _ Subtype.val_injective]

Subset Relation between Preimage and Image under Subtype Projection

Informal description

For sets $D \subseteq A$ and $E \subseteq \mathrm{Elem}\, A$, the following equivalence holds: $D$ is a subset of the preimage of $E$ under the projection map $\mathrm{val} : \mathrm{Elem}\, A \to \alpha$ if and only if $D$ is a subset of $E$.

Set.image_val_inj theorem

: (D : Set α) = ↑E ↔ D = E

Full source

@[simp]
lemma image_val_inj : (D : Set α) = ↑E ↔ D = E := Subtype.val_injective.image_injective.eq_iff

Injectivity of Subset Coercion: $\uparrow E = D \leftrightarrow E = D$

Informal description

For any sets $D \subseteq \alpha$ and $E \subseteq A$ (where $A$ is a subset of $\alpha$), the coerced set $\uparrow E$ equals $D$ if and only if $D$ equals $E$ as subsets of $A$.

Set.image_val_injective theorem

: Function.Injective ((↑) : Set A → Set α)

Full source

lemma image_val_injective : Function.Injective ((↑) : Set A → Set α) :=
  Subtype.val_injective.image_injective

Injectivity of Subtype Set Image under Projection

Informal description

The function that maps a set $D$ in the subtype $A$ to its image under the projection map $\mathrm{val} : A \to \alpha$ is injective. In other words, if $D, E \subseteq A$ are sets in the subtype and their images in $\alpha$ coincide (i.e., $\mathrm{val}'' D = \mathrm{val}'' E$), then $D = E$.

Set.subset_of_image_val_subset_image_val theorem

(h : (↑D : Set α) ⊆ ↑E) : D ⊆ E

Full source

lemma subset_of_image_val_subset_image_val (h : (↑D : Set α) ⊆ ↑E) : D ⊆ E :=
  (image_subset_image_iff Subtype.val_injective).1 h

Subset Relation Preservation under Subtype Inclusion: $\uparrow D \subseteq \uparrow E \implies D \subseteq E$

Informal description

For any type $\alpha$, subsets $A \subseteq \alpha$, and sets $D, E \subseteq A$, if the image of $D$ under the canonical inclusion map $\uparrow : A \to \alpha$ is contained in the image of $E$ under the same map, then $D$ is a subset of $E$. In symbols: $$ \uparrow D \subseteq \uparrow E \implies D \subseteq E $$

Set.image_val_mono theorem

(h : D ⊆ E) : (↑D : Set α) ⊆ ↑E

Full source

@[mono]
lemma image_val_mono (h : D ⊆ E) : (↑D : Set α) ⊆ ↑E :=
  (image_subset_image_iff Subtype.val_injective).2 h

Monotonicity of Subset Image under Inclusion

Informal description

For any subsets $D$ and $E$ of a set $A$ in a type $\alpha$, if $D \subseteq E$, then the image of $D$ under the canonical inclusion map $\uparrow : A \to \alpha$ is a subset of the image of $E$ under the same map. In symbols: $$ D \subseteq E \implies \uparrow D \subseteq \uparrow E $$

Set.image_val_preimage_val_subset_self theorem

: ↑(A ↓∩ B) ⊆ B

Full source

lemma image_val_preimage_val_subset_self : ↑(A ↓∩ B) ⊆ B :=
  image_preimage_subset _ _

Image of Preimage under Inclusion is Subset

Informal description

For any sets $A, B \subseteq \alpha$, the image under the inclusion map of the preimage of $B$ in the subtype $A$ is a subset of $B$, i.e., \[ \{\uparrow x \mid x \in A \text{ and } \uparrow x \in B\} \subseteq B. \]

Set.preimage_val_image_val_eq_self theorem

: A ↓∩ ↑D = D

Full source

lemma preimage_val_image_val_eq_self : A ↓∩ ↑D = D :=
  Function.Injective.preimage_image Subtype.val_injective _

Preimage-Image Identity for Subtype Inclusion: $A \downarrow\cap \uparrow D = D$

Informal description

For any set $A \subseteq \alpha$ and any set $D \subseteq A$ (where $A$ is viewed as a subtype), the preimage under the canonical inclusion map of the image of $D$ under this map equals $D$ itself. In symbols, this is expressed as $A \downarrow\cap \uparrow D = D$, where $\uparrow D$ denotes the image of $D$ under the inclusion map and $\downarrow\cap$ denotes the preimage operation.