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

theorem Set.preimage_val_eq_univ_of_subset {α : Type u_2} {A B : Set α} (h : A ⊆ B) : Subtype.val ⁻¹' B = univ

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}

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

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}

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)

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.

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

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

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

@[simp]

theorem Set.image_val_compl {α : Type u_2} {A : Set α} {D : Set ↑A} : Subtype.val '' Dᶜ = A \ Subtype.val '' D

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

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

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

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

@[simp]

theorem Set.image_val_union_self_right_eq {α : Type u_2} {A : Set α} {D : Set ↑A} : A ∪ Subtype.val '' D = A

@[simp]

theorem Set.image_val_union_self_left_eq {α : Type u_2} {A : Set α} {D : Set ↑A} : Subtype.val '' D ∪ A = A

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

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

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

@[simp]

theorem Set.image_val_inj {α : Type u_2} {A : Set α} {D E : Set ↑A} : Subtype.val '' D = Subtype.val '' E ↔ D = E

theorem Set.image_val_injective {α : Type u_2} {A : Set α} : Function.Injective (image Subtype.val)

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

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.

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

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