Documentation

Mathlib.Logic.Equiv.Set

Equivalences and sets #

In this file we provide lemmas linking equivalences to sets.

Some notable definitions are:

This file is separate from Equiv/Basic such that we do not require the full lattice structure on sets before defining what an equivalence is.

@[simp]
theorem Equiv.range_eq_univ {α : Type u_1} {β : Type u_2} (e : α β) :
Set.range e = Set.univ
theorem Equiv.image_eq_preimage {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) :
e '' s = e.symm ⁻¹' s
@[simp]
theorem Set.mem_image_equiv {α : Type u_1} {β : Type u_2} {S : Set α} {f : α β} {x : β} :
x f '' S f.symm x S
theorem Set.image_equiv_eq_preimage_symm {α : Type u_1} {β : Type u_2} (S : Set α) (f : α β) :
f '' S = f.symm ⁻¹' S

Alias for Equiv.image_eq_preimage

theorem Set.preimage_equiv_eq_image_symm {α : Type u_1} {β : Type u_2} (S : Set α) (f : β α) :
f ⁻¹' S = f.symm '' S

Alias for Equiv.image_eq_preimage

@[simp]
theorem Equiv.subset_image {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) (t : Set β) :
e.symm '' t s t e '' s
@[simp]
theorem Equiv.subset_image' {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) (t : Set β) :
s e.symm '' t e '' s t
@[simp]
theorem Equiv.symm_image_image {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) :
e.symm '' (e '' s) = s
theorem Equiv.eq_image_iff_symm_image_eq {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) (t : Set β) :
t = e '' s e.symm '' t = s
@[simp]
theorem Equiv.image_symm_image {α : Type u_1} {β : Type u_2} (e : α β) (s : Set β) :
e '' (e.symm '' s) = s
@[simp]
theorem Equiv.image_preimage {α : Type u_1} {β : Type u_2} (e : α β) (s : Set β) :
e '' (e ⁻¹' s) = s
@[simp]
theorem Equiv.preimage_image {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) :
e ⁻¹' (e '' s) = s
theorem Equiv.image_compl {α : Type u_1} {β : Type u_2} (f : α β) (s : Set α) :
f '' s = (f '' s)
@[simp]
theorem Equiv.symm_preimage_preimage {α : Type u_1} {β : Type u_2} (e : α β) (s : Set β) :
e.symm ⁻¹' (e ⁻¹' s) = s
@[simp]
theorem Equiv.preimage_symm_preimage {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) :
e ⁻¹' (e.symm ⁻¹' s) = s
@[simp]
theorem Equiv.preimage_subset {α : Type u_1} {β : Type u_2} (e : α β) (s : Set β) (t : Set β) :
e ⁻¹' s e ⁻¹' t s t
theorem Equiv.image_subset {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) (t : Set α) :
e '' s e '' t s t
@[simp]
theorem Equiv.image_eq_iff_eq {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) (t : Set α) :
e '' s = e '' t s = t
theorem Equiv.preimage_eq_iff_eq_image {α : Type u_1} {β : Type u_2} (e : α β) (s : Set β) (t : Set α) :
e ⁻¹' s = t s = e '' t
theorem Equiv.eq_preimage_iff_image_eq {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) (t : Set β) :
s = e ⁻¹' t e '' s = t
@[simp]
theorem Equiv.prod_assoc_preimage {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {u : Set γ} :
↑(Equiv.prodAssoc α β γ) ⁻¹' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u
@[simp]
theorem Equiv.prod_assoc_symm_preimage {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {u : Set γ} :
(Equiv.prodAssoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u
theorem Equiv.prod_assoc_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {u : Set γ} :
↑(Equiv.prodAssoc α β γ) '' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u
theorem Equiv.prod_assoc_symm_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {u : Set γ} :
(Equiv.prodAssoc α β γ).symm '' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u
def Equiv.setProdEquivSigma {α : Type u_1} {β : Type u_2} (s : Set (α × β)) :
s (x : α) × {y | (x, y) s}

A set s in α × β is equivalent to the sigma-type Σ x, {y | (x, y) ∈ s}.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem Equiv.setCongr_apply {α : Type u_1} {s : Set α} {t : Set α} (h : s = t) (a : { a // (fun a => (fun x => x s) a) a }) :
    ↑(Equiv.setCongr h) a = { val := a, property := (_ : ↑(Equiv.refl α) a t) }
    def Equiv.setCongr {α : Type u_1} {s : Set α} {t : Set α} (h : s = t) :
    s t

    The subtypes corresponding to equal sets are equivalent.

    Equations
    Instances For
      @[simp]
      theorem Equiv.image_symm_apply_coe {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) (y : ↑(e '' s)) :
      ↑((Equiv.image e s).symm y) = e.symm y
      @[simp]
      theorem Equiv.image_apply_coe {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) (x : s) :
      ↑(↑(Equiv.image e s) x) = e x
      def Equiv.image {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) :
      s ↑(e '' s)

      A set is equivalent to its image under an equivalence.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def Equiv.Set.univ (α : Type u_1) :
        Set.univ α

        univ α is equivalent to α.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def Equiv.Set.empty (α : Type u_1) :

          An empty set is equivalent to the Empty type.

          Equations
          Instances For

            An empty set is equivalent to a PEmpty type.

            Equations
            Instances For
              def Equiv.Set.union' {α : Type u_1} {s : Set α} {t : Set α} (p : αProp) [DecidablePred p] (hs : (x : α) → x sp x) (ht : ∀ (x : α), x t¬p x) :
              ↑(s t) s t

              If sets s and t are separated by a decidable predicate, then s ∪ t is equivalent to s ⊕ t.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def Equiv.Set.union {α : Type u_1} {s : Set α} {t : Set α} [DecidablePred fun x => x s] (H : s t ) :
                ↑(s t) s t

                If sets s and t are disjoint, then s ∪ t is equivalent to s ⊕ t.

                Equations
                Instances For
                  theorem Equiv.Set.union_apply_left {α : Type u_1} {s : Set α} {t : Set α} [DecidablePred fun x => x s] (H : s t ) {a : ↑(s t)} (ha : a s) :
                  ↑(Equiv.Set.union H) a = Sum.inl { val := a, property := ha }
                  theorem Equiv.Set.union_apply_right {α : Type u_1} {s : Set α} {t : Set α} [DecidablePred fun x => x s] (H : s t ) {a : ↑(s t)} (ha : a t) :
                  ↑(Equiv.Set.union H) a = Sum.inr { val := a, property := ha }
                  @[simp]
                  theorem Equiv.Set.union_symm_apply_left {α : Type u_1} {s : Set α} {t : Set α} [DecidablePred fun x => x s] (H : s t ) (a : s) :
                  (Equiv.Set.union H).symm (Sum.inl a) = { val := a, property := (_ : a s t) }
                  @[simp]
                  theorem Equiv.Set.union_symm_apply_right {α : Type u_1} {s : Set α} {t : Set α} [DecidablePred fun x => x s] (H : s t ) (a : t) :
                  (Equiv.Set.union H).symm (Sum.inr a) = { val := a, property := (_ : a s t) }
                  def Equiv.Set.singleton {α : Type u_1} (a : α) :
                  {a} PUnit.{u}

                  A singleton set is equivalent to a PUnit type.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem Equiv.Set.ofEq_apply {α : Type u} {s : Set α} {t : Set α} (h : s = t) (a : { a // (fun a => (fun x => x s) a) a }) :
                    ↑(Equiv.Set.ofEq h) a = { val := a, property := (_ : ↑(Equiv.refl α) a t) }
                    @[simp]
                    theorem Equiv.Set.ofEq_symm_apply {α : Type u} {s : Set α} {t : Set α} (h : s = t) (b : { b // (fun b => (fun x => x t) b) b }) :
                    (Equiv.Set.ofEq h).symm b = { val := b, property := (_ : (Equiv.refl α).symm b s) }
                    def Equiv.Set.ofEq {α : Type u} {s : Set α} {t : Set α} (h : s = t) :
                    s t

                    Equal sets are equivalent.

                    TODO: this is the same as Equiv.setCongr!

                    Equations
                    Instances For
                      def Equiv.Set.insert {α : Type u} {s : Set α} [DecidablePred fun x => x s] {a : α} (H : ¬a s) :
                      ↑(insert a s) s PUnit.{u + 1}

                      If a ∉ s, then insert a s is equivalent to s ⊕ PUnit.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem Equiv.Set.insert_symm_apply_inl {α : Type u} {s : Set α} [DecidablePred fun x => x s] {a : α} (H : ¬a s) (b : s) :
                        (Equiv.Set.insert H).symm (Sum.inl b) = { val := b, property := (_ : b = a b s) }
                        @[simp]
                        theorem Equiv.Set.insert_symm_apply_inr {α : Type u} {s : Set α} [DecidablePred fun x => x s] {a : α} (H : ¬a s) (b : PUnit.{u + 1} ) :
                        (Equiv.Set.insert H).symm (Sum.inr b) = { val := a, property := (_ : a = a a s) }
                        @[simp]
                        theorem Equiv.Set.insert_apply_left {α : Type u} {s : Set α} [DecidablePred fun x => x s] {a : α} (H : ¬a s) :
                        ↑(Equiv.Set.insert H) { val := a, property := (_ : a = a a s) } = Sum.inr PUnit.unit
                        @[simp]
                        theorem Equiv.Set.insert_apply_right {α : Type u} {s : Set α} [DecidablePred fun x => x s] {a : α} (H : ¬a s) (b : s) :
                        ↑(Equiv.Set.insert H) { val := b, property := (_ : b = a b s) } = Sum.inl b
                        def Equiv.Set.sumCompl {α : Type u_1} (s : Set α) [DecidablePred fun x => x s] :
                        s s α

                        If s : Set α is a set with decidable membership, then s ⊕ sᶜ is equivalent to α.

                        Equations
                        Instances For
                          @[simp]
                          theorem Equiv.Set.sumCompl_apply_inl {α : Type u} (s : Set α) [DecidablePred fun x => x s] (x : s) :
                          ↑(Equiv.Set.sumCompl s) (Sum.inl x) = x
                          @[simp]
                          theorem Equiv.Set.sumCompl_apply_inr {α : Type u} (s : Set α) [DecidablePred fun x => x s] (x : s) :
                          ↑(Equiv.Set.sumCompl s) (Sum.inr x) = x
                          theorem Equiv.Set.sumCompl_symm_apply_of_mem {α : Type u} {s : Set α} [DecidablePred fun x => x s] {x : α} (hx : x s) :
                          (Equiv.Set.sumCompl s).symm x = Sum.inl { val := x, property := hx }
                          theorem Equiv.Set.sumCompl_symm_apply_of_not_mem {α : Type u} {s : Set α} [DecidablePred fun x => x s] {x : α} (hx : ¬x s) :
                          (Equiv.Set.sumCompl s).symm x = Sum.inr { val := x, property := hx }
                          @[simp]
                          theorem Equiv.Set.sumCompl_symm_apply {α : Type u_1} {s : Set α} [DecidablePred fun x => x s] {x : s} :
                          (Equiv.Set.sumCompl s).symm x = Sum.inl x
                          @[simp]
                          theorem Equiv.Set.sumCompl_symm_apply_compl {α : Type u_1} {s : Set α} [DecidablePred fun x => x s] {x : s} :
                          (Equiv.Set.sumCompl s).symm x = Sum.inr x
                          def Equiv.Set.sumDiffSubset {α : Type u_1} {s : Set α} {t : Set α} (h : s t) [DecidablePred fun x => x s] :
                          s ↑(t \ s) t

                          sumDiffSubset s t is the natural equivalence between s ⊕ (t \ s) and t, where s and t are two sets.

                          Equations
                          Instances For
                            @[simp]
                            theorem Equiv.Set.sumDiffSubset_apply_inl {α : Type u_1} {s : Set α} {t : Set α} (h : s t) [DecidablePred fun x => x s] (x : s) :
                            @[simp]
                            theorem Equiv.Set.sumDiffSubset_apply_inr {α : Type u_1} {s : Set α} {t : Set α} (h : s t) [DecidablePred fun x => x s] (x : ↑(t \ s)) :
                            theorem Equiv.Set.sumDiffSubset_symm_apply_of_mem {α : Type u_1} {s : Set α} {t : Set α} (h : s t) [DecidablePred fun x => x s] {x : t} (hx : x s) :
                            (Equiv.Set.sumDiffSubset h).symm x = Sum.inl { val := x, property := hx }
                            theorem Equiv.Set.sumDiffSubset_symm_apply_of_not_mem {α : Type u_1} {s : Set α} {t : Set α} (h : s t) [DecidablePred fun x => x s] {x : t} (hx : ¬x s) :
                            (Equiv.Set.sumDiffSubset h).symm x = Sum.inr { val := x, property := (_ : x t ¬x s) }
                            def Equiv.Set.unionSumInter {α : Type u} (s : Set α) (t : Set α) [DecidablePred fun x => x s] :
                            ↑(s t) ↑(s t) s t

                            If s is a set with decidable membership, then the sum of s ∪ t and s ∩ t is equivalent to s ⊕ t.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              def Equiv.Set.compl {α : Type u} {β : Type v} {s : Set α} {t : Set β} [DecidablePred fun x => x s] [DecidablePred fun x => x t] (e₀ : s t) :
                              { e // ∀ (x : s), e x = ↑(e₀ x) } (s t)

                              Given an equivalence e₀ between sets s : Set α and t : Set β, the set of equivalences e : α ≃ β such that e ↑x = ↑(e₀ x) for each x : s is equivalent to the set of equivalences between sᶜ and tᶜ.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                def Equiv.Set.prod {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) :
                                ↑(s ×ˢ t) s × t

                                The set product of two sets is equivalent to the type product of their coercions to types.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem Equiv.Set.univPi_symm_apply_coe {α : Type u_1} {β : αType u_2} (s : (a : α) → Set (β a)) (f : (a : α) → ↑(s a)) (a : α) :
                                  ↑((Equiv.Set.univPi s).symm f) a = ↑(f a)
                                  @[simp]
                                  theorem Equiv.Set.univPi_apply_coe {α : Type u_1} {β : αType u_2} (s : (a : α) → Set (β a)) (f : ↑(Set.pi Set.univ s)) (a : α) :
                                  ↑(↑(Equiv.Set.univPi s) f a) = f a
                                  def Equiv.Set.univPi {α : Type u_1} {β : αType u_2} (s : (a : α) → Set (β a)) :
                                  ↑(Set.pi Set.univ s) ((a : α) → ↑(s a))

                                  The set Set.pi Set.univ s is equivalent to Π a, s a.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    noncomputable def Equiv.Set.imageOfInjOn {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (H : Set.InjOn f s) :
                                    s ↑(f '' s)

                                    If a function f is injective on a set s, then s is equivalent to f '' s.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[simp]
                                      theorem Equiv.Set.image_apply {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (H : Function.Injective f) (p : s) :
                                      ↑(Equiv.Set.image f s H) p = { val := f p, property := (_ : f p f '' s) }
                                      noncomputable def Equiv.Set.image {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (H : Function.Injective f) :
                                      s ↑(f '' s)

                                      If f is an injective function, then s is equivalent to f '' s.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem Equiv.Set.image_symm_apply {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (H : Function.Injective f) (x : α) (h : x s) :
                                        (Equiv.Set.image f s H).symm { val := f x, property := (_ : a, a s f a = f x) } = { val := x, property := h }
                                        theorem Equiv.Set.image_symm_preimage {α : Type u_1} {β : Type u_2} {f : αβ} (hf : Function.Injective f) (u : Set α) (s : Set α) :
                                        (fun x => ↑((Equiv.Set.image f s hf).symm x)) ⁻¹' u = Subtype.val ⁻¹' (f '' u)
                                        @[simp]
                                        theorem Equiv.Set.congr_symm_apply {α : Type u_1} {β : Type u_2} (e : α β) (t : Set β) :
                                        (Equiv.Set.congr e).symm t = e.symm '' t
                                        @[simp]
                                        theorem Equiv.Set.congr_apply {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) :
                                        ↑(Equiv.Set.congr e) s = e '' s
                                        def Equiv.Set.congr {α : Type u_1} {β : Type u_2} (e : α β) :
                                        Set α Set β

                                        If α is equivalent to β, then Set α is equivalent to Set β.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          def Equiv.Set.sep {α : Type u} (s : Set α) (t : αProp) :
                                          {x | x s t x} {x | t x}

                                          The set {x ∈ s | t x} is equivalent to the set of x : s such that t x.

                                          Equations
                                          Instances For
                                            def Equiv.Set.powerset {α : Type u_1} (S : Set α) :
                                            ↑(𝒫 S) Set S

                                            The set 𝒫 S := {x | x ⊆ S} is equivalent to the type Set S.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              @[simp]
                                              theorem Equiv.Set.rangeSplittingImageEquiv_symm_apply_coe {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set ↑(Set.range f)) (x : s) :
                                              @[simp]
                                              theorem Equiv.Set.rangeSplittingImageEquiv_apply_coe_coe {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set ↑(Set.range f)) (x : ↑(Set.rangeSplitting f '' s)) :
                                              ↑(↑(Equiv.Set.rangeSplittingImageEquiv f s) x) = f x
                                              noncomputable def Equiv.Set.rangeSplittingImageEquiv {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set ↑(Set.range f)) :
                                              ↑(Set.rangeSplitting f '' s) s

                                              If s is a set in range f, then its image under rangeSplitting f is in bijection (via f) with s.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                @[simp]
                                                theorem Equiv.Set.rangeInl_symm_apply_coe (α : Type u_1) (β : Type u_2) (x : α) :
                                                ↑((Equiv.Set.rangeInl α β).symm x) = Sum.inl x
                                                def Equiv.Set.rangeInl (α : Type u_1) (β : Type u_2) :
                                                ↑(Set.range Sum.inl) α

                                                Equivalence between the range of Sum.inl : α → α ⊕ β and α.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  @[simp]
                                                  theorem Equiv.Set.rangeInl_apply_inl {α : Type u_1} (β : Type u_2) (x : α) :
                                                  ↑(Equiv.Set.rangeInl α β) { val := Sum.inl x, property := (_ : Sum.inl x Set.range Sum.inl) } = x
                                                  @[simp]
                                                  theorem Equiv.Set.rangeInr_symm_apply_coe (α : Type u_1) (β : Type u_2) (x : β) :
                                                  ↑((Equiv.Set.rangeInr α β).symm x) = Sum.inr x
                                                  def Equiv.Set.rangeInr (α : Type u_1) (β : Type u_2) :
                                                  ↑(Set.range Sum.inr) β

                                                  Equivalence between the range of Sum.inr : β → α ⊕ β and β.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    @[simp]
                                                    theorem Equiv.Set.rangeInr_apply_inr (α : Type u_1) {β : Type u_2} (x : β) :
                                                    ↑(Equiv.Set.rangeInr α β) { val := Sum.inr x, property := (_ : Sum.inr x Set.range Sum.inr) } = x
                                                    @[simp]
                                                    theorem Equiv.ofLeftInverse_apply_coe {α : Sort u_1} {β : Type u_2} (f : αβ) (f_inv : Nonempty αβα) (hf : ∀ (h : Nonempty α), Function.LeftInverse (f_inv h) f) (a : α) :
                                                    ↑(↑(Equiv.ofLeftInverse f f_inv hf) a) = f a
                                                    @[simp]
                                                    theorem Equiv.ofLeftInverse_symm_apply {α : Sort u_1} {β : Type u_2} (f : αβ) (f_inv : Nonempty αβα) (hf : ∀ (h : Nonempty α), Function.LeftInverse (f_inv h) f) (b : ↑(Set.range f)) :
                                                    (Equiv.ofLeftInverse f f_inv hf).symm b = f_inv (_ : Nonempty α) b
                                                    def Equiv.ofLeftInverse {α : Sort u_1} {β : Type u_2} (f : αβ) (f_inv : Nonempty αβα) (hf : ∀ (h : Nonempty α), Function.LeftInverse (f_inv h) f) :
                                                    α ↑(Set.range f)

                                                    If f : α → β has a left-inverse when α is nonempty, then α is computably equivalent to the range of f.

                                                    While awkward, the Nonempty α hypothesis on f_inv and hf allows this to be used when α is empty too. This hypothesis is absent on analogous definitions on stronger Equivs like LinearEquiv.ofLeftInverse and RingEquiv.ofLeftInverse as their typeclass assumptions are already sufficient to ensure non-emptiness.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      @[inline, reducible]
                                                      abbrev Equiv.ofLeftInverse' {α : Sort u_1} {β : Type u_2} (f : αβ) (f_inv : βα) (hf : Function.LeftInverse f_inv f) :
                                                      α ↑(Set.range f)

                                                      If f : α → β has a left-inverse, then α is computably equivalent to the range of f.

                                                      Note that if α is empty, no such f_inv exists and so this definition can't be used, unlike the stronger but less convenient ofLeftInverse.

                                                      Equations
                                                      Instances For
                                                        @[simp]
                                                        theorem Equiv.ofInjective_apply {α : Sort u_1} {β : Type u_2} (f : αβ) (hf : Function.Injective f) (a : α) :
                                                        ↑(Equiv.ofInjective f hf) a = { val := f a, property := (_ : y, f y = f a) }
                                                        noncomputable def Equiv.ofInjective {α : Sort u_1} {β : Type u_2} (f : αβ) (hf : Function.Injective f) :
                                                        α ↑(Set.range f)

                                                        If f : α → β is an injective function, then domain α is equivalent to the range of f.

                                                        Equations
                                                        Instances For
                                                          theorem Equiv.apply_ofInjective_symm {α : Sort u_1} {β : Type u_2} {f : αβ} (hf : Function.Injective f) (b : ↑(Set.range f)) :
                                                          f ((Equiv.ofInjective f hf).symm b) = b
                                                          @[simp]
                                                          theorem Equiv.ofInjective_symm_apply {α : Sort u_1} {β : Type u_2} {f : αβ} (hf : Function.Injective f) (a : α) :
                                                          (Equiv.ofInjective f hf).symm { val := f a, property := (_ : y, f y = f a) } = a
                                                          theorem Equiv.coe_ofInjective_symm {α : Type u_1} {β : Type u_2} {f : αβ} (hf : Function.Injective f) :
                                                          @[simp]
                                                          theorem Equiv.self_comp_ofInjective_symm {α : Sort u_1} {β : Type u_2} {f : αβ} (hf : Function.Injective f) :
                                                          f (Equiv.ofInjective f hf).symm = Subtype.val
                                                          theorem Equiv.ofLeftInverse_eq_ofInjective {α : Type u_1} {β : Type u_2} (f : αβ) (f_inv : Nonempty αβα) (hf : ∀ (h : Nonempty α), Function.LeftInverse (f_inv h) f) :
                                                          theorem Equiv.ofLeftInverse'_eq_ofInjective {α : Type u_1} {β : Type u_2} (f : αβ) (f_inv : βα) (hf : Function.LeftInverse f_inv f) :
                                                          theorem Equiv.set_forall_iff {α : Type u_1} {β : Type u_2} (e : α β) {p : Set αProp} :
                                                          ((a : Set α) → p a) (a : Set β) → p (e ⁻¹' a)
                                                          theorem Equiv.preimage_piEquivPiSubtypeProd_symm_pi {α : Type u_1} {β : αType u_2} (p : αProp) [DecidablePred p] (s : (i : α) → Set (β i)) :
                                                          (Equiv.piEquivPiSubtypeProd p β).symm ⁻¹' Set.pi Set.univ s = (Set.pi Set.univ fun i => s i) ×ˢ Set.pi Set.univ fun i => s i
                                                          @[simp]
                                                          theorem Equiv.sigmaPreimageEquiv_symm_apply_snd_coe {α : Type u_1} {β : Type u_2} (f : αβ) (x : α) :
                                                          ((Equiv.sigmaPreimageEquiv f).symm x).snd = x
                                                          @[simp]
                                                          theorem Equiv.sigmaPreimageEquiv_apply {α : Type u_1} {β : Type u_2} (f : αβ) (x : (y : β) × { x // f x = y }) :
                                                          ↑(Equiv.sigmaPreimageEquiv f) x = x.snd
                                                          @[simp]
                                                          theorem Equiv.sigmaPreimageEquiv_symm_apply_fst {α : Type u_1} {β : Type u_2} (f : αβ) (x : α) :
                                                          ((Equiv.sigmaPreimageEquiv f).symm x).fst = f x
                                                          def Equiv.sigmaPreimageEquiv {α : Type u_1} {β : Type u_2} (f : αβ) :
                                                          (b : β) × ↑(f ⁻¹' {b}) α

                                                          sigmaPreimageEquiv f for f : α → β is the natural equivalence between the type of all preimages of points under f and the total space α.

                                                          Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem Equiv.ofPreimageEquiv_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αγ} {g : βγ} (e : (c : γ) → ↑(f ⁻¹' {c}) ↑(g ⁻¹' {c})) :
                                                            ∀ (a : α), ↑(Equiv.ofPreimageEquiv e) a = ↑(↑(e (f a)) ((Equiv.sigmaFiberEquiv fun a => f a).symm a).snd)
                                                            @[simp]
                                                            theorem Equiv.ofPreimageEquiv_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αγ} {g : βγ} (e : (c : γ) → ↑(f ⁻¹' {c}) ↑(g ⁻¹' {c})) :
                                                            ∀ (a : β), (Equiv.ofPreimageEquiv e).symm a = ((Equiv.sigmaCongrRight e).symm ((Equiv.sigmaFiberEquiv fun b => g b).symm a)).snd
                                                            def Equiv.ofPreimageEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αγ} {g : βγ} (e : (c : γ) → ↑(f ⁻¹' {c}) ↑(g ⁻¹' {c})) :
                                                            α β

                                                            A family of equivalences between preimages of points gives an equivalence between domains.

                                                            Equations
                                                            Instances For
                                                              theorem Equiv.ofPreimageEquiv_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αγ} {g : βγ} (e : (c : γ) → ↑(f ⁻¹' {c}) ↑(g ⁻¹' {c})) (a : α) :
                                                              g (↑(Equiv.ofPreimageEquiv e) a) = f a
                                                              noncomputable def Set.BijOn.equiv {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (f : αβ) (h : Set.BijOn f s t) :
                                                              s t

                                                              If a function is a bijection between two sets s and t, then it induces an equivalence between the types ↥s and ↥t.

                                                              Equations
                                                              Instances For
                                                                theorem dite_comp_equiv_update {α : Type u_1} {β : Sort u_2} {γ : Sort u_3} {p : αProp} (e : β Subtype p) (v : βγ) (w : αγ) (j : β) (x : γ) [DecidableEq β] [DecidableEq α] [(j : α) → Decidable (p j)] :
                                                                (fun i => if h : p i then Function.update v j x (e.symm { val := i, property := h }) else w i) = Function.update (fun i => if h : p i then v (e.symm { val := i, property := h }) else w i) (↑(e j)) x

                                                                The composition of an updated function with an equiv on a subtype can be expressed as an updated function.