Documentation

Mathlib.Order.Hom.Basic

Order homomorphisms #

This file defines order homomorphisms, which are bundled monotone functions. A preorder homomorphism f : α →o β is a function α → β along with a proof that ∀ x y, x ≤ y → f x ≤ f y.

Main definitions #

In this file we define the following bundled monotone maps:

We also define many OrderHoms. In some cases we define two versions, one with suffix and one without it (e.g., OrderHom.compₘ and OrderHom.comp). This means that the former function is a "more bundled" version of the latter. We can't just drop the "less bundled" version because the more bundled version usually does not work with dot notation.

We also define two functions to convert other bundled maps to α →o β:

Tags #

monotone map, bundled morphism

structure OrderHom (α : Type u_6) (β : Type u_7) [Preorder α] [Preorder β] :
Type (max u_6 u_7)

Bundled monotone (aka, increasing) function

  • toFun : αβ

    The underlying function of an OrderHom.

  • monotone' : Monotone self.toFun

    The underlying function of an OrderHom is monotone.

Instances For
    @[inline, reducible]
    abbrev OrderEmbedding (α : Type u_6) (β : Type u_7) [LE α] [LE β] :
    Type (max u_6 u_7)

    An order embedding is an embedding f : α ↪ β such that a ≤ b ↔ (f a) ≤ (f b). This definition is an abbreviation of RelEmbedding (≤) (≤).

    Equations
    • (α ↪o β) = ((fun (x x_1 : α) => x x_1) ↪r fun (x x_1 : β) => x x_1)
    Instances For
      @[inline, reducible]
      abbrev OrderIso (α : Type u_6) (β : Type u_7) [LE α] [LE β] :
      Type (max u_6 u_7)

      An order isomorphism is an equivalence such that a ≤ b ↔ (f a) ≤ (f b). This definition is an abbreviation of RelIso (≤) (≤).

      Equations
      • (α ≃o β) = ((fun (x x_1 : α) => x x_1) ≃r fun (x x_1 : β) => x x_1)
      Instances For
        @[inline, reducible]
        abbrev OrderHomClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [LE α] [LE β] [FunLike F α β] :

        OrderHomClass F α b asserts that F is a type of -preserving morphisms.

        Equations
        Instances For
          class OrderIsoClass (F : Type u_6) (α : Type u_7) (β : Type u_8) [LE α] [LE β] [EquivLike F α β] :

          OrderIsoClass F α β states that F is a type of order isomorphisms.

          You should extend this class when you extend OrderIso.

          • map_le_map_iff : ∀ (f : F) {a b : α}, f a f b a b

            An order isomorphism respects .

          Instances
            def OrderIsoClass.toOrderIso {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [LE β] [EquivLike F α β] [OrderIsoClass F α β] (f : F) :
            α ≃o β

            Turn an element of a type F satisfying OrderIsoClass F α β into an actual OrderIso. This is declared as the default coercion from F to α ≃o β.

            Equations
            • f = let __src := f; { toEquiv := __src, map_rel_iff' := }
            Instances For
              instance instCoeTCOrderIso {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [LE β] [EquivLike F α β] [OrderIsoClass F α β] :
              CoeTC F (α ≃o β)

              Any type satisfying OrderIsoClass can be cast into OrderIso via OrderIsoClass.toOrderIso.

              Equations
              • instCoeTCOrderIso = { coe := OrderIsoClass.toOrderIso }
              instance OrderIsoClass.toOrderHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [LE β] [EquivLike F α β] [OrderIsoClass F α β] :
              Equations
              • =
              theorem OrderHomClass.monotone {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [FunLike F α β] [OrderHomClass F α β] (f : F) :
              theorem OrderHomClass.mono {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [FunLike F α β] [OrderHomClass F α β] (f : F) :
              def OrderHomClass.toOrderHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [FunLike F α β] [OrderHomClass F α β] (f : F) :
              α →o β

              Turn an element of a type F satisfying OrderHomClass F α β into an actual OrderHom. This is declared as the default coercion from F to α →o β.

              Equations
              • f = { toFun := f, monotone' := }
              Instances For
                instance OrderHomClass.instCoeTCOrderHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [FunLike F α β] [OrderHomClass F α β] :
                CoeTC F (α →o β)

                Any type satisfying OrderHomClass can be cast into OrderHom via OrderHomClass.toOrderHom.

                Equations
                • OrderHomClass.instCoeTCOrderHom = { coe := OrderHomClass.toOrderHom }
                @[simp]
                theorem map_inv_le_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [LE β] [EquivLike F α β] [OrderIsoClass F α β] (f : F) {a : α} {b : β} :
                EquivLike.inv f b a b f a
                @[simp]
                theorem le_map_inv_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [LE β] [EquivLike F α β] [OrderIsoClass F α β] (f : F) {a : α} {b : β} :
                a EquivLike.inv f b f a b
                theorem map_lt_map_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [EquivLike F α β] [OrderIsoClass F α β] (f : F) {a : α} {b : α} :
                f a < f b a < b
                @[simp]
                theorem map_inv_lt_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [EquivLike F α β] [OrderIsoClass F α β] (f : F) {a : α} {b : β} :
                EquivLike.inv f b < a b < f a
                @[simp]
                theorem lt_map_inv_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [EquivLike F α β] [OrderIsoClass F α β] (f : F) {a : α} {b : β} :
                a < EquivLike.inv f b f a < b
                instance OrderHom.instFunLikeOrderHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] :
                FunLike (α →o β) α β
                Equations
                • OrderHom.instFunLikeOrderHom = { coe := OrderHom.toFun, coe_injective' := }
                Equations
                • =
                @[simp]
                theorem OrderHom.coe_mk {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : αβ) (hf : Monotone f) :
                { toFun := f, monotone' := hf } = f
                theorem OrderHom.monotone {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :
                theorem OrderHom.mono {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :
                def OrderHom.Simps.coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :
                αβ

                See Note [custom simps projection]. We give this manually so that we use toFun as the projection directly instead.

                Equations
                Instances For
                  @[simp]
                  theorem OrderHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :
                  f.toFun = f
                  theorem OrderHom.ext {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) (g : α →o β) (h : f = g) :
                  f = g
                  @[simp]
                  theorem OrderHom.coe_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :
                  f = f
                  @[simp]
                  theorem OrderHomClass.coe_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {F : Type u_6} [FunLike F α β] [OrderHomClass F α β] (f : F) :
                  f = f
                  instance OrderHom.canLift {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] :
                  CanLift (αβ) (α →o β) DFunLike.coe Monotone

                  One can lift an unbundled monotone function to a bundled one.

                  Equations
                  • =
                  def OrderHom.copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) (f' : αβ) (h : f' = f) :
                  α →o β

                  Copy of an OrderHom with a new toFun equal to the old one. Useful to fix definitional equalities.

                  Equations
                  Instances For
                    @[simp]
                    theorem OrderHom.coe_copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) (f' : αβ) (h : f' = f) :
                    (OrderHom.copy f f' h) = f'
                    theorem OrderHom.copy_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) (f' : αβ) (h : f' = f) :
                    OrderHom.copy f f' h = f
                    @[simp]
                    theorem OrderHom.id_coe {α : Type u_2} [Preorder α] :
                    OrderHom.id = id
                    def OrderHom.id {α : Type u_2} [Preorder α] :
                    α →o α

                    The identity function as bundled monotone function.

                    Equations
                    • OrderHom.id = { toFun := id, monotone' := }
                    Instances For
                      instance OrderHom.instInhabitedOrderHom {α : Type u_2} [Preorder α] :
                      Inhabited (α →o α)
                      Equations
                      • OrderHom.instInhabitedOrderHom = { default := OrderHom.id }
                      instance OrderHom.instPreorderOrderHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] :
                      Preorder (α →o β)

                      The preorder structure of α →o β is pointwise inequality: f ≤ g ↔ ∀ a, f a ≤ g a.

                      Equations
                      Equations
                      theorem OrderHom.le_def {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {f : α →o β} {g : α →o β} :
                      f g ∀ (x : α), f x g x
                      @[simp]
                      theorem OrderHom.coe_le_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {f : α →o β} {g : α →o β} :
                      f g f g
                      @[simp]
                      theorem OrderHom.mk_le_mk {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {f : αβ} {g : αβ} {hf : Monotone f} {hg : Monotone g} :
                      { toFun := f, monotone' := hf } { toFun := g, monotone' := hg } f g
                      theorem OrderHom.apply_mono {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {f : α →o β} {g : α →o β} {x : α} {y : α} (h₁ : f g) (h₂ : x y) :
                      f x g y
                      def OrderHom.curry {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] :
                      (α × β →o γ) ≃o (α →o β →o γ)

                      Curry/uncurry as an order isomorphism between α × β →o γ and α →o β →o γ.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem OrderHom.curry_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : α × β →o γ) (x : α) (y : β) :
                        ((OrderHom.curry f) x) y = f (x, y)
                        @[simp]
                        theorem OrderHom.curry_symm_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : α →o β →o γ) (x : α × β) :
                        ((RelIso.symm OrderHom.curry) f) x = (f x.1) x.2
                        @[simp]
                        theorem OrderHom.comp_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (g : β →o γ) (f : α →o β) :
                        (OrderHom.comp g f) = g f
                        def OrderHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (g : β →o γ) (f : α →o β) :
                        α →o γ

                        The composition of two bundled monotone functions.

                        Equations
                        Instances For
                          theorem OrderHom.comp_mono {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] ⦃g₁ : β →o γ ⦃g₂ : β →o γ (hg : g₁ g₂) ⦃f₁ : α →o β ⦃f₂ : α →o β (hf : f₁ f₂) :
                          OrderHom.comp g₁ f₁ OrderHom.comp g₂ f₂
                          @[simp]
                          theorem OrderHom.compₘ_coe_coe_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (x : β →o γ) :
                          ∀ (a : α →o β), ((OrderHom.compₘ x) a) = x a
                          def OrderHom.compₘ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] :
                          (β →o γ) →o (α →o β) →o α →o γ

                          The composition of two bundled monotone functions, a fully bundled version.

                          Equations
                          • OrderHom.compₘ = OrderHom.curry { toFun := fun (f : (β →o γ) × (α →o β)) => OrderHom.comp f.1 f.2, monotone' := }
                          Instances For
                            @[simp]
                            theorem OrderHom.comp_id {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :
                            OrderHom.comp f OrderHom.id = f
                            @[simp]
                            theorem OrderHom.id_comp {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :
                            OrderHom.comp OrderHom.id f = f
                            @[simp]
                            theorem OrderHom.const_coe_coe (α : Type u_6) [Preorder α] {β : Type u_7} [Preorder β] (b : β) :
                            def OrderHom.const (α : Type u_6) [Preorder α] {β : Type u_7} [Preorder β] :
                            β →o α →o β

                            Constant function bundled as an OrderHom.

                            Equations
                            Instances For
                              @[simp]
                              theorem OrderHom.const_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : α →o β) (c : γ) :
                              @[simp]
                              theorem OrderHom.comp_const {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (γ : Type u_6) [Preorder γ] (f : α →o β) (c : α) :
                              @[simp]
                              theorem OrderHom.prod_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : α →o β) (g : α →o γ) (x : α) :
                              (OrderHom.prod f g) x = (f x, g x)
                              def OrderHom.prod {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : α →o β) (g : α →o γ) :
                              α →o β × γ

                              Given two bundled monotone maps f, g, f.prod g is the map x ↦ (f x, g x) bundled as a OrderHom.

                              Equations
                              • OrderHom.prod f g = { toFun := fun (x : α) => (f x, g x), monotone' := }
                              Instances For
                                theorem OrderHom.prod_mono {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] {f₁ : α →o β} {f₂ : α →o β} (hf : f₁ f₂) {g₁ : α →o γ} {g₂ : α →o γ} (hg : g₁ g₂) :
                                OrderHom.prod f₁ g₁ OrderHom.prod f₂ g₂
                                theorem OrderHom.comp_prod_comp_same {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f₁ : β →o γ) (f₂ : β →o γ) (g : α →o β) :
                                @[simp]
                                theorem OrderHom.prodₘ_coe_coe_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (x : α →o β) :
                                ∀ (a : α →o γ) (x_1 : α), ((OrderHom.prodₘ x) a) x_1 = (x x_1, a x_1)
                                def OrderHom.prodₘ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] :
                                (α →o β) →o (α →o γ) →o α →o β × γ

                                Given two bundled monotone maps f, g, f.prod g is the map x ↦ (f x, g x) bundled as a OrderHom. This is a fully bundled version.

                                Equations
                                • OrderHom.prodₘ = OrderHom.curry { toFun := fun (f : (α →o β) × (α →o γ)) => OrderHom.prod f.1 f.2, monotone' := }
                                Instances For
                                  @[simp]
                                  theorem OrderHom.diag_coe {α : Type u_2} [Preorder α] (x : α) :
                                  OrderHom.diag x = (x, x)
                                  def OrderHom.diag {α : Type u_2} [Preorder α] :
                                  α →o α × α

                                  Diagonal embedding of α into α × α as an OrderHom.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem OrderHom.onDiag_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o α →o β) :
                                    ∀ (a : α), (OrderHom.onDiag f) a = (f a) a
                                    def OrderHom.onDiag {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o α →o β) :
                                    α →o β

                                    Restriction of f : α →o α →o β to the diagonal.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem OrderHom.fst_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (self : α × β) :
                                      OrderHom.fst self = self.1
                                      def OrderHom.fst {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] :
                                      α × β →o α

                                      Prod.fst as an OrderHom.

                                      Equations
                                      • OrderHom.fst = { toFun := Prod.fst, monotone' := }
                                      Instances For
                                        @[simp]
                                        theorem OrderHom.snd_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (self : α × β) :
                                        OrderHom.snd self = self.2
                                        def OrderHom.snd {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] :
                                        α × β →o β

                                        Prod.snd as an OrderHom.

                                        Equations
                                        • OrderHom.snd = { toFun := Prod.snd, monotone' := }
                                        Instances For
                                          @[simp]
                                          theorem OrderHom.fst_prod_snd {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] :
                                          OrderHom.prod OrderHom.fst OrderHom.snd = OrderHom.id
                                          @[simp]
                                          theorem OrderHom.fst_comp_prod {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : α →o β) (g : α →o γ) :
                                          OrderHom.comp OrderHom.fst (OrderHom.prod f g) = f
                                          @[simp]
                                          theorem OrderHom.snd_comp_prod {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : α →o β) (g : α →o γ) :
                                          OrderHom.comp OrderHom.snd (OrderHom.prod f g) = g
                                          @[simp]
                                          theorem OrderHom.prodIso_symm_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : (α →o β) × (α →o γ)) :
                                          (RelIso.symm OrderHom.prodIso) f = OrderHom.prod f.1 f.2
                                          @[simp]
                                          theorem OrderHom.prodIso_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : α →o β × γ) :
                                          OrderHom.prodIso f = (OrderHom.comp OrderHom.fst f, OrderHom.comp OrderHom.snd f)
                                          def OrderHom.prodIso {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] :
                                          (α →o β × γ) ≃o (α →o β) × (α →o γ)

                                          Order isomorphism between the space of monotone maps to β × γ and the product of the spaces of monotone maps to β and γ.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            @[simp]
                                            theorem OrderHom.prodMap_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] (f : α →o β) (g : γ →o δ) :
                                            ∀ (a : α × γ), (OrderHom.prodMap f g) a = Prod.map (f) (g) a
                                            def OrderHom.prodMap {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] (f : α →o β) (g : γ →o δ) :
                                            α × γ →o β × δ

                                            Prod.map of two OrderHoms as an OrderHom.

                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem Pi.evalOrderHom_coe {ι : Type u_6} {π : ιType u_7} [(i : ι) → Preorder (π i)] (i : ι) :
                                              def Pi.evalOrderHom {ι : Type u_6} {π : ιType u_7} [(i : ι) → Preorder (π i)] (i : ι) :
                                              ((j : ι) → π j) →o π i

                                              Evaluation of an unbundled function at a point (Function.eval) as an OrderHom.

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem OrderHom.coeFnHom_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] :
                                                OrderHom.coeFnHom = fun (f : α →o β) => f
                                                def OrderHom.coeFnHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] :
                                                (α →o β) →o αβ

                                                The "forgetful functor" from α →o β to α → β that takes the underlying function, is monotone.

                                                Equations
                                                • OrderHom.coeFnHom = { toFun := fun (f : α →o β) => f, monotone' := }
                                                Instances For
                                                  @[simp]
                                                  theorem OrderHom.apply_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (x : α) :
                                                  (OrderHom.apply x) = Function.eval x fun (f : α →o β) => f
                                                  def OrderHom.apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (x : α) :
                                                  (α →o β) →o β

                                                  Function application fun f => f a (for fixed a) is a monotone function from the monotone function space α →o β to β. See also Pi.evalOrderHom.

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem OrderHom.pi_coe {α : Type u_2} [Preorder α] {ι : Type u_6} {π : ιType u_7} [(i : ι) → Preorder (π i)] (f : (i : ι) → α →o π i) (x : α) (i : ι) :
                                                    (OrderHom.pi f) x i = (f i) x
                                                    def OrderHom.pi {α : Type u_2} [Preorder α] {ι : Type u_6} {π : ιType u_7} [(i : ι) → Preorder (π i)] (f : (i : ι) → α →o π i) :
                                                    α →o (i : ι) → π i

                                                    Construct a bundled monotone map α →o Π i, π i from a family of monotone maps f i : α →o π i.

                                                    Equations
                                                    • OrderHom.pi f = { toFun := fun (x : α) (i : ι) => (f i) x, monotone' := }
                                                    Instances For
                                                      @[simp]
                                                      theorem OrderHom.piIso_apply {α : Type u_2} [Preorder α] {ι : Type u_6} {π : ιType u_7} [(i : ι) → Preorder (π i)] (f : α →o (i : ι) → π i) (i : ι) :
                                                      OrderHom.piIso f i = OrderHom.comp (Pi.evalOrderHom i) f
                                                      @[simp]
                                                      theorem OrderHom.piIso_symm_apply {α : Type u_2} [Preorder α] {ι : Type u_6} {π : ιType u_7} [(i : ι) → Preorder (π i)] (f : (i : ι) → α →o π i) :
                                                      (RelIso.symm OrderHom.piIso) f = OrderHom.pi f
                                                      def OrderHom.piIso {α : Type u_2} [Preorder α] {ι : Type u_6} {π : ιType u_7} [(i : ι) → Preorder (π i)] :
                                                      (α →o (i : ι) → π i) ≃o ((i : ι) → α →o π i)

                                                      Order isomorphism between bundled monotone maps α →o Π i, π i and families of bundled monotone maps Π i, α →o π i.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        @[simp]
                                                        theorem OrderHom.Subtype.val_coe {α : Type u_2} [Preorder α] (p : αProp) :
                                                        (OrderHom.Subtype.val p) = Subtype.val
                                                        def OrderHom.Subtype.val {α : Type u_2} [Preorder α] (p : αProp) :

                                                        Subtype.val as a bundled monotone function.

                                                        Equations
                                                        Instances For
                                                          @[simp]
                                                          theorem Subtype.orderEmbedding_apply_coe {α : Type u_2} [Preorder α] {p : αProp} {q : αProp} (h : ∀ (a : α), p aq a) (x : { x : α // (fun (x : α) => p x) x }) :
                                                          ((Subtype.orderEmbedding h) x) = x
                                                          def Subtype.orderEmbedding {α : Type u_2} [Preorder α] {p : αProp} {q : αProp} (h : ∀ (a : α), p aq a) :
                                                          { x : α // p x } ↪o { x : α // q x }

                                                          Subtype.impEmbedding as an order embedding.

                                                          Equations
                                                          Instances For
                                                            instance OrderHom.unique {α : Type u_2} [Preorder α] [Subsingleton α] :
                                                            Unique (α →o α)

                                                            There is a unique monotone map from a subsingleton to itself.

                                                            Equations
                                                            • OrderHom.unique = { toInhabited := { default := OrderHom.id }, uniq := }
                                                            theorem OrderHom.orderHom_eq_id {α : Type u_2} [Preorder α] [Subsingleton α] (g : α →o α) :
                                                            g = OrderHom.id
                                                            @[simp]
                                                            theorem OrderHom.dual_apply_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :
                                                            ∀ (a : αᵒᵈ), (OrderHom.dual f) a = (OrderDual.toDual f OrderDual.ofDual) a
                                                            @[simp]
                                                            theorem OrderHom.dual_symm_apply_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : αᵒᵈ →o βᵒᵈ) :
                                                            ∀ (a : α), (OrderHom.dual.symm f) a = (OrderDual.ofDual f OrderDual.toDual) a
                                                            def OrderHom.dual {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] :
                                                            (α →o β) (αᵒᵈ →o βᵒᵈ)

                                                            Reinterpret a bundled monotone function as a monotone function between dual orders.

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              @[simp]
                                                              theorem OrderHom.dual_id {α : Type u_2} [Preorder α] :
                                                              OrderHom.dual OrderHom.id = OrderHom.id
                                                              @[simp]
                                                              theorem OrderHom.dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (g : β →o γ) (f : α →o β) :
                                                              OrderHom.dual (OrderHom.comp g f) = OrderHom.comp (OrderHom.dual g) (OrderHom.dual f)
                                                              @[simp]
                                                              theorem OrderHom.symm_dual_id {α : Type u_2} [Preorder α] :
                                                              OrderHom.dual.symm OrderHom.id = OrderHom.id
                                                              @[simp]
                                                              theorem OrderHom.symm_dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (g : βᵒᵈ →o γᵒᵈ) (f : αᵒᵈ →o βᵒᵈ) :
                                                              OrderHom.dual.symm (OrderHom.comp g f) = OrderHom.comp (OrderHom.dual.symm g) (OrderHom.dual.symm f)
                                                              def OrderHom.dualIso (α : Type u_8) (β : Type u_9) [Preorder α] [Preorder β] :

                                                              OrderHom.dual as an order isomorphism.

                                                              Equations
                                                              • OrderHom.dualIso α β = { toEquiv := OrderHom.dual.trans OrderDual.toDual, map_rel_iff' := }
                                                              Instances For
                                                                @[simp]
                                                                theorem OrderHom.withBotMap_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :
                                                                def OrderHom.withBotMap {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :

                                                                Lift an order homomorphism f : α →o β to an order homomorphism WithBot α →o WithBot β.

                                                                Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem OrderHom.withTopMap_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :
                                                                  def OrderHom.withTopMap {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :

                                                                  Lift an order homomorphism f : α →o β to an order homomorphism WithTop α →o WithTop β.

                                                                  Equations
                                                                  Instances For
                                                                    def RelEmbedding.orderEmbeddingOfLTEmbedding {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] (f : (fun (x x_1 : α) => x < x_1) ↪r fun (x x_1 : β) => x < x_1) :
                                                                    α ↪o β

                                                                    Embeddings of partial orders that preserve < also preserve .

                                                                    Equations
                                                                    Instances For
                                                                      @[simp]
                                                                      theorem RelEmbedding.orderEmbeddingOfLTEmbedding_apply {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] {f : (fun (x x_1 : α) => x < x_1) ↪r fun (x x_1 : β) => x < x_1} {x : α} :
                                                                      def OrderEmbedding.ltEmbedding {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) :
                                                                      (fun (x x_1 : α) => x < x_1) ↪r fun (x x_1 : β) => x < x_1

                                                                      < is preserved by order embeddings of preorders.

                                                                      Equations
                                                                      Instances For
                                                                        @[simp]
                                                                        theorem OrderEmbedding.ltEmbedding_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) (x : α) :
                                                                        @[simp]
                                                                        theorem OrderEmbedding.le_iff_le {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) {a : α} {b : α} :
                                                                        f a f b a b
                                                                        @[simp]
                                                                        theorem OrderEmbedding.lt_iff_lt {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) {a : α} {b : α} :
                                                                        f a < f b a < b
                                                                        theorem OrderEmbedding.eq_iff_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) {a : α} {b : α} :
                                                                        f a = f b a = b
                                                                        theorem OrderEmbedding.monotone {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) :
                                                                        theorem OrderEmbedding.strictMono {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) :
                                                                        theorem OrderEmbedding.acc {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) (a : α) :
                                                                        Acc (fun (x x_1 : β) => x < x_1) (f a)Acc (fun (x x_1 : α) => x < x_1) a
                                                                        theorem OrderEmbedding.wellFounded {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) :
                                                                        (WellFounded fun (x x_1 : β) => x < x_1)WellFounded fun (x x_1 : α) => x < x_1
                                                                        theorem OrderEmbedding.isWellOrder {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) [IsWellOrder β fun (x x_1 : β) => x < x_1] :
                                                                        IsWellOrder α fun (x x_1 : α) => x < x_1
                                                                        def OrderEmbedding.dual {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) :

                                                                        An order embedding is also an order embedding between dual orders.

                                                                        Equations
                                                                        Instances For
                                                                          theorem OrderEmbedding.wellFoundedLT {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) [WellFoundedLT β] :

                                                                          A preorder which embeds into a well-founded preorder is itself well-founded.

                                                                          theorem OrderEmbedding.wellFoundedGT {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) [WellFoundedGT β] :

                                                                          A preorder which embeds into a preorder in which (· > ·) is well-founded also has (· > ·) well-founded.

                                                                          @[simp]
                                                                          theorem OrderEmbedding.withBotMap_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) :
                                                                          def OrderEmbedding.withBotMap {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) :

                                                                          A version of WithBot.map for order embeddings.

                                                                          Equations
                                                                          Instances For
                                                                            @[simp]
                                                                            theorem OrderEmbedding.withTopMap_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) :
                                                                            def OrderEmbedding.withTopMap {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) :

                                                                            A version of WithTop.map for order embeddings.

                                                                            Equations
                                                                            Instances For
                                                                              def OrderEmbedding.ofMapLEIff {α : Type u_6} {β : Type u_7} [PartialOrder α] [Preorder β] (f : αβ) (hf : ∀ (a b : α), f a f b a b) :
                                                                              α ↪o β

                                                                              To define an order embedding from a partial order to a preorder it suffices to give a function together with a proof that it satisfies f a ≤ f b ↔ a ≤ b.

                                                                              Equations
                                                                              Instances For
                                                                                @[simp]
                                                                                theorem OrderEmbedding.coe_ofMapLEIff {α : Type u_6} {β : Type u_7} [PartialOrder α] [Preorder β] {f : αβ} (h : ∀ (a b : α), f a f b a b) :
                                                                                def OrderEmbedding.ofStrictMono {α : Type u_6} {β : Type u_7} [LinearOrder α] [Preorder β] (f : αβ) (h : StrictMono f) :
                                                                                α ↪o β

                                                                                A strictly monotone map from a linear order is an order embedding.

                                                                                Equations
                                                                                Instances For
                                                                                  @[simp]
                                                                                  theorem OrderEmbedding.coe_ofStrictMono {α : Type u_6} {β : Type u_7} [LinearOrder α] [Preorder β] {f : αβ} (h : StrictMono f) :
                                                                                  @[simp]
                                                                                  theorem OrderEmbedding.subtype_apply {α : Type u_2} [Preorder α] (p : αProp) :
                                                                                  (OrderEmbedding.subtype p) = Subtype.val
                                                                                  def OrderEmbedding.subtype {α : Type u_2} [Preorder α] (p : αProp) :

                                                                                  Embedding of a subtype into the ambient type as an OrderEmbedding.

                                                                                  Equations
                                                                                  Instances For
                                                                                    @[simp]
                                                                                    theorem OrderEmbedding.toOrderHom_coe {X : Type u_6} {Y : Type u_7} [Preorder X] [Preorder Y] (f : X ↪o Y) :
                                                                                    def OrderEmbedding.toOrderHom {X : Type u_6} {Y : Type u_7} [Preorder X] [Preorder Y] (f : X ↪o Y) :
                                                                                    X →o Y

                                                                                    Convert an OrderEmbedding to an OrderHom.

                                                                                    Equations
                                                                                    Instances For
                                                                                      @[simp]
                                                                                      theorem OrderEmbedding.ofIsEmpty_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [IsEmpty α] (a : α) :
                                                                                      OrderEmbedding.ofIsEmpty a = isEmptyElim a
                                                                                      def OrderEmbedding.ofIsEmpty {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [IsEmpty α] :
                                                                                      α ↪o β

                                                                                      The trivial embedding from an empty preorder to another preorder

                                                                                      Equations
                                                                                      • OrderEmbedding.ofIsEmpty = { toEmbedding := { toFun := fun (a : α) => isEmptyElim a, inj' := }, map_rel_iff' := }
                                                                                      Instances For
                                                                                        @[simp]
                                                                                        theorem OrderEmbedding.coe_ofIsEmpty {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [IsEmpty α] :
                                                                                        OrderEmbedding.ofIsEmpty = fun (a : α) => isEmptyElim a
                                                                                        @[simp]
                                                                                        theorem RelHom.toOrderHom_coe {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] (f : (fun (x x_1 : α) => x < x_1) →r fun (x x_1 : β) => x < x_1) :
                                                                                        (RelHom.toOrderHom f) = f
                                                                                        def RelHom.toOrderHom {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] (f : (fun (x x_1 : α) => x < x_1) →r fun (x x_1 : β) => x < x_1) :
                                                                                        α →o β

                                                                                        A bundled expression of the fact that a map between partial orders that is strictly monotone is weakly monotone.

                                                                                        Equations
                                                                                        Instances For
                                                                                          theorem RelEmbedding.toOrderHom_injective {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] (f : (fun (x x_1 : α) => x < x_1) ↪r fun (x x_1 : β) => x < x_1) :
                                                                                          instance OrderIso.instEquivLikeOrderIso {α : Type u_2} {β : Type u_3} [LE α] [LE β] :
                                                                                          EquivLike (α ≃o β) α β
                                                                                          Equations
                                                                                          • OrderIso.instEquivLikeOrderIso = { coe := fun (f : α ≃o β) => f.toFun, inv := fun (f : α ≃o β) => f.invFun, left_inv := , right_inv := , coe_injective' := }
                                                                                          instance OrderIso.instOrderIsoClassOrderIsoInstEquivLikeOrderIso {α : Type u_2} {β : Type u_3} [LE α] [LE β] :
                                                                                          OrderIsoClass (α ≃o β) α β
                                                                                          Equations
                                                                                          • =
                                                                                          @[simp]
                                                                                          theorem OrderIso.toFun_eq_coe {α : Type u_2} {β : Type u_3} [LE α] [LE β] {f : α ≃o β} :
                                                                                          f.toFun = f
                                                                                          theorem OrderIso.ext {α : Type u_2} {β : Type u_3} [LE α] [LE β] {f : α ≃o β} {g : α ≃o β} (h : f = g) :
                                                                                          f = g
                                                                                          def OrderIso.toOrderEmbedding {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
                                                                                          α ↪o β

                                                                                          Reinterpret an order isomorphism as an order embedding.

                                                                                          Equations
                                                                                          Instances For
                                                                                            @[simp]
                                                                                            theorem OrderIso.coe_toOrderEmbedding {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
                                                                                            theorem OrderIso.bijective {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
                                                                                            theorem OrderIso.injective {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
                                                                                            theorem OrderIso.surjective {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
                                                                                            theorem OrderIso.apply_eq_iff_eq {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x : α} {y : α} :
                                                                                            e x = e y x = y
                                                                                            def OrderIso.refl (α : Type u_6) [LE α] :
                                                                                            α ≃o α

                                                                                            Identity order isomorphism.

                                                                                            Equations
                                                                                            Instances For
                                                                                              @[simp]
                                                                                              theorem OrderIso.coe_refl {α : Type u_2} [LE α] :
                                                                                              (OrderIso.refl α) = id
                                                                                              @[simp]
                                                                                              theorem OrderIso.refl_apply {α : Type u_2} [LE α] (x : α) :
                                                                                              (OrderIso.refl α) x = x
                                                                                              @[simp]
                                                                                              theorem OrderIso.refl_toEquiv {α : Type u_2} [LE α] :
                                                                                              (OrderIso.refl α).toEquiv = Equiv.refl α
                                                                                              def OrderIso.symm {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
                                                                                              β ≃o α

                                                                                              Inverse of an order isomorphism.

                                                                                              Equations
                                                                                              Instances For
                                                                                                @[simp]
                                                                                                theorem OrderIso.apply_symm_apply {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) (x : β) :
                                                                                                e ((OrderIso.symm e) x) = x
                                                                                                @[simp]
                                                                                                theorem OrderIso.symm_apply_apply {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) (x : α) :
                                                                                                (OrderIso.symm e) (e x) = x
                                                                                                @[simp]
                                                                                                theorem OrderIso.apply_eq_iff_eq_symm_apply {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) (x : α) (y : β) :
                                                                                                e x = y x = (OrderIso.symm e) y
                                                                                                theorem OrderIso.symm_apply_eq {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x : α} {y : β} :
                                                                                                (OrderIso.symm e) y = x y = e x
                                                                                                @[simp]
                                                                                                theorem OrderIso.symm_symm {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
                                                                                                theorem OrderIso.symm_bijective {α : Type u_2} {β : Type u_3} [LE α] [LE β] :
                                                                                                Function.Bijective OrderIso.symm
                                                                                                theorem OrderIso.symm_injective {α : Type u_2} {β : Type u_3} [LE α] [LE β] :
                                                                                                Function.Injective OrderIso.symm
                                                                                                @[simp]
                                                                                                theorem OrderIso.toEquiv_symm {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
                                                                                                e.symm = (OrderIso.symm e).toEquiv
                                                                                                def OrderIso.trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [LE α] [LE β] [LE γ] (e : α ≃o β) (e' : β ≃o γ) :
                                                                                                α ≃o γ

                                                                                                Composition of two order isomorphisms is an order isomorphism.

                                                                                                Equations
                                                                                                Instances For
                                                                                                  @[simp]
                                                                                                  theorem OrderIso.coe_trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [LE α] [LE β] [LE γ] (e : α ≃o β) (e' : β ≃o γ) :
                                                                                                  (OrderIso.trans e e') = e' e
                                                                                                  @[simp]
                                                                                                  theorem OrderIso.trans_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [LE α] [LE β] [LE γ] (e : α ≃o β) (e' : β ≃o γ) (x : α) :
                                                                                                  (OrderIso.trans e e') x = e' (e x)
                                                                                                  @[simp]
                                                                                                  theorem OrderIso.refl_trans {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
                                                                                                  @[simp]
                                                                                                  theorem OrderIso.trans_refl {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
                                                                                                  @[simp]
                                                                                                  theorem OrderIso.symm_trans_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [LE α] [LE β] [LE γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) (c : γ) :
                                                                                                  (OrderIso.symm (OrderIso.trans e₁ e₂)) c = (OrderIso.symm e₁) ((OrderIso.symm e₂) c)
                                                                                                  theorem OrderIso.symm_trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [LE α] [LE β] [LE γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) :
                                                                                                  def OrderIso.prodComm {α : Type u_2} {β : Type u_3} [LE α] [LE β] :
                                                                                                  α × β ≃o β × α

                                                                                                  Prod.swap as an OrderIso.

                                                                                                  Equations
                                                                                                  • OrderIso.prodComm = { toEquiv := Equiv.prodComm α β, map_rel_iff' := }
                                                                                                  Instances For
                                                                                                    @[simp]
                                                                                                    theorem OrderIso.coe_prodComm {α : Type u_2} {β : Type u_3} [LE α] [LE β] :
                                                                                                    OrderIso.prodComm = Prod.swap
                                                                                                    @[simp]
                                                                                                    theorem OrderIso.prodComm_symm {α : Type u_2} {β : Type u_3} [LE α] [LE β] :
                                                                                                    OrderIso.symm OrderIso.prodComm = OrderIso.prodComm
                                                                                                    def OrderIso.dualDual (α : Type u_2) [LE α] :

                                                                                                    The order isomorphism between a type and its double dual.

                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      @[simp]
                                                                                                      theorem OrderIso.coe_dualDual (α : Type u_2) [LE α] :
                                                                                                      (OrderIso.dualDual α) = OrderDual.toDual OrderDual.toDual
                                                                                                      @[simp]
                                                                                                      theorem OrderIso.coe_dualDual_symm (α : Type u_2) [LE α] :
                                                                                                      (OrderIso.symm (OrderIso.dualDual α)) = OrderDual.ofDual OrderDual.ofDual
                                                                                                      @[simp]
                                                                                                      theorem OrderIso.dualDual_apply {α : Type u_2} [LE α] (a : α) :
                                                                                                      (OrderIso.dualDual α) a = OrderDual.toDual (OrderDual.toDual a)
                                                                                                      @[simp]
                                                                                                      theorem OrderIso.dualDual_symm_apply {α : Type u_2} [LE α] (a : αᵒᵈᵒᵈ) :
                                                                                                      (OrderIso.symm (OrderIso.dualDual α)) a = OrderDual.ofDual (OrderDual.ofDual a)
                                                                                                      theorem OrderIso.le_iff_le {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x : α} {y : α} :
                                                                                                      e x e y x y
                                                                                                      theorem OrderIso.le_symm_apply {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x : α} {y : β} :
                                                                                                      x (OrderIso.symm e) y e x y
                                                                                                      theorem OrderIso.symm_apply_le {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x : α} {y : β} :
                                                                                                      (OrderIso.symm e) y x y e x
                                                                                                      theorem OrderIso.monotone {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) :
                                                                                                      theorem OrderIso.strictMono {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) :
                                                                                                      @[simp]
                                                                                                      theorem OrderIso.lt_iff_lt {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) {x : α} {y : α} :
                                                                                                      e x < e y x < y
                                                                                                      def OrderIso.toRelIsoLT {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) :
                                                                                                      (fun (x x_1 : α) => x < x_1) ≃r fun (x x_1 : β) => x < x_1

                                                                                                      Converts an OrderIso into a RelIso (<) (<).

                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        @[simp]
                                                                                                        theorem OrderIso.toRelIsoLT_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) (x : α) :
                                                                                                        def OrderIso.ofRelIsoLT {α : Type u_6} {β : Type u_7} [PartialOrder α] [PartialOrder β] (e : (fun (x x_1 : α) => x < x_1) ≃r fun (x x_1 : β) => x < x_1) :
                                                                                                        α ≃o β

                                                                                                        Converts a RelIso (<) (<) into an OrderIso.

                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          @[simp]
                                                                                                          theorem OrderIso.ofRelIsoLT_apply {α : Type u_6} {β : Type u_7} [PartialOrder α] [PartialOrder β] (e : (fun (x x_1 : α) => x < x_1) ≃r fun (x x_1 : β) => x < x_1) (x : α) :
                                                                                                          @[simp]
                                                                                                          theorem OrderIso.ofRelIsoLT_symm {α : Type u_6} {β : Type u_7} [PartialOrder α] [PartialOrder β] (e : (fun (x x_1 : α) => x < x_1) ≃r fun (x x_1 : β) => x < x_1) :
                                                                                                          @[simp]
                                                                                                          @[simp]
                                                                                                          theorem OrderIso.toRelIsoLT_ofRelIsoLT {α : Type u_6} {β : Type u_7} [PartialOrder α] [PartialOrder β] (e : (fun (x x_1 : α) => x < x_1) ≃r fun (x x_1 : β) => x < x_1) :
                                                                                                          def OrderIso.ofCmpEqCmp {α : Type u_6} {β : Type u_7} [LinearOrder α] [LinearOrder β] (f : αβ) (g : βα) (h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b) :
                                                                                                          α ≃o β

                                                                                                          To show that f : α → β, g : β → α make up an order isomorphism of linear orders, it suffices to prove cmp a (g b) = cmp (f a) b.

                                                                                                          Equations
                                                                                                          • OrderIso.ofCmpEqCmp f g h = let_fun gf := ; { toEquiv := { toFun := f, invFun := g, left_inv := , right_inv := }, map_rel_iff' := }
                                                                                                          Instances For
                                                                                                            def OrderIso.ofHomInv {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {F : Type u_6} {G : Type u_7} [FunLike F α β] [OrderHomClass F α β] [FunLike G β α] [OrderHomClass G β α] (f : F) (g : G) (h₁ : OrderHom.comp f g = OrderHom.id) (h₂ : OrderHom.comp g f = OrderHom.id) :
                                                                                                            α ≃o β

                                                                                                            To show that f : α →o β and g : β →o α make up an order isomorphism it is enough to show that g is the inverse of f

                                                                                                            Equations
                                                                                                            • OrderIso.ofHomInv f g h₁ h₂ = { toEquiv := { toFun := f, invFun := g, left_inv := , right_inv := }, map_rel_iff' := }
                                                                                                            Instances For
                                                                                                              @[simp]
                                                                                                              theorem OrderIso.funUnique_toEquiv (α : Type u_6) (β : Type u_7) [Unique α] [Preorder β] :
                                                                                                              (OrderIso.funUnique α β).toEquiv = Equiv.funUnique α β
                                                                                                              @[simp]
                                                                                                              theorem OrderIso.funUnique_apply (α : Type u_6) (β : Type u_7) [Unique α] [Preorder β] (f : (i : α) → (fun (a : α) => β) i) :
                                                                                                              (OrderIso.funUnique α β) f = f default
                                                                                                              def OrderIso.funUnique (α : Type u_6) (β : Type u_7) [Unique α] [Preorder β] :
                                                                                                              (αβ) ≃o β

                                                                                                              Order isomorphism between α → β and β, where α has a unique element.

                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                @[simp]
                                                                                                                theorem OrderIso.funUnique_symm_apply {α : Type u_6} {β : Type u_7} [Unique α] [Preorder β] :
                                                                                                                def Equiv.toOrderIso {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α β) (h₁ : Monotone e) (h₂ : Monotone e.symm) :
                                                                                                                α ≃o β

                                                                                                                If e is an equivalence with monotone forward and inverse maps, then e is an order isomorphism.

                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  @[simp]
                                                                                                                  theorem Equiv.coe_toOrderIso {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α β) (h₁ : Monotone e) (h₂ : Monotone e.symm) :
                                                                                                                  (Equiv.toOrderIso e h₁ h₂) = e
                                                                                                                  @[simp]
                                                                                                                  theorem Equiv.toOrderIso_toEquiv {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α β) (h₁ : Monotone e) (h₂ : Monotone e.symm) :
                                                                                                                  (Equiv.toOrderIso e h₁ h₂).toEquiv = e
                                                                                                                  @[simp]
                                                                                                                  theorem StrictMono.orderIsoOfRightInverse_symm_apply {α : Type u_2} {β : Type u_3} [LinearOrder α] [Preorder β] (f : αβ) (h_mono : StrictMono f) (g : βα) (hg : Function.RightInverse g f) :
                                                                                                                  @[simp]
                                                                                                                  theorem StrictMono.orderIsoOfRightInverse_apply {α : Type u_2} {β : Type u_3} [LinearOrder α] [Preorder β] (f : αβ) (h_mono : StrictMono f) (g : βα) (hg : Function.RightInverse g f) :
                                                                                                                  def StrictMono.orderIsoOfRightInverse {α : Type u_2} {β : Type u_3} [LinearOrder α] [Preorder β] (f : αβ) (h_mono : StrictMono f) (g : βα) (hg : Function.RightInverse g f) :
                                                                                                                  α ≃o β

                                                                                                                  A strictly monotone function with a right inverse is an order isomorphism.

                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    def OrderIso.dual {α : Type u_2} {β : Type u_3} [LE α] [LE β] (f : α ≃o β) :

                                                                                                                    An order isomorphism is also an order isomorphism between dual orders.

                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      theorem OrderIso.map_bot' {α : Type u_2} {β : Type u_3} [LE α] [PartialOrder β] (f : α ≃o β) {x : α} {y : β} (hx : ∀ (x' : α), x x') (hy : ∀ (y' : β), y y') :
                                                                                                                      f x = y
                                                                                                                      theorem OrderIso.map_bot {α : Type u_2} {β : Type u_3} [LE α] [PartialOrder β] [OrderBot α] [OrderBot β] (f : α ≃o β) :
                                                                                                                      theorem OrderIso.map_top' {α : Type u_2} {β : Type u_3} [LE α] [PartialOrder β] (f : α ≃o β) {x : α} {y : β} (hx : ∀ (x' : α), x' x) (hy : ∀ (y' : β), y' y) :
                                                                                                                      f x = y
                                                                                                                      theorem OrderIso.map_top {α : Type u_2} {β : Type u_3} [LE α] [PartialOrder β] [OrderTop α] [OrderTop β] (f : α ≃o β) :
                                                                                                                      theorem OrderEmbedding.map_inf_le {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [SemilatticeInf β] (f : α ↪o β) (x : α) (y : α) :
                                                                                                                      f (x y) f x f y
                                                                                                                      theorem OrderEmbedding.le_map_sup {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [SemilatticeSup β] (f : α ↪o β) (x : α) (y : α) :
                                                                                                                      f x f y f (x y)
                                                                                                                      theorem OrderIso.map_inf {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [SemilatticeInf β] (f : α ≃o β) (x : α) (y : α) :
                                                                                                                      f (x y) = f x f y
                                                                                                                      theorem OrderIso.map_sup {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [SemilatticeSup β] (f : α ≃o β) (x : α) (y : α) :
                                                                                                                      f (x y) = f x f y
                                                                                                                      theorem Disjoint.map_orderIso {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderBot α] [SemilatticeInf β] [OrderBot β] {a : α} {b : α} (f : α ≃o β) (ha : Disjoint a b) :
                                                                                                                      Disjoint (f a) (f b)

                                                                                                                      Note that this goal could also be stated (Disjoint on f) a b

                                                                                                                      theorem Codisjoint.map_orderIso {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderTop α] [SemilatticeSup β] [OrderTop β] {a : α} {b : α} (f : α ≃o β) (ha : Codisjoint a b) :
                                                                                                                      Codisjoint (f a) (f b)

                                                                                                                      Note that this goal could also be stated (Codisjoint on f) a b

                                                                                                                      @[simp]
                                                                                                                      theorem disjoint_map_orderIso_iff {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderBot α] [SemilatticeInf β] [OrderBot β] {a : α} {b : α} (f : α ≃o β) :
                                                                                                                      Disjoint (f a) (f b) Disjoint a b
                                                                                                                      @[simp]
                                                                                                                      theorem codisjoint_map_orderIso_iff {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderTop α] [SemilatticeSup β] [OrderTop β] {a : α} {b : α} (f : α ≃o β) :
                                                                                                                      Codisjoint (f a) (f b) Codisjoint a b

                                                                                                                      Taking the dual then adding is the same as adding then taking the dual. This is the order iso form of WithBot.ofDual, as proven by coe_toDualTopEquiv_eq.

                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        @[simp]
                                                                                                                        theorem WithBot.toDualTopEquiv_coe {α : Type u_2} [LE α] (a : α) :
                                                                                                                        WithBot.toDualTopEquiv (OrderDual.toDual a) = OrderDual.toDual a
                                                                                                                        @[simp]
                                                                                                                        theorem WithBot.toDualTopEquiv_symm_coe {α : Type u_2} [LE α] (a : α) :
                                                                                                                        (OrderIso.symm WithBot.toDualTopEquiv) (OrderDual.toDual a) = (OrderDual.toDual a)
                                                                                                                        @[simp]
                                                                                                                        theorem WithBot.toDualTopEquiv_bot {α : Type u_2} [LE α] :
                                                                                                                        WithBot.toDualTopEquiv =
                                                                                                                        @[simp]
                                                                                                                        theorem WithBot.toDualTopEquiv_symm_bot {α : Type u_2} [LE α] :
                                                                                                                        (OrderIso.symm WithBot.toDualTopEquiv) =
                                                                                                                        theorem WithBot.coe_toDualTopEquiv_eq {α : Type u_2} [LE α] :
                                                                                                                        WithBot.toDualTopEquiv = OrderDual.toDual WithBot.ofDual

                                                                                                                        Taking the dual then adding is the same as adding then taking the dual. This is the order iso form of WithTop.ofDual, as proven by coe_toDualBotEquiv_eq.

                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          @[simp]
                                                                                                                          theorem WithTop.toDualBotEquiv_coe {α : Type u_2} [LE α] (a : α) :
                                                                                                                          WithTop.toDualBotEquiv (OrderDual.toDual a) = OrderDual.toDual a
                                                                                                                          @[simp]
                                                                                                                          theorem WithTop.toDualBotEquiv_symm_coe {α : Type u_2} [LE α] (a : α) :
                                                                                                                          (OrderIso.symm WithTop.toDualBotEquiv) (OrderDual.toDual a) = (OrderDual.toDual a)
                                                                                                                          @[simp]
                                                                                                                          theorem WithTop.toDualBotEquiv_top {α : Type u_2} [LE α] :
                                                                                                                          WithTop.toDualBotEquiv =
                                                                                                                          @[simp]
                                                                                                                          theorem WithTop.toDualBotEquiv_symm_top {α : Type u_2} [LE α] :
                                                                                                                          (OrderIso.symm WithTop.toDualBotEquiv) =
                                                                                                                          theorem WithTop.coe_toDualBotEquiv {α : Type u_2} [LE α] :
                                                                                                                          WithTop.toDualBotEquiv = OrderDual.toDual WithTop.ofDual
                                                                                                                          @[simp]
                                                                                                                          theorem OrderIso.withTopCongr_apply {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] (e : α ≃o β) :
                                                                                                                          ∀ (a : Option α), (OrderIso.withTopCongr e) a = Option.map (e) a
                                                                                                                          def OrderIso.withTopCongr {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] (e : α ≃o β) :

                                                                                                                          A version of Equiv.optionCongr for WithTop.

                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            @[simp]
                                                                                                                            theorem OrderIso.withTopCongr_trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [PartialOrder α] [PartialOrder β] [PartialOrder γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) :
                                                                                                                            @[simp]
                                                                                                                            theorem OrderIso.withBotCongr_apply {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] (e : α ≃o β) :
                                                                                                                            ∀ (a : Option α), (OrderIso.withBotCongr e) a = Option.map (e) a
                                                                                                                            def OrderIso.withBotCongr {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] (e : α ≃o β) :

                                                                                                                            A version of Equiv.optionCongr for WithBot.

                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              @[simp]
                                                                                                                              theorem OrderIso.withBotCongr_trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [PartialOrder α] [PartialOrder β] [PartialOrder γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) :
                                                                                                                              theorem OrderIso.isCompl {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : α ≃o β) {x : α} {y : α} (h : IsCompl x y) :
                                                                                                                              IsCompl (f x) (f y)
                                                                                                                              theorem OrderIso.isCompl_iff {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : α ≃o β) {x : α} {y : α} :
                                                                                                                              IsCompl x y IsCompl (f x) (f y)