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
    theorem OrderHom.monotone' {α : Type u_6} {β : Type u_7} [Preorder α] [Preorder β] (self : α →o β) :
    Monotone self.toFun

    The underlying function of an OrderHom is monotone.

    @[reducible, inline]
    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 (x1 x2 : α) => x1 x2) ↪r fun (x1 x2 : β) => x1 x2)
    Instances For
      @[reducible, inline]
      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 (x1 x2 : α) => x1 x2) ≃r fun (x1 x2 : β) => x1 x2)
      Instances For
        @[reducible, inline]
        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) (α : outParam (Type u_7)) (β : outParam (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
            @[simp]
            theorem OrderIsoClass.map_le_map_iff {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} :
            ∀ {inst : LE α} {inst_1 : LE β} {inst_2 : EquivLike F α β} [self : OrderIsoClass F α β] (f : F) {a b : α}, f a f b a b

            An order isomorphism respects .

            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 = { toEquiv := f, map_rel_iff' := }
            Instances For
              instance instCoeTCOrderIsoOfOrderIsoClass {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
              • instCoeTCOrderIsoOfOrderIsoClass = { coe := OrderIsoClass.toOrderIso }
              @[instance 100]
              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) :
              theorem OrderHomClass.GCongr.mono {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [FunLike F α β] [OrderHomClass F α β] (f : F) {a : α} {b : α} (hab : a b) :
              f a f b
              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
                theorem map_inv_le_map_inv_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [LE β] [EquivLike F α β] [OrderIsoClass F α β] (f : F) {a : β} {b : β} :
                @[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
                theorem map_inv_lt_map_inv_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [EquivLike F α β] [OrderIsoClass F α β] (f : F) {a : β} {b : β} :
                @[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.instFunLike {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] :
                FunLike (α →o β) α β
                Equations
                • OrderHom.instFunLike = { coe := OrderHom.toFun, coe_injective' := }
                instance OrderHom.instOrderHomClass {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] :
                OrderHomClass (α →o β) α β
                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_iff {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {f : α →o β} {g : α →o β} :
                  f = g f = g
                  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
                  • f.copy f' h = { toFun := f', monotone' := }
                  Instances For
                    @[simp]
                    theorem OrderHom.coe_copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) (f' : αβ) (h : f' = f) :
                    (f.copy f' h) = f'
                    theorem OrderHom.copy_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) (f' : αβ) (h : f' = f) :
                    f.copy 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.instInhabited {α : Type u_2} [Preorder α] :
                      Inhabited (α →o α)
                      Equations
                      • OrderHom.instInhabited = { default := OrderHom.id }
                      instance OrderHom.instPreorder {α : 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
                      instance OrderHom.instPartialOrder {α : Type u_2} [Preorder α] {β : Type u_6} [PartialOrder β] :
                      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 β) :
                        (g.comp 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
                        • g.comp f = { toFun := g f, monotone' := }
                        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₂) :
                          g₁.comp f₁ g₂.comp f₂
                          @[simp]
                          theorem OrderHom.mk_comp_mk {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (g : βγ) (f : αβ) (hg : Monotone g) (hf : Monotone f) :
                          { toFun := g, monotone' := hg }.comp { toFun := f, monotone' := hf } = { toFun := g f, monotone' := }
                          @[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 β)) => f.1.comp f.2, monotone' := }
                          Instances For
                            @[simp]
                            theorem OrderHom.comp_id {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :
                            f.comp OrderHom.id = f
                            @[simp]
                            theorem OrderHom.id_comp {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :
                            OrderHom.id.comp 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 : γ) :
                              ((OrderHom.const β) c).comp f = (OrderHom.const α) c
                              @[simp]
                              theorem OrderHom.comp_const {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (γ : Type u_6) [Preorder γ] (f : α →o β) (c : α) :
                              f.comp ((OrderHom.const γ) c) = (OrderHom.const γ) (f c)
                              @[simp]
                              theorem OrderHom.prod_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : α →o β) (g : α →o γ) (x : α) :
                              (f.prod 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
                              • f.prod 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₂) :
                                f₁.prod g₁ f₂.prod 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 β) :
                                (f₁.comp g).prod (f₂.comp g) = (f₁.prod f₂).comp g
                                @[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 γ)) => f.1.prod 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
                                  • OrderHom.diag = OrderHom.id.prod OrderHom.id
                                  Instances For
                                    @[simp]
                                    theorem OrderHom.onDiag_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o α →o β) :
                                    ∀ (a : α), f.onDiag 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
                                    • f.onDiag = ((RelIso.symm OrderHom.curry) f).comp OrderHom.diag
                                    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.fst.prod 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.fst.comp (f.prod 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.snd.comp (f.prod g) = g
                                          @[simp]
                                          theorem OrderHom.prodIso_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : α →o β × γ) :
                                          OrderHom.prodIso f = (OrderHom.fst.comp f, OrderHom.snd.comp f)
                                          @[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 = f.1.prod f.2
                                          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 : α × γ), (f.prodMap 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
                                            • f.prodMap g = { toFun := Prod.map f g, monotone' := }
                                            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_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
                                                      @[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 = (Pi.evalOrderHom i).comp 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
                                                      • OrderHom.piIso = { toFun := fun (f : α →o (i : ι) → π i) (i : ι) => (Pi.evalOrderHom i).comp f, invFun := OrderHom.pi, left_inv := , right_inv := , map_rel_iff' := }
                                                      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 : α // p 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 = { default := OrderHom.id, uniq := }
                                                            theorem OrderHom.orderHom_eq_id {α : Type u_2} [Preorder α] [Subsingleton α] (g : α →o α) :
                                                            g = OrderHom.id
                                                            @[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
                                                            @[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
                                                            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 (g.comp f) = (OrderHom.dual g).comp (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 (g.comp f) = (OrderHom.dual.symm g).comp (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 β) :
                                                                f.withBotMap = WithBot.map f
                                                                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
                                                                • f.withBotMap = { toFun := WithBot.map f, monotone' := }
                                                                Instances For
                                                                  @[simp]
                                                                  theorem OrderHom.withTopMap_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :
                                                                  f.withTopMap = WithTop.map f
                                                                  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
                                                                  • f.withTopMap = { toFun := WithTop.map f, monotone' := }
                                                                  Instances For
                                                                    def RelEmbedding.orderEmbeddingOfLTEmbedding {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] (f : (fun (x1 x2 : α) => x1 < x2) ↪r fun (x1 x2 : β) => x1 < x2) :
                                                                    α ↪o β

                                                                    Embeddings of partial orders that preserve < also preserve .

                                                                    Equations
                                                                    • f.orderEmbeddingOfLTEmbedding = { toEmbedding := f.toEmbedding, map_rel_iff' := }
                                                                    Instances For
                                                                      @[simp]
                                                                      theorem RelEmbedding.orderEmbeddingOfLTEmbedding_apply {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] {f : (fun (x1 x2 : α) => x1 < x2) ↪r fun (x1 x2 : β) => x1 < x2} {x : α} :
                                                                      f.orderEmbeddingOfLTEmbedding x = f x
                                                                      def OrderEmbedding.ltEmbedding {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) :
                                                                      (fun (x1 x2 : α) => x1 < x2) ↪r fun (x1 x2 : β) => x1 < x2

                                                                      < is preserved by order embeddings of preorders.

                                                                      Equations
                                                                      • f.ltEmbedding = { toEmbedding := f.toEmbedding, map_rel_iff' := }
                                                                      Instances For
                                                                        @[simp]
                                                                        theorem OrderEmbedding.ltEmbedding_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) (x : α) :
                                                                        f.ltEmbedding x = f 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 (x1 x2 : β) => x1 < x2) (f a)Acc (fun (x1 x2 : α) => x1 < x2) a
                                                                        theorem OrderEmbedding.wellFounded {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) :
                                                                        (WellFounded fun (x1 x2 : β) => x1 < x2)WellFounded fun (x1 x2 : α) => x1 < x2
                                                                        theorem OrderEmbedding.isWellOrder {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [IsWellOrder β fun (x1 x2 : β) => x1 < x2] (f : α ↪o β) :
                                                                        IsWellOrder α fun (x1 x2 : α) => x1 < x2
                                                                        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
                                                                        • f.dual = { toEmbedding := f.toEmbedding, map_rel_iff' := }
                                                                        Instances For
                                                                          theorem OrderEmbedding.wellFoundedLT {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [WellFoundedLT β] (f : α ↪o β) :

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

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

                                                                          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 β) :
                                                                          f.withBotMap = WithBot.map f
                                                                          def OrderEmbedding.withBotMap {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) :

                                                                          A version of WithBot.map for order embeddings.

                                                                          Equations
                                                                          • f.withBotMap = { toFun := WithBot.map f, inj' := , map_rel_iff' := }
                                                                          Instances For
                                                                            @[simp]
                                                                            theorem OrderEmbedding.withTopMap_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) :
                                                                            f.withTopMap = WithTop.map f
                                                                            def OrderEmbedding.withTopMap {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) :

                                                                            A version of WithTop.map for order embeddings.

                                                                            Equations
                                                                            • f.withTopMap = { toFun := WithTop.map f, inj' := , map_rel_iff' := }
                                                                            Instances For
                                                                              @[simp]
                                                                              theorem OrderEmbedding.withBotCoe_apply {α : Type u_2} [Preorder α] :
                                                                              OrderEmbedding.withBotCoe = WithBot.some

                                                                              Coercion α → WithBot α as an OrderEmbedding.

                                                                              Equations
                                                                              • OrderEmbedding.withBotCoe = { toFun := WithBot.some, inj' := , map_rel_iff' := }
                                                                              Instances For
                                                                                @[simp]
                                                                                theorem OrderEmbedding.withTopCoe_apply {α : Type u_2} [Preorder α] :
                                                                                OrderEmbedding.withTopCoe = WithTop.some

                                                                                Coercion α → WithTop α as an OrderEmbedding.

                                                                                Equations
                                                                                • OrderEmbedding.withTopCoe = { toFun := WithTop.some, inj' := , map_rel_iff' := }
                                                                                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) :
                                                                                        f.toOrderHom = f
                                                                                        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
                                                                                        • f.toOrderHom = { toFun := f, monotone' := }
                                                                                        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 = { 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
                                                                                            theorem Disjoint.of_orderEmbedding {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] (f : α ↪o β) [OrderBot α] [OrderBot β] {a₁ : α} {a₂ : α} :
                                                                                            Disjoint (f a₁) (f a₂)Disjoint a₁ a₂

                                                                                            If the images by an order embedding of two elements are disjoint, then they are themselves disjoint.

                                                                                            theorem Codisjoint.of_orderEmbedding {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] (f : α ↪o β) [OrderTop α] [OrderTop β] {a₁ : α} {a₂ : α} :
                                                                                            Codisjoint (f a₁) (f a₂)Codisjoint a₁ a₂

                                                                                            If the images by an order embedding of two elements are codisjoint, then they are themselves codisjoint.

                                                                                            theorem IsCompl.of_orderEmbedding {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] (f : α ↪o β) [BoundedOrder α] [BoundedOrder β] {a₁ : α} {a₂ : α} :
                                                                                            IsCompl (f a₁) (f a₂)IsCompl a₁ a₂

                                                                                            If the images by an order embedding of two elements are complements, then they are themselves complements.

                                                                                            @[simp]
                                                                                            theorem RelHom.toOrderHom_coe {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] (f : (fun (x1 x2 : α) => x1 < x2) →r fun (x1 x2 : β) => x1 < x2) :
                                                                                            f.toOrderHom = f
                                                                                            def RelHom.toOrderHom {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] (f : (fun (x1 x2 : α) => x1 < x2) →r fun (x1 x2 : β) => x1 < x2) :
                                                                                            α →o β

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

                                                                                            Equations
                                                                                            • f.toOrderHom = { toFun := f, monotone' := }
                                                                                            Instances For
                                                                                              theorem RelEmbedding.toOrderHom_injective {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] (f : (fun (x1 x2 : α) => x1 < x2) ↪r fun (x1 x2 : β) => x1 < x2) :
                                                                                              Function.Injective f.toRelHom.toOrderHom
                                                                                              instance OrderIso.instEquivLike {α : Type u_2} {β : Type u_3} [LE α] [LE β] :
                                                                                              EquivLike (α ≃o β) α β
                                                                                              Equations
                                                                                              • OrderIso.instEquivLike = { coe := fun (f : α ≃o β) => f.toFun, inv := fun (f : α ≃o β) => f.invFun, left_inv := , right_inv := , coe_injective' := }
                                                                                              instance OrderIso.instOrderIsoClass {α : 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_iff {α : Type u_2} {β : Type u_3} [LE α] [LE β] {f : α ≃o β} {g : α ≃o β} :
                                                                                              f = g f = g
                                                                                              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 β) :
                                                                                                e.toOrderEmbedding = e
                                                                                                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 (e.symm x) = x
                                                                                                    @[simp]
                                                                                                    theorem OrderIso.symm_apply_apply {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) (x : α) :
                                                                                                    e.symm (e x) = x
                                                                                                    @[simp]
                                                                                                    theorem OrderIso.symm_refl (α : Type u_6) [LE α] :
                                                                                                    theorem OrderIso.apply_eq_iff_eq_symm_apply {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) (x : α) (y : β) :
                                                                                                    e x = y x = e.symm y
                                                                                                    theorem OrderIso.symm_apply_eq {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x : α} {y : β} :
                                                                                                    e.symm y = x y = e x
                                                                                                    @[simp]
                                                                                                    theorem OrderIso.symm_symm {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
                                                                                                    e.symm.symm = e
                                                                                                    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 = e.symm.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 γ) :
                                                                                                      (e.trans 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 : α) :
                                                                                                      (e.trans e') x = e' (e x)
                                                                                                      @[simp]
                                                                                                      theorem OrderIso.refl_trans {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
                                                                                                      (OrderIso.refl α).trans e = e
                                                                                                      @[simp]
                                                                                                      theorem OrderIso.trans_refl {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
                                                                                                      e.trans (OrderIso.refl β) = e
                                                                                                      @[simp]
                                                                                                      theorem OrderIso.symm_trans_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [LE α] [LE β] [LE γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) (c : γ) :
                                                                                                      (e₁.trans e₂).symm c = e₁.symm (e₂.symm c)
                                                                                                      theorem OrderIso.symm_trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [LE α] [LE β] [LE γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) :
                                                                                                      (e₁.trans e₂).symm = e₂.symm.trans e₁.symm
                                                                                                      @[simp]
                                                                                                      theorem OrderIso.self_trans_symm {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
                                                                                                      e.trans e.symm = OrderIso.refl α
                                                                                                      @[simp]
                                                                                                      theorem OrderIso.symm_trans_self {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
                                                                                                      e.symm.trans e = OrderIso.refl β
                                                                                                      @[simp]
                                                                                                      theorem OrderIso.arrowCongr_symm_apply {α : Type u_6} {β : Type u_7} {γ : Type u_8} {δ : Type u_9} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] (f : α ≃o γ) (g : β ≃o δ) (p : γ →o δ) :
                                                                                                      (RelIso.symm (f.arrowCongr g)) p = (↑g.symm).comp (p.comp f)
                                                                                                      @[simp]
                                                                                                      theorem OrderIso.arrowCongr_apply {α : Type u_6} {β : Type u_7} {γ : Type u_8} {δ : Type u_9} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] (f : α ≃o γ) (g : β ≃o δ) (p : α →o β) :
                                                                                                      (f.arrowCongr g) p = (↑g).comp (p.comp f.symm)
                                                                                                      def OrderIso.arrowCongr {α : Type u_6} {β : Type u_7} {γ : Type u_8} {δ : Type u_9} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] (f : α ≃o γ) (g : β ≃o δ) :
                                                                                                      (α →o β) ≃o (γ →o δ)

                                                                                                      An order isomorphism between the domains and codomains of two prosets of order homomorphisms gives an order isomorphism between the two function prosets.

                                                                                                      Equations
                                                                                                      • f.arrowCongr g = { toFun := fun (p : α →o β) => (↑g).comp (p.comp f.symm), invFun := fun (p : γ →o δ) => (↑g.symm).comp (p.comp f), left_inv := , right_inv := , map_rel_iff' := }
                                                                                                      Instances For
                                                                                                        @[simp]
                                                                                                        theorem OrderIso.conj_apply {α : Type u_6} {β : Type u_7} [Preorder α] [Preorder β] (f : α ≃o β) (a : α →o α) :
                                                                                                        f.conj a = (↑f).comp (a.comp f.symm)
                                                                                                        @[simp]
                                                                                                        theorem OrderIso.conj_symm_apply {α : Type u_6} {β : Type u_7} [Preorder α] [Preorder β] (f : α ≃o β) :
                                                                                                        ∀ (a : β →o β), f.conj.symm a = EquivLike.inv (f.arrowCongr f) a
                                                                                                        def OrderIso.conj {α : Type u_6} {β : Type u_7} [Preorder α] [Preorder β] (f : α ≃o β) :
                                                                                                        (α →o α) (β →o β)

                                                                                                        If α and β are order-isomorphic then the two orders of order-homomorphisms from α and β to themselves are order-isomorphic.

                                                                                                        Equations
                                                                                                        • f.conj = (f.arrowCongr f)
                                                                                                        Instances For
                                                                                                          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.prodComm.symm = 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.dualDual α).symm = 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.dualDual α).symm 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.GCongr.orderIso_apply_le_apply {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x : α} {y : α} :
                                                                                                              x ye x e y

                                                                                                              Alias of the reverse direction of OrderIso.le_iff_le.

                                                                                                              theorem OrderIso.le_symm_apply {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x : α} {y : β} :
                                                                                                              x e.symm y e x y
                                                                                                              theorem OrderIso.symm_apply_le {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x : α} {y : β} :
                                                                                                              e.symm 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
                                                                                                              theorem OrderIso.GCongr.orderIso_apply_lt_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) {x : α} {y : α} :
                                                                                                              x < ye x < e y

                                                                                                              Alias of the reverse direction of OrderIso.lt_iff_lt.

                                                                                                              def OrderIso.toRelIsoLT {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) :
                                                                                                              (fun (x1 x2 : α) => x1 < x2) ≃r fun (x1 x2 : β) => x1 < x2

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

                                                                                                              Equations
                                                                                                              • e.toRelIsoLT = { toEquiv := e.toEquiv, map_rel_iff' := }
                                                                                                              Instances For
                                                                                                                @[simp]
                                                                                                                theorem OrderIso.toRelIsoLT_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) (x : α) :
                                                                                                                e.toRelIsoLT x = e x
                                                                                                                @[simp]
                                                                                                                theorem OrderIso.toRelIsoLT_symm {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) :
                                                                                                                e.toRelIsoLT.symm = e.symm.toRelIsoLT
                                                                                                                def OrderIso.ofRelIsoLT {α : Type u_6} {β : Type u_7} [PartialOrder α] [PartialOrder β] (e : (fun (x1 x2 : α) => x1 < x2) ≃r fun (x1 x2 : β) => x1 < x2) :
                                                                                                                α ≃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 (x1 x2 : α) => x1 < x2) ≃r fun (x1 x2 : β) => x1 < x2) (x : α) :
                                                                                                                  @[simp]
                                                                                                                  theorem OrderIso.ofRelIsoLT_symm {α : Type u_6} {β : Type u_7} [PartialOrder α] [PartialOrder β] (e : (fun (x1 x2 : α) => x1 < x2) ≃r fun (x1 x2 : β) => x1 < x2) :
                                                                                                                  @[simp]
                                                                                                                  theorem OrderIso.ofRelIsoLT_toRelIsoLT {α : Type u_6} {β : Type u_7} [PartialOrder α] [PartialOrder β] (e : α ≃o β) :
                                                                                                                  OrderIso.ofRelIsoLT e.toRelIsoLT = e
                                                                                                                  @[simp]
                                                                                                                  theorem OrderIso.toRelIsoLT_ofRelIsoLT {α : Type u_6} {β : Type u_7} [PartialOrder α] [PartialOrder β] (e : (fun (x1 x2 : α) => x1 < x2) ≃r fun (x1 x2 : β) => x1 < x2) :
                                                                                                                  (OrderIso.ofRelIsoLT e).toRelIsoLT = e
                                                                                                                  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 = { 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₁ : (↑f).comp g = OrderHom.id) (h₂ : (↑g).comp 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₂ = { toFun := f, invFun := g, left_inv := , right_inv := , map_rel_iff' := }
                                                                                                                    Instances For
                                                                                                                      @[simp]
                                                                                                                      theorem OrderIso.funUnique_apply (α : Type u_6) (β : Type u_7) [Unique α] [Preorder β] (f : (i : α) → (fun (a : α) => β) i) :
                                                                                                                      (OrderIso.funUnique α β) f = f default
                                                                                                                      @[simp]
                                                                                                                      theorem OrderIso.funUnique_toEquiv (α : Type u_6) (β : Type u_7) [Unique α] [Preorder β] :
                                                                                                                      (OrderIso.funUnique α β).toEquiv = Equiv.funUnique α β
                                                                                                                      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
                                                                                                                        • e.toOrderIso h₁ h₂ = { toEquiv := e, map_rel_iff' := }
                                                                                                                        Instances For
                                                                                                                          @[simp]
                                                                                                                          theorem Equiv.coe_toOrderIso {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α β) (h₁ : Monotone e) (h₂ : Monotone e.symm) :
                                                                                                                          (e.toOrderIso h₁ h₂) = e
                                                                                                                          @[simp]
                                                                                                                          theorem Equiv.toOrderIso_toEquiv {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α β) (h₁ : Monotone e) (h₂ : Monotone e.symm) :
                                                                                                                          (e.toOrderIso 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
                                                                                                                            • f.dual = { toEquiv := f.toEquiv, map_rel_iff' := }
                                                                                                                            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 OrderIso.isMax_apply {α : Type u_6} {β : Type u_7} [Preorder α] [Preorder β] (f : α ≃o β) {x : α} :
                                                                                                                              IsMax (f x) IsMax x
                                                                                                                              theorem OrderIso.isMin_apply {α : Type u_6} {β : Type u_7} [Preorder α] [Preorder β] (f : α ≃o β) {x : α} :
                                                                                                                              IsMin (f x) IsMin x
                                                                                                                              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 : α) :
                                                                                                                                WithBot.toDualTopEquiv.symm (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 α] :
                                                                                                                                WithBot.toDualTopEquiv.symm =
                                                                                                                                theorem WithBot.coe_toDualTopEquiv_eq {α : Type u_2} [LE α] :
                                                                                                                                WithBot.toDualTopEquiv = OrderDual.toDual WithBot.ofDual
                                                                                                                                @[simp]
                                                                                                                                theorem WithBot.coeOrderHom_apply {α : Type u_6} [Preorder α] :
                                                                                                                                ∀ (a : α), WithBot.coeOrderHom a = a
                                                                                                                                def WithBot.coeOrderHom {α : Type u_6} [Preorder α] :

                                                                                                                                The coercion α → WithBot α bundled as monotone map.

                                                                                                                                Equations
                                                                                                                                • WithBot.coeOrderHom = { toFun := WithBot.some, inj' := , map_rel_iff' := }
                                                                                                                                Instances For

                                                                                                                                  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 : α) :
                                                                                                                                    WithTop.toDualBotEquiv.symm (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 α] :
                                                                                                                                    WithTop.toDualBotEquiv.symm =
                                                                                                                                    theorem WithTop.coe_toDualBotEquiv {α : Type u_2} [LE α] :
                                                                                                                                    WithTop.toDualBotEquiv = OrderDual.toDual WithTop.ofDual
                                                                                                                                    @[simp]
                                                                                                                                    theorem WithTop.coeOrderHom_apply {α : Type u_6} [Preorder α] :
                                                                                                                                    ∀ (a : α), WithTop.coeOrderHom a = a
                                                                                                                                    def WithTop.coeOrderHom {α : Type u_6} [Preorder α] :

                                                                                                                                    The coercion α → WithTop α bundled as monotone map.

                                                                                                                                    Equations
                                                                                                                                    • WithTop.coeOrderHom = { toFun := WithTop.some, inj' := , map_rel_iff' := }
                                                                                                                                    Instances For
                                                                                                                                      @[simp]
                                                                                                                                      theorem OrderIso.withTopCongr_apply {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] (e : α ≃o β) :
                                                                                                                                      ∀ (a : Option α), e.withTopCongr 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
                                                                                                                                      • e.withTopCongr = { toEquiv := e.optionCongr, map_rel_iff' := }
                                                                                                                                      Instances For
                                                                                                                                        @[simp]
                                                                                                                                        theorem OrderIso.withTopCongr_refl {α : Type u_2} [PartialOrder α] :
                                                                                                                                        (OrderIso.refl α).withTopCongr = OrderIso.refl (WithTop α)
                                                                                                                                        @[simp]
                                                                                                                                        theorem OrderIso.withTopCongr_symm {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] (e : α ≃o β) :
                                                                                                                                        e.withTopCongr.symm = e.symm.withTopCongr
                                                                                                                                        @[simp]
                                                                                                                                        theorem OrderIso.withTopCongr_trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [PartialOrder α] [PartialOrder β] [PartialOrder γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) :
                                                                                                                                        e₁.withTopCongr.trans e₂.withTopCongr = (e₁.trans e₂).withTopCongr
                                                                                                                                        @[simp]
                                                                                                                                        theorem OrderIso.withBotCongr_apply {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] (e : α ≃o β) :
                                                                                                                                        ∀ (a : Option α), e.withBotCongr 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
                                                                                                                                        • e.withBotCongr = { toEquiv := e.optionCongr, map_rel_iff' := }
                                                                                                                                        Instances For
                                                                                                                                          @[simp]
                                                                                                                                          theorem OrderIso.withBotCongr_refl {α : Type u_2} [PartialOrder α] :
                                                                                                                                          (OrderIso.refl α).withBotCongr = OrderIso.refl (WithBot α)
                                                                                                                                          @[simp]
                                                                                                                                          theorem OrderIso.withBotCongr_symm {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] (e : α ≃o β) :
                                                                                                                                          e.withBotCongr.symm = e.symm.withBotCongr
                                                                                                                                          @[simp]
                                                                                                                                          theorem OrderIso.withBotCongr_trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [PartialOrder α] [PartialOrder β] [PartialOrder γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) :
                                                                                                                                          e₁.withBotCongr.trans e₂.withBotCongr = (e₁.trans e₂).withBotCongr
                                                                                                                                          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)
                                                                                                                                          theorem denselyOrdered_iff_of_orderIsoClass {X : Type u_6} {Y : Type u_7} {F : Type u_8} [Preorder X] [Preorder Y] [EquivLike F X Y] [OrderIsoClass F X Y] (f : F) :