Documentation

Mathlib.Data.Set.Subset

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.

This notation, (together with the ↑ notation for Set.CoeHead in Mathlib.Data.Set.Functor) 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
def Set.Notation.«term_↓∩_».delab :
Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Set.Notation.«term_↓∩_» :
    Lean.TrailingParserDescr

    Given two sets A and B, A ↓∩ B denotes the intersection of A and B as a set in Set A.

    The notation is short for ((↑) ⁻¹' B : Set A), while giving hints to the elaborator that both A and B are terms of Set α for the same α. This set is the same as {x : ↑A | ↑x ∈ B}.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Set.preimage_val_eq_univ_of_subset {α : Type u_2} {A : Set α} {B : Set α} (h : A ⊆ B) :
      Subtype.val ⁻¹' B = Set.univ
      source
      theorem Set.preimage_val_sUnion {α : Type u_2} {A : Set α} {S : Set (Set α)} :
      Subtype.val ⁻¹' S.sUnion = {x : Set ↑A | ∃ B ∈ S, Subtype.val ⁻¹' B = x}.sUnion
      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.sInter = {x : Set ↑A | ∃ B ∈ S, Subtype.val ⁻¹' B = x}.sInter
      source
      theorem Set.preimage_val_sInter_eq_sInter {α : Type u_2} {A : Set α} {S : Set (Set α)} :
      Subtype.val ⁻¹' S.sInter = ((fun (x : Set α) => Subtype.val ⁻¹' x) '' S).sInter
      source
      theorem Set.eq_of_preimage_val_eq_of_subset {α : Type u_2} {A : Set α} {B : Set α} {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 : Set ↑A} {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 : Set ↑A} {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 : Set ↑A} {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.sUnion = {x : Set α | ∃ B ∈ T, Subtype.val '' B = x}.sUnion
      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.sInter = {x : Set α | ∃ B ∈ T, Subtype.val '' B = x}.sInter
      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.cou_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 : Set ↑A} {E : Set ↑A} :
      D ⊆ Subtype.val ⁻¹' (Subtype.val '' E) ↔ D ⊆ E
      source
      @[simp]
      theorem Set.image_val_inj {α : Type u_2} {A : Set α} {D : Set ↑A} {E : Set ↑A} :
      Subtype.val '' D = Subtype.val '' E ↔ D = E
      source
      theorem Set.image_val_injective {α : Type u_2} {A : Set α} :
      Function.Injective (Set.image Subtype.val)
      source
      theorem Set.subset_of_image_val_subset_image_val {α : Type u_2} {A : Set α} {D : Set ↑A} {E : Set ↑A} (h : Subtype.val '' D ⊆ Subtype.val '' E) :
      D ⊆ E
      source
      theorem Set.image_val_mono {α : Type u_2} {A : Set α} {D : Set ↑A} {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 : Set α} {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