Documentation

Mathlib.Order.Hom.Set

Order homomorphisms and sets #

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

Order isomorphism between two equal sets.

Equations
Instances For
    def OrderIso.Set.univ {α : Type u_2} [Preorder α] :
    Set.univ ≃o α

    Order isomorphism between univ : Set α and α.

    Equations
    Instances For
      @[simp]
      theorem OrderEmbedding.orderIso_apply {α : Type u_2} {β : Type u_3} [LE α] [LE β] {f : α ↪o β} (a : α) :
      OrderEmbedding.orderIso a = f a,
      noncomputable def OrderEmbedding.orderIso {α : Type u_2} {β : Type u_3} [LE α] [LE β] {f : α ↪o β} :
      α ≃o (Set.range f)

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

      Equations
      Instances For
        noncomputable def StrictMonoOn.orderIso {α : Type u_6} {β : Type u_7} [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
          @[simp]
          theorem StrictMono.orderIso_apply {α : Type u_2} {β : Type u_3} [LinearOrder α] [Preorder β] (f : αβ) (h_mono : StrictMono f) (a : α) :
          (StrictMono.orderIso f h_mono) a = f a,
          noncomputable def StrictMono.orderIso {α : Type u_2} {β : Type u_3} [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
            noncomputable def StrictMono.orderIsoOfSurjective {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [LinearOrder α] [Preorder β] (f : αβ) (h_mono : StrictMono f) (h_surj : Function.Surjective f) :
              (StrictMono.orderIsoOfSurjective f h_mono h_surj) = f
              @[simp]
              theorem StrictMono.orderIsoOfSurjective_symm_apply_self {α : Type u_2} {β : Type u_3} [LinearOrder α] [Preorder β] (f : αβ) (h_mono : StrictMono f) (h_surj : Function.Surjective f) (a : α) :
              (StrictMono.orderIsoOfSurjective f h_mono h_surj).symm (f a) = a
              theorem StrictMono.orderIsoOfSurjective_self_symm_apply {α : Type u_2} {β : Type u_3} [LinearOrder α] [Preorder β] (f : αβ) (h_mono : StrictMono f) (h_surj : Function.Surjective f) (b : β) :
              f ((StrictMono.orderIsoOfSurjective f h_mono h_surj).symm b) = b
              theorem OrderEmbedding.range_inj {α : Type u_2} {β : Type u_3} [LinearOrder α] [WellFoundedLT α] [Preorder β] {f : α ↪o β} {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
              • =
              Equations
              Equations
              • =
              Equations
              • =
              Equations
              @[simp]
              theorem OrderIso.compl_apply (α : Type u_2) [BooleanAlgebra α] :
              ∀ (a : α), (OrderIso.compl α) a = (OrderDual.toDual a)
              @[simp]
              theorem OrderIso.compl_symm_apply (α : Type u_2) [BooleanAlgebra α] :
              ∀ (a : αᵒᵈ), (RelIso.symm (OrderIso.compl α)) a = (OrderDual.ofDual a)
              def OrderIso.compl (α : Type u_2) [BooleanAlgebra α] :

              Taking complements as an order isomorphism to the order dual.

              Equations
              • OrderIso.compl α = { toFun := OrderDual.toDual compl, invFun := compl OrderDual.ofDual, left_inv := , right_inv := , map_rel_iff' := }
              Instances For
                theorem compl_strictAnti (α : Type u_2) [BooleanAlgebra α] :
                theorem compl_antitone (α : Type u_2) [BooleanAlgebra α] :
                Antitone compl