# 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.lean` 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

source
theorem Set.preimage_val_eq_univ_of_subset {α : Type u_2} {A B : Set α} (h : A ⊆ B) :
Subtype.val ⁻¹' B = univ
source
theorem Set.preimage_val_sUnion {α : Type u_2} {A : Set α} {S : Set (Set α)} :
Subtype.val ⁻¹' ⋃₀ S = ⋃₀ {x : Set ↑A | ∃ B ∈ S, Subtype.val ⁻¹' B = x}
source
@[simp]
theorem Set.preimage_val_iInter {ι : Sort u_1} {α : Type u_2} {A : Set α} {s : ι → Set α} :
Subtype.val ⁻¹' ⋂ (i : ι), s i = ⋂ (i : ι), Subtype.val ⁻¹' s i
source
theorem Set.preimage_val_sInter {α : Type u_2} {A : Set α} {S : Set (Set α)} :
Subtype.val ⁻¹' ⋂₀ S = ⋂₀ {x : Set ↑A | ∃ B ∈ S, Subtype.val ⁻¹' B = x}
source
theorem Set.preimage_val_sInter_eq_sInter {α : Type u_2} {A : Set α} {S : Set (Set α)} :
Subtype.val ⁻¹' ⋂₀ S = ⋂₀ ((fun (x : Set α) => Subtype.val ⁻¹' x) '' S)
source
theorem Set.eq_of_preimage_val_eq_of_subset {α : Type u_2} {A B C : Set α} (hB : B ⊆ A) (hC : C ⊆ A) (h : Subtype.val ⁻¹' B = Subtype.val ⁻¹' C) :
B = C

The following simp lemmas try to transform operations in the subtype into operations in the ambient type, if possible.

source
@[simp]
theorem Set.image_val_union {α : Type u_2} {A : Set α} {D E : Set ↑A} :
Subtype.val '' (D ∪ E) = Subtype.val '' D ∪ Subtype.val '' E
source
@[simp]
theorem Set.image_val_inter {α : Type u_2} {A : Set α} {D E : Set ↑A} :
Subtype.val '' (D ∩ E) = Subtype.val '' D ∩ Subtype.val '' E
source
@[simp]
theorem Set.image_val_diff {α : Type u_2} {A : Set α} {D E : Set ↑A} :
Subtype.val '' (D \ E) = Subtype.val '' D \ Subtype.val '' E
source
@[simp]
theorem Set.image_val_compl {α : Type u_2} {A : Set α} {D : Set ↑A} :
Subtype.val '' D ᶜ = A \ Subtype.val '' D
source
@[simp]
theorem Set.image_val_sUnion {α : Type u_2} {A : Set α} {T : Set (Set ↑A)} :
Subtype.val '' ⋃₀ T = ⋃₀ {x : Set α | ∃ B ∈ T, Subtype.val '' B = x}
source
@[simp]
theorem Set.image_val_iUnion {ι : Sort u_1} {α : Type u_2} {A : Set α} {t : ι → Set ↑A} :
Subtype.val '' ⋃ (i : ι), t i = ⋃ (i : ι), Subtype.val '' t i
source
@[simp]
theorem Set.image_val_sInter {α : Type u_2} {A : Set α} {T : Set (Set ↑A)} (hT : T.Nonempty) :
Subtype.val '' ⋂₀ T = ⋂₀ {x : Set α | ∃ B ∈ T, Subtype.val '' B = x}
source
@[simp]
theorem Set.image_val_iInter {ι : Sort u_1} {α : Type u_2} {A : Set α} {t : ι → Set ↑A} [Nonempty ι] :
Subtype.val '' ⋂ (i : ι), t i = ⋂ (i : ι), Subtype.val '' t i
source
@[simp]
theorem Set.image_val_union_self_right_eq {α : Type u_2} {A : Set α} {D : Set ↑A} :
A ∪ Subtype.val '' D = A
source
@[simp]
theorem Set.image_val_union_self_left_eq {α : Type u_2} {A : Set α} {D : Set ↑A} :
Subtype.val '' D ∪ A = A
source
@[simp]
theorem Set.image_val_inter_self_right_eq_coe {α : Type u_2} {A : Set α} {D : Set ↑A} :
A ∩ Subtype.val '' D = Subtype.val '' D
source
@[simp]
theorem Set.image_val_inter_self_left_eq_coe {α : Type u_2} {A : Set α} {D : Set ↑A} :
Subtype.val '' D ∩ A = Subtype.val '' D
source
theorem Set.subset_preimage_val_image_val_iff {α : Type u_2} {A : Set α} {D E : Set ↑A} :
D ⊆ Subtype.val ⁻¹' (Subtype.val '' E) ↔ D ⊆ E
source
@[simp]
theorem Set.image_val_inj {α : Type u_2} {A : Set α} {D E : Set ↑A} :
Subtype.val '' D = Subtype.val '' E ↔ D = E
source
theorem Set.image_val_injective {α : Type u_2} {A : Set α} :
Function.Injective (image Subtype.val)
source
theorem Set.subset_of_image_val_subset_image_val {α : Type u_2} {A : Set α} {D E : Set ↑A} (h : Subtype.val '' D ⊆ Subtype.val '' E) :
D ⊆ E
source
theorem Set.image_val_mono {α : Type u_2} {A : Set α} {D E : Set ↑A} (h : D ⊆ E) :
Subtype.val '' D ⊆ Subtype.val '' E

Relations between restriction and coercion.

source
theorem Set.image_val_preimage_val_subset_self {α : Type u_2} {A B : Set α} :
Subtype.val '' (Subtype.val ⁻¹' B) ⊆ B
source
theorem Set.preimage_val_image_val_eq_self {α : Type u_2} {A : Set α} {D : Set ↑A} :
Subtype.val ⁻¹' (Subtype.val '' D) = D