Documentation

Mathlib.Order.Hom.Set

Order homomorphisms and sets #

def Set.sumEquiv {α : Type u_1} {β : Type u_2} :
Set (α β) ≃o Set α × Set β

Sets on sum types are order-equivalent to pairs of sets on each summand.

Equations
    Instances For
      theorem OrderIso.range_eq {α : Type u_1} {β : Type u_2} [LE α] [LE β] (e : α ≃o β) :
      @[simp]
      theorem OrderIso.symm_image_image {α : Type u_1} {β : Type u_2} [LE α] [LE β] (e : α ≃o β) (s : Set α) :
      e.symm '' (e '' s) = s
      @[simp]
      theorem OrderIso.image_symm_image {α : Type u_1} {β : Type u_2} [LE α] [LE β] (e : α ≃o β) (s : Set β) :
      e '' (e.symm '' s) = s
      theorem OrderIso.image_eq_preimage {α : Type u_1} {β : Type u_2} [LE α] [LE β] (e : α ≃o β) (s : Set α) :
      e '' s = e.symm ⁻¹' s
      @[simp]
      theorem OrderIso.preimage_symm_preimage {α : Type u_1} {β : Type u_2} [LE α] [LE β] (e : α ≃o β) (s : Set α) :
      e ⁻¹' (e.symm ⁻¹' s) = s
      @[simp]
      theorem OrderIso.symm_preimage_preimage {α : Type u_1} {β : Type u_2} [LE α] [LE β] (e : α ≃o β) (s : Set β) :
      e.symm ⁻¹' (e ⁻¹' s) = s
      @[simp]
      theorem OrderIso.image_preimage {α : Type u_1} {β : Type u_2} [LE α] [LE β] (e : α ≃o β) (s : Set β) :
      e '' (e ⁻¹' s) = s
      @[simp]
      theorem OrderIso.preimage_image {α : Type u_1} {β : Type u_2} [LE α] [LE β] (e : α ≃o β) (s : Set α) :
      e ⁻¹' (e '' s) = s
      def OrderIso.setCongr {α : Type u_1} [Preorder α] (s t : Set α) (h : s = t) :
      s ≃o t

      Order isomorphism between two equal sets.

      Equations
        Instances For

          Order isomorphism between univ : Set α and α.

          Equations
            Instances For
              noncomputable def OrderEmbedding.orderIso {α : Type u_1} {β : Type u_2} [LE α] [LE β] {f : α ↪o β} :
              α ≃o (Set.range f)

              We can regard an order embedding as an order isomorphism to its range.

              Equations
                Instances For
                  @[simp]
                  theorem OrderEmbedding.orderIso_apply {α : Type u_1} {β : Type u_2} [LE α] [LE β] {f : α ↪o β} (a : α) :
                  orderIso a = f a,
                  noncomputable def StrictMonoOn.orderIso {α : Type u_3} {β : Type u_4} [LinearOrder α] [Preorder β] (f : αβ) (s : Set α) (hf : StrictMonoOn f s) :
                  s ≃o ↑(f '' s)

                  If a function f is strictly monotone on a set s, then it defines an order isomorphism between s and its image.

                  Equations
                    Instances For
                      noncomputable def StrictMono.orderIso {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] (f : αβ) (h_mono : StrictMono f) :
                      α ≃o (Set.range f)

                      A strictly monotone function from a linear order is an order isomorphism between its domain and its range.

                      Equations
                        Instances For
                          @[simp]
                          theorem StrictMono.orderIso_apply {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] (f : αβ) (h_mono : StrictMono f) (a : α) :
                          (StrictMono.orderIso f h_mono) a = f a,
                          noncomputable def StrictMono.orderIsoOfSurjective {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] (f : αβ) (h_mono : StrictMono f) (h_surj : Function.Surjective f) :
                          α ≃o β

                          A strictly monotone surjective function from a linear order is an order isomorphism.

                          Equations
                            Instances For
                              @[simp]
                              theorem StrictMono.coe_orderIsoOfSurjective {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] (f : αβ) (h_mono : StrictMono f) (h_surj : Function.Surjective f) :
                              (orderIsoOfSurjective f h_mono h_surj) = f
                              @[simp]
                              theorem StrictMono.orderIsoOfSurjective_symm_apply_self {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] (f : αβ) (h_mono : StrictMono f) (h_surj : Function.Surjective f) (a : α) :
                              (orderIsoOfSurjective f h_mono h_surj).symm (f a) = a
                              theorem StrictMono.orderIsoOfSurjective_self_symm_apply {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] (f : αβ) (h_mono : StrictMono f) (h_surj : Function.Surjective f) (b : β) :
                              f ((orderIsoOfSurjective f h_mono h_surj).symm b) = b
                              theorem OrderEmbedding.range_inj {α : Type u_1} {β : Type u_2} [LinearOrder α] [WellFoundedLT α] [Preorder β] {f g : α ↪o β} :
                              Set.range f = Set.range g f = g

                              Two order embeddings on a well-order are equal provided that their ranges are equal.

                              Equations
                                Equations
                                  def OrderIso.Iic {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (e : α ≃o β) (x : α) :
                                  (Set.Iic x) ≃o (Set.Iic (e x))

                                  An order isomorphism between lattices induces an order isomorphism between corresponding interval sublattices.

                                  Equations
                                    Instances For
                                      def OrderIso.Ici {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (e : α ≃o β) (x : α) :
                                      (Set.Ici x) ≃o (Set.Ici (e x))

                                      An order isomorphism between lattices induces an order isomorphism between corresponding interval sublattices.

                                      Equations
                                        Instances For
                                          def OrderIso.Icc {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (e : α ≃o β) (x y : α) :
                                          (Set.Icc x y) ≃o (Set.Icc (e x) (e y))

                                          An order isomorphism between lattices induces an order isomorphism between corresponding interval sublattices.

                                          Equations
                                            Instances For
                                              def OrderIso.compl (α : Type u_1) [BooleanAlgebra α] :

                                              Taking complements as an order isomorphism to the order dual.

                                              Equations
                                                Instances For
                                                  @[simp]
                                                  theorem OrderIso.compl_apply (α : Type u_1) [BooleanAlgebra α] (a✝ : α) :
                                                  (compl α) a✝ = (OrderDual.toDual a✝)
                                                  @[simp]
                                                  theorem OrderIso.compl_symm_apply (α : Type u_1) [BooleanAlgebra α] (a✝ : αᵒᵈ) :