Documentation

Mathlib.Order.Hom.Basic

Order homomorphisms #

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

Tags #

monotone map, bundled morphism

structure OrderHom (α : Type u_1) (β : Type u_2) [inst : Preorder α] [inst : Preorder β] :
Type (maxu_1u_2)
  • The underlying funcrion of an OrderHom.

    toFun : αβ
  • The underlying function of an OrderHom is monotone.

    monotone' : Monotone toFun

Bundled monotone (aka, increasing) function

Instances For
    @[inline]
    abbrev OrderEmbedding (α : Type u_1) (β : Type u_2) [inst : LE α] [inst : LE β] :
    Type (maxu_1u_2)

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

    Equations
    @[inline]
    abbrev OrderIso (α : Type u_1) (β : Type u_2) [inst : LE α] [inst : LE β] :
    Type (maxu_1u_2)

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

    Equations
    @[inline]
    abbrev OrderHomClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : LE α] [inst : LE β] :
    Type (max(maxu_1u_2)u_3)

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

    Equations
    class OrderIsoClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : LE α] [inst : LE β] extends EquivLike :
    Type (max(maxu_1u_2)u_3)
    • An order isomorphism respects ≤≤.

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

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

    You should extend this class when you extend OrderIso.

    Instances
      def OrderIsoClass.toOrderIso {F : Type u_1} {α : Type u_2} {β : Type u_3} :
      {x : LE α} → {x_1 : LE β} → [inst : OrderIsoClass 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 β≃o β.

      Equations
      • One or more equations did not get rendered due to their size.
      instance instCoeTCOrderIso {F : Type u_1} {α : Type u_2} {β : Type u_3} :
      {x : LE α} → {x_1 : LE β} → [inst : OrderIsoClass F α β] → CoeTC F (α ≃o β)

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

      Equations
      • instCoeTCOrderIso = { coe := OrderIsoClass.toOrderIso }
      instance OrderIsoClass.toOrderHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} :
      {x : LE α} → {x_1 : LE β} → [inst : OrderIsoClass F α β] → OrderHomClass F α β
      Equations
      • OrderIsoClass.toOrderHomClass = let src := EquivLike.toEmbeddingLike; RelHomClass.mk (_ : ∀ (f : F) (x x_1 : α), x x_1f x f x_1)
      theorem OrderHomClass.monotone {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : OrderHomClass F α β] (f : F) :
      theorem OrderHomClass.mono {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : OrderHomClass F α β] (f : F) :
      def OrderHomClass.toOrderHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : OrderHomClass F α β] (f : F) :
      α →o β

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

      Equations
      • f = { toFun := f, monotone' := (_ : Monotone f) }
      instance OrderHomClass.instCoeTCOrderHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : 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_2} {α : Type u_1} {β : Type u_3} [inst : LE α] [inst : LE β] [inst : OrderIsoClass F α β] (f : F) {a : α} {b : β} :
      EquivLike.inv f b a b f a
      @[simp]
      theorem le_map_inv_iff {F : Type u_2} {α : Type u_1} {β : Type u_3} [inst : LE α] [inst : LE β] [inst : OrderIsoClass F α β] (f : F) {a : α} {b : β} :
      a EquivLike.inv f b f a b
      theorem map_lt_map_iff {F : Type u_2} {α : Type u_3} {β : Type u_1} [inst : Preorder α] [inst : Preorder β] [inst : OrderIsoClass F α β] (f : F) {a : α} {b : α} :
      f a < f b a < b
      @[simp]
      theorem map_inv_lt_iff {F : Type u_2} {α : Type u_1} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : OrderIsoClass F α β] (f : F) {a : α} {b : β} :
      EquivLike.inv f b < a b < f a
      @[simp]
      theorem lt_map_inv_iff {F : Type u_2} {α : Type u_1} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : OrderIsoClass F α β] (f : F) {a : α} {b : β} :
      a < EquivLike.inv f b f a < b
      instance OrderHom.instCoeFunOrderHomForAll {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] :
      CoeFun (α →o β) fun x => αβ

      Helper instance for when there's too many metavariables to apply the coercion via FunLike directly. Remark(Floris): I think this instance is a really bad idea because now applications of FunLike.coe are not being simplified by simp, unlike all other hom-classes. Todo: fix after port.

      Equations
      • OrderHom.instCoeFunOrderHomForAll = { coe := OrderHom.toFun }
      theorem OrderHom.monotone {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (f : α →o β) :
      theorem OrderHom.mono {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (f : α →o β) :
      instance OrderHom.instOrderHomClassOrderHomToLEToLE {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] :
      OrderHomClass (α →o β) α β
      Equations
      • OrderHom.instOrderHomClassOrderHomToLEToLE = RelHomClass.mk (_ : ∀ (f : α →o β) (x x_1 : α), x x_1f x f x_1)
      def OrderHom.Simps.coe {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (f : α →o β) :
      αβ

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

      Equations
      theorem OrderHom.coe_fun_mk {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {f : αβ} (hf : Monotone f) :
      { toFun := f, monotone' := hf } = f
      theorem OrderHom.ext {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (f : α →o β) (g : α →o β) (h : f = g) :
      f = g
      instance OrderHom.instCanLiftForAllOrderHomToFunMonotone {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] :
      CanLift (αβ) (α →o β) OrderHom.toFun Monotone

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

      Equations
      • OrderHom.instCanLiftForAllOrderHomToFunMonotone = { prf := (_ : ∀ (f : αβ), Monotone fy, y = f) }
      def OrderHom.copy {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : 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
      @[simp]
      theorem OrderHom.coe_copy {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (f : α →o β) (f' : αβ) (h : f' = f) :
      ↑(OrderHom.copy f f' h) = f'
      theorem OrderHom.copy_eq {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (f : α →o β) (f' : αβ) (h : f' = f) :
      OrderHom.copy f f' h = f
      @[simp]
      theorem OrderHom.id_coe {α : Type u_1} [inst : Preorder α] :
      OrderHom.id = id
      def OrderHom.id {α : Type u_1} [inst : Preorder α] :
      α →o α

      The identity function as bundled monotone function.

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

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

      Equations
      instance OrderHom.instPartialOrderOrderHomToPreorder {α : Type u_1} [inst : Preorder α] {β : Type u_2} [inst : PartialOrder β] :
      Equations
      • OrderHom.instPartialOrderOrderHomToPreorder = PartialOrder.lift OrderHom.toFun (_ : ∀ (f g : α →o β), f = gf = g)
      theorem OrderHom.le_def {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {f : α →o β} {g : α →o β} :
      f g ∀ (x : α), f x g x
      @[simp]
      theorem OrderHom.coe_le_coe {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {f : α →o β} {g : α →o β} :
      f g f g
      @[simp]
      theorem OrderHom.mk_le_mk {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : 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_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {f : α →o β} {g : α →o β} {x : α} {y : α} (h₁ : f g) (h₂ : x y) :
      f x g y
      def OrderHom.curry {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] :
      (α × β →o γ) ≃o (α →o β →o γ)

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

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

      The composition of two bundled monotone functions.

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

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

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem OrderHom.comp_id {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (f : α →o β) :
      OrderHom.comp f OrderHom.id = f
      @[simp]
      theorem OrderHom.id_comp {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (f : α →o β) :
      OrderHom.comp OrderHom.id f = f
      @[simp]
      theorem OrderHom.const_coe_coe (α : Type u_1) [inst : Preorder α] {β : Type u_2} [inst : Preorder β] (b : β) :
      ↑(↑(OrderHom.const α) b) = Function.const α b
      def OrderHom.const (α : Type u_1) [inst : Preorder α] {β : Type u_2} [inst : Preorder β] :
      β →o α →o β

      Constant function bundled as a OrderHom.

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem OrderHom.const_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] (f : α →o β) (c : γ) :
      @[simp]
      theorem OrderHom.comp_const {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] (γ : Type u_1) [inst : Preorder γ] (f : α →o β) (c : α) :
      OrderHom.comp f (↑(OrderHom.const γ) c) = ↑(OrderHom.const γ) (f c)
      @[simp]
      theorem OrderHom.prod_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] (f : α →o β) (g : α →o γ) (x : α) :
      ↑(OrderHom.prod f g) x = (f x, g x)
      def OrderHom.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] (f : α →o β) (g : α →o γ) :
      α →o β × γ

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

      Equations
      • One or more equations did not get rendered due to their size.
      theorem OrderHom.prod_mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] {f₁ : α →o β} {f₂ : α →o β} (hf : f₁ f₂) {g₁ : α →o γ} {g₂ : α →o γ} (hg : g₁ g₂) :
      OrderHom.prod f₁ g₁ OrderHom.prod f₂ g₂
      theorem OrderHom.comp_prod_comp_same {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] (f₁ : β →o γ) (f₂ : β →o γ) (g : α →o β) :
      @[simp]
      theorem OrderHom.prodₘ_coe_coe_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] (x : α →o β) :
      ∀ (a : α →o γ) (x : α), ↑(↑(OrderHom.prodₘ x) a) x = (x x, a x)
      def OrderHom.prodₘ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] :
      (α →o β) →o (α →o γ) →o α →o β × γ

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

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem OrderHom.diag_coe {α : Type u_1} [inst : Preorder α] (x : α) :
      OrderHom.diag x = (x, x)
      def OrderHom.diag {α : Type u_1} [inst : Preorder α] :
      α →o α × α

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

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

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

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

      Prod.fst as a OrderHom.

      Equations
      • OrderHom.fst = { toFun := Prod.fst, monotone' := (_ : ∀ (x x_1 : α × β), x x_1x.fst x_1.fst) }
      @[simp]
      theorem OrderHom.snd_coe {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (self : α × β) :
      OrderHom.snd self = self.snd
      def OrderHom.snd {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] :
      α × β →o β

      Prod.snd as a OrderHom.

      Equations
      • OrderHom.snd = { toFun := Prod.snd, monotone' := (_ : ∀ (x x_1 : α × β), x x_1x.snd x_1.snd) }
      @[simp]
      theorem OrderHom.fst_prod_snd {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] :
      OrderHom.prod OrderHom.fst OrderHom.snd = OrderHom.id
      @[simp]
      theorem OrderHom.fst_comp_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] (f : α →o β) (g : α →o γ) :
      OrderHom.comp OrderHom.fst (OrderHom.prod f g) = f
      @[simp]
      theorem OrderHom.snd_comp_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] (f : α →o β) (g : α →o γ) :
      OrderHom.comp OrderHom.snd (OrderHom.prod f g) = g
      @[simp]
      theorem OrderHom.prodIso_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] (f : (α →o β) × (α →o γ)) :
      (RelIso.toRelEmbedding (RelIso.symm OrderHom.prodIso)).toEmbedding f = OrderHom.prod f.fst f.snd
      @[simp]
      theorem OrderHom.prodIso_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] (f : α →o β × γ) :
      (RelIso.toRelEmbedding OrderHom.prodIso).toEmbedding f = (OrderHom.comp OrderHom.fst f, OrderHom.comp OrderHom.snd f)
      def OrderHom.prodIso {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : 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.
      @[simp]
      theorem OrderHom.prodMap_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : Preorder δ] (f : α →o β) (g : γ →o δ) :
      ∀ (a : α × γ), ↑(OrderHom.prodMap f g) a = Prod.map (f) (g) a
      def OrderHom.prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : Preorder δ] (f : α →o β) (g : γ →o δ) :
      α × γ →o β × δ

      Prod.map of two OrderHoms as a OrderHom.

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem Pi.evalOrderHom_coe {ι : Type u_1} {π : ιType u_2} [inst : (i : ι) → Preorder (π i)] (i : ι) :
      def Pi.evalOrderHom {ι : Type u_1} {π : ιType u_2} [inst : (i : ι) → Preorder (π i)] (i : ι) :
      ((j : ι) → π j) →o π i

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

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

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

      Equations
      • OrderHom.coeFnHom = { toFun := fun f => f, monotone' := (_ : ∀ (x x_1 : α →o β), x x_1x x_1) }
      @[simp]
      theorem OrderHom.apply_coe {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (x : α) :
      ↑(OrderHom.apply x) = (fun f => f x) fun f => f
      def OrderHom.apply {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (x : α) :
      (α →o β) →o β

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

      Equations
      @[simp]
      theorem OrderHom.pi_coe {α : Type u_1} [inst : Preorder α] {ι : Type u_2} {π : ιType u_3} [inst : (i : ι) → Preorder (π i)] (f : (i : ι) → α →o π i) (x : α) (i : ι) :
      ↑(OrderHom.pi f) x i = ↑(f i) x
      def OrderHom.pi {α : Type u_1} [inst : Preorder α] {ι : Type u_2} {π : ιType u_3} [inst : (i : ι) → Preorder (π i)] (f : (i : ι) → α →o π i) :
      α →o (i : ι) → π i

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

      Equations
      • OrderHom.pi f = { toFun := fun x i => ↑(f i) x, monotone' := (_ : ∀ (x x_1 : α), x x_1∀ (i : ι), ↑(f i) x ↑(f i) x_1) }
      @[simp]
      theorem OrderHom.piIso_symm_apply {α : Type u_1} [inst : Preorder α] {ι : Type u_2} {π : ιType u_3} [inst : (i : ι) → Preorder (π i)] (f : (i : ι) → α →o π i) :
      (RelIso.toRelEmbedding (RelIso.symm OrderHom.piIso)).toEmbedding f = OrderHom.pi f
      @[simp]
      theorem OrderHom.piIso_apply {α : Type u_1} [inst : Preorder α] {ι : Type u_2} {π : ιType u_3} [inst : (i : ι) → Preorder (π i)] (f : α →o (i : ι) → π i) (i : ι) :
      (RelIso.toRelEmbedding OrderHom.piIso).toEmbedding f i = OrderHom.comp (Pi.evalOrderHom i) f
      def OrderHom.piIso {α : Type u_1} [inst : Preorder α] {ι : Type u_2} {π : ιType u_3} [inst : (i : ι) → Preorder (π i)] :
      (α →o (i : ι) → π i) ≃o ((i : ι) → α →o π i)

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

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

      Subtype.val as a bundled monotone function.

      Equations
      instance OrderHom.unique {α : Type u_1} [inst : Preorder α] [inst : Subsingleton α] :
      Unique (α →o α)

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

      Equations
      • OrderHom.unique = { toInhabited := { default := OrderHom.id }, uniq := (_ : ∀ (x : α →o α), x = default) }
      theorem OrderHom.orderHom_eq_id {α : Type u_1} [inst : Preorder α] [inst : Subsingleton α] (g : α →o α) :
      g = OrderHom.id
      @[simp]
      theorem OrderHom.dual_symm_apply_coe {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (f : αᵒᵈ →o βᵒᵈ) :
      ∀ (a : α), ↑(↑(Equiv.symm OrderHom.dual) f) a = (OrderDual.ofDual f OrderDual.toDual) a
      @[simp]
      theorem OrderHom.dual_apply_coe {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (f : α →o β) :
      ∀ (a : αᵒᵈ), ↑(OrderHom.dual f) a = (OrderDual.toDual f OrderDual.ofDual) a
      def OrderHom.dual {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : 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.
      @[simp]
      theorem OrderHom.dual_id {α : Type u_1} [inst : Preorder α] :
      OrderHom.dual OrderHom.id = OrderHom.id
      @[simp]
      theorem OrderHom.dual_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] (g : β →o γ) (f : α →o β) :
      OrderHom.dual (OrderHom.comp g f) = OrderHom.comp (OrderHom.dual g) (OrderHom.dual f)
      @[simp]
      theorem OrderHom.symm_dual_id {α : Type u_1} [inst : Preorder α] :
      ↑(Equiv.symm OrderHom.dual) OrderHom.id = OrderHom.id
      @[simp]
      theorem OrderHom.symm_dual_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] (g : βᵒᵈ →o γᵒᵈ) (f : αᵒᵈ →o βᵒᵈ) :
      ↑(Equiv.symm OrderHom.dual) (OrderHom.comp g f) = OrderHom.comp (↑(Equiv.symm OrderHom.dual) g) (↑(Equiv.symm OrderHom.dual) f)
      def OrderHom.dualIso (α : Type u_1) (β : Type u_2) [inst : Preorder α] [inst : Preorder β] :

      OrderHom.dual as an order isomorphism.

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem OrderHom.withBotMap_coe {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (f : α →o β) :
      def OrderHom.withBotMap {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (f : α →o β) :

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

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

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

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

      Embeddings of partial orders that preserve < also preserve ≤≤.

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

      < is preserved by order embeddings of preorders.

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

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

      Equations
      @[simp]
      theorem OrderEmbedding.withBotMap_apply {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (f : α ↪o β) :
      (OrderEmbedding.withBotMap f).toEmbedding = WithBot.map f.toEmbedding
      def OrderEmbedding.withBotMap {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (f : α ↪o β) :

      A version of WithBot.map for order embeddings.

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem OrderEmbedding.withTopMap_apply {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (f : α ↪o β) :
      (OrderEmbedding.withTopMap f).toEmbedding = WithTop.map f.toEmbedding
      def OrderEmbedding.withTopMap {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (f : α ↪o β) :

      A version of WithTop.map for order embeddings.

      Equations
      • One or more equations did not get rendered due to their size.
      def OrderEmbedding.ofMapLEIff {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : 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≤ f b ↔ a ≤ b↔ a ≤ b≤ b.

      Equations
      @[simp]
      theorem OrderEmbedding.coe_ofMapLEIff {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : Preorder β] {f : αβ} (h : ∀ (a b : α), f a f b a b) :
      (OrderEmbedding.ofMapLEIff f h).toEmbedding = f
      def OrderEmbedding.ofStrictMono {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst : Preorder β] (f : αβ) (h : StrictMono f) :
      α ↪o β

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

      Equations
      @[simp]
      theorem OrderEmbedding.coe_ofStrictMono {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst : Preorder β] {f : αβ} (h : StrictMono f) :
      (OrderEmbedding.ofStrictMono f h).toEmbedding = f
      @[simp]
      theorem OrderEmbedding.subtype_apply {α : Type u_1} [inst : Preorder α] (p : αProp) :
      (OrderEmbedding.subtype p).toEmbedding = Subtype.val
      def OrderEmbedding.subtype {α : Type u_1} [inst : Preorder α] (p : αProp) :

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

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem OrderEmbedding.toOrderHom_coe {X : Type u_1} {Y : Type u_2} [inst : Preorder X] [inst : Preorder Y] (f : X ↪o Y) :
      ↑(OrderEmbedding.toOrderHom f) = f.toEmbedding
      def OrderEmbedding.toOrderHom {X : Type u_1} {Y : Type u_2} [inst : Preorder X] [inst : Preorder Y] (f : X ↪o Y) :
      X →o Y

      Convert an OrderEmbedding to a OrderHom.

      Equations
      @[simp]
      theorem RelHom.toOrderHom_coe {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : Preorder β] (f : (fun x x_1 => x < x_1) →r fun x x_1 => x < x_1) :
      ↑(RelHom.toOrderHom f) = f
      def RelHom.toOrderHom {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : Preorder β] (f : (fun x x_1 => x < x_1) →r fun x x_1 => x < x_1) :
      α →o β

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

      Equations
      theorem RelEmbedding.toOrderHom_injective {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : Preorder β] (f : (fun x x_1 => x < x_1) ↪r fun x x_1 => x < x_1) :
      instance OrderIso.instOrderIsoClassOrderIso {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] :
      OrderIsoClass (α ≃o β) α β
      Equations
      @[simp]
      theorem OrderIso.toFun_eq_coe {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] {f : α ≃o β} :
      f.toEquiv.toFun = (RelIso.toRelEmbedding f).toEmbedding
      theorem OrderIso.ext {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] {f : α ≃o β} {g : α ≃o β} (h : (RelIso.toRelEmbedding f).toEmbedding = (RelIso.toRelEmbedding g).toEmbedding) :
      f = g
      def OrderIso.toOrderEmbedding {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (e : α ≃o β) :
      α ↪o β

      Reinterpret an order isomorphism as an order embedding.

      Equations
      @[simp]
      theorem OrderIso.coe_toOrderEmbedding {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (e : α ≃o β) :
      (OrderIso.toOrderEmbedding e).toEmbedding = (RelIso.toRelEmbedding e).toEmbedding
      theorem OrderIso.bijective {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (e : α ≃o β) :
      theorem OrderIso.injective {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (e : α ≃o β) :
      theorem OrderIso.surjective {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (e : α ≃o β) :
      theorem OrderIso.apply_eq_iff_eq {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (e : α ≃o β) {x : α} {y : α} :
      (RelIso.toRelEmbedding e).toEmbedding x = (RelIso.toRelEmbedding e).toEmbedding y x = y
      def OrderIso.refl (α : Type u_1) [inst : LE α] :
      α ≃o α

      Identity order isomorphism.

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

      Inverse of an order isomorphism.

      Equations
      @[simp]
      theorem OrderIso.apply_symm_apply {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (e : α ≃o β) (x : β) :
      (RelIso.toRelEmbedding e).toEmbedding ((RelIso.toRelEmbedding (OrderIso.symm e)).toEmbedding x) = x
      @[simp]
      theorem OrderIso.symm_apply_apply {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (e : α ≃o β) (x : α) :
      (RelIso.toRelEmbedding (OrderIso.symm e)).toEmbedding ((RelIso.toRelEmbedding e).toEmbedding x) = x
      @[simp]
      theorem OrderIso.symm_refl (α : Type u_1) [inst : LE α] :
      theorem OrderIso.apply_eq_iff_eq_symm_apply {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (e : α ≃o β) (x : α) (y : β) :
      (RelIso.toRelEmbedding e).toEmbedding x = y x = (RelIso.toRelEmbedding (OrderIso.symm e)).toEmbedding y
      theorem OrderIso.symm_apply_eq {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (e : α ≃o β) {x : α} {y : β} :
      (RelIso.toRelEmbedding (OrderIso.symm e)).toEmbedding y = x y = (RelIso.toRelEmbedding e).toEmbedding x
      @[simp]
      theorem OrderIso.symm_symm {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (e : α ≃o β) :
      theorem OrderIso.symm_injective {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] :
      Function.Injective OrderIso.symm
      @[simp]
      theorem OrderIso.toEquiv_symm {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (e : α ≃o β) :
      Equiv.symm e.toEquiv = (OrderIso.symm e).toEquiv
      def OrderIso.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst : LE β] [inst : LE γ] (e : α ≃o β) (e' : β ≃o γ) :
      α ≃o γ

      Composition of two order isomorphisms is an order isomorphism.

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

      Prod.swap as an OrderIso.

      Equations
      @[simp]
      theorem OrderIso.coe_prodComm {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] :
      (RelIso.toRelEmbedding OrderIso.prodComm).toEmbedding = Prod.swap
      @[simp]
      theorem OrderIso.prodComm_symm {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] :
      OrderIso.symm OrderIso.prodComm = OrderIso.prodComm
      def OrderIso.dualDual (α : Type u_1) [inst : LE α] :

      The order isomorphism between a type and its double dual.

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

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

      Equations
      @[simp]
      theorem OrderIso.toRelIsoLT_apply {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (e : α ≃o β) (x : α) :
      (RelIso.toRelEmbedding (OrderIso.toRelIsoLT e)).toEmbedding x = (RelIso.toRelEmbedding e).toEmbedding x
      @[simp]
      theorem OrderIso.toRelIsoLT_symm {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (e : α ≃o β) :
      def OrderIso.ofRelIsoLT {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] (e : (fun x x_1 => x < x_1) ≃r fun x x_1 => x < x_1) :
      α ≃o β

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

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem OrderIso.ofRelIsoLT_apply {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] (e : (fun x x_1 => x < x_1) ≃r fun x x_1 => x < x_1) (x : α) :
      (RelIso.toRelEmbedding (OrderIso.ofRelIsoLT e)).toEmbedding x = (RelIso.toRelEmbedding e).toEmbedding x
      @[simp]
      theorem OrderIso.ofRelIsoLT_symm {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] (e : (fun x x_1 => x < x_1) ≃r fun x x_1 => x < x_1) :
      @[simp]
      theorem OrderIso.ofRelIsoLT_toRelIsoLT {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] (e : α ≃o β) :
      @[simp]
      theorem OrderIso.toRelIsoLT_ofRelIsoLT {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] (e : (fun x x_1 => x < x_1) ≃r fun x x_1 => x < x_1) :
      def OrderIso.ofCmpEqCmp {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst : 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
      • One or more equations did not get rendered due to their size.
      def OrderIso.ofHomInv {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {F : Type u_3} {G : Type u_4} [inst : OrderHomClass F α β] [inst : OrderHomClass G β α] (f : F) (g : G) (h₁ : OrderHom.comp f g = OrderHom.id) (h₂ : OrderHom.comp g f = OrderHom.id) :
      α ≃o β

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

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem OrderIso.funUnique_toEquiv (α : Type u_1) (β : Type u_2) [inst : Unique α] [inst : Preorder β] :
      (OrderIso.funUnique α β).toEquiv = Equiv.funUnique α β
      @[simp]
      theorem OrderIso.funUnique_apply (α : Type u_1) (β : Type u_2) [inst : Unique α] [inst : Preorder β] (f : (x : α) → (fun a => β) x) :
      (RelIso.toRelEmbedding (OrderIso.funUnique α β)).toEmbedding f = f default
      def OrderIso.funUnique (α : Type u_1) (β : Type u_2) [inst : Unique α] [inst : Preorder β] :
      (αβ) ≃o β

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

      Equations
      @[simp]
      theorem OrderIso.funUnique_symm_apply {α : Type u_1} {β : Type u_2} [inst : Unique α] [inst : Preorder β] :
      def Equiv.toOrderIso {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (e : α β) (h₁ : Monotone e) (h₂ : Monotone ↑(Equiv.symm e)) :
      α ≃o β

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

      Equations
      @[simp]
      theorem Equiv.coe_toOrderIso {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (e : α β) (h₁ : Monotone e) (h₂ : Monotone ↑(Equiv.symm e)) :
      (RelIso.toRelEmbedding (Equiv.toOrderIso e h₁ h₂)).toEmbedding = e
      @[simp]
      theorem Equiv.toOrderIso_toEquiv {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (e : α β) (h₁ : Monotone e) (h₂ : Monotone ↑(Equiv.symm e)) :
      (Equiv.toOrderIso e h₁ h₂).toEquiv = e
      @[simp]
      theorem StrictMono.orderIsoOfRightInverse_symm_apply {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst : Preorder β] (f : αβ) (h_mono : StrictMono f) (g : βα) (hg : Function.RightInverse g f) :
      @[simp]
      theorem StrictMono.orderIsoOfRightInverse_apply {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst : Preorder β] (f : αβ) (h_mono : StrictMono f) (g : βα) (hg : Function.RightInverse g f) :
      (RelIso.toRelEmbedding (StrictMono.orderIsoOfRightInverse f h_mono g hg)).toEmbedding = f
      def StrictMono.orderIsoOfRightInverse {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst : 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
      • One or more equations did not get rendered due to their size.
      def OrderIso.dual {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (f : α ≃o β) :

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

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

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

      theorem Codisjoint.map_orderIso {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst : OrderTop α] [inst : SemilatticeSup β] [inst : OrderTop β] {a : α} {b : α} (f : α ≃o β) (ha : Codisjoint a b) :
      Codisjoint ((RelIso.toRelEmbedding f).toEmbedding a) ((RelIso.toRelEmbedding f).toEmbedding b)

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

      @[simp]
      theorem disjoint_map_orderIso_iff {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] [inst : OrderBot α] [inst : SemilatticeInf β] [inst : OrderBot β] {a : α} {b : α} (f : α ≃o β) :
      Disjoint ((RelIso.toRelEmbedding f).toEmbedding a) ((RelIso.toRelEmbedding f).toEmbedding b) Disjoint a b
      @[simp]
      theorem codisjoint_map_orderIso_iff {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst : OrderTop α] [inst : SemilatticeSup β] [inst : OrderTop β] {a : α} {b : α} (f : α ≃o β) :
      Codisjoint ((RelIso.toRelEmbedding f).toEmbedding a) ((RelIso.toRelEmbedding f).toEmbedding b) Codisjoint a b
      def WithBot.toDualTopEquiv {α : Type u_1} [inst : LE α] :

      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
      @[simp]
      theorem WithBot.toDualTopEquiv_coe {α : Type u_1} [inst : LE α] (a : α) :
      (RelIso.toRelEmbedding WithBot.toDualTopEquiv).toEmbedding ↑(OrderDual.toDual a) = OrderDual.toDual a
      @[simp]
      theorem WithBot.toDualTopEquiv_symm_coe {α : Type u_1} [inst : LE α] (a : α) :
      (RelIso.toRelEmbedding (OrderIso.symm WithBot.toDualTopEquiv)).toEmbedding (OrderDual.toDual a) = ↑(OrderDual.toDual a)
      @[simp]
      theorem WithBot.toDualTopEquiv_bot {α : Type u_1} [inst : LE α] :
      (RelIso.toRelEmbedding WithBot.toDualTopEquiv).toEmbedding =
      @[simp]
      theorem WithBot.toDualTopEquiv_symm_bot {α : Type u_1} [inst : LE α] :
      (RelIso.toRelEmbedding (OrderIso.symm WithBot.toDualTopEquiv)).toEmbedding =
      theorem WithBot.coe_toDualTopEquiv_eq {α : Type u_1} [inst : LE α] :
      (RelIso.toRelEmbedding WithBot.toDualTopEquiv).toEmbedding = OrderDual.toDual WithBot.ofDual
      def WithTop.toDualBotEquiv {α : Type u_1} [inst : LE α] :

      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
      @[simp]
      theorem WithTop.toDualBotEquiv_coe {α : Type u_1} [inst : LE α] (a : α) :
      (RelIso.toRelEmbedding WithTop.toDualBotEquiv).toEmbedding ↑(OrderDual.toDual a) = OrderDual.toDual a
      @[simp]
      theorem WithTop.toDualBotEquiv_symm_coe {α : Type u_1} [inst : LE α] (a : α) :
      (RelIso.toRelEmbedding (OrderIso.symm WithTop.toDualBotEquiv)).toEmbedding (OrderDual.toDual a) = ↑(OrderDual.toDual a)
      @[simp]
      theorem WithTop.toDualBotEquiv_top {α : Type u_1} [inst : LE α] :
      (RelIso.toRelEmbedding WithTop.toDualBotEquiv).toEmbedding =
      @[simp]
      theorem WithTop.toDualBotEquiv_symm_top {α : Type u_1} [inst : LE α] :
      (RelIso.toRelEmbedding (OrderIso.symm WithTop.toDualBotEquiv)).toEmbedding =
      theorem WithTop.coe_toDualBotEquiv {α : Type u_1} [inst : LE α] :
      (RelIso.toRelEmbedding WithTop.toDualBotEquiv).toEmbedding = OrderDual.toDual WithTop.ofDual
      @[simp]
      theorem OrderIso.withTopCongr_apply {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] (e : α ≃o β) :
      ∀ (a : Option α), (RelIso.toRelEmbedding (OrderIso.withTopCongr e)).toEmbedding a = Option.map ((RelIso.toRelEmbedding e).toEmbedding) a
      def OrderIso.withTopCongr {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] (e : α ≃o β) :

      A version of Equiv.optionCongr for WithTop.

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem OrderIso.withTopCongr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PartialOrder α] [inst : PartialOrder β] [inst : PartialOrder γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) :
      @[simp]
      theorem OrderIso.withBotCongr_apply {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] (e : α ≃o β) :
      ∀ (a : Option α), (RelIso.toRelEmbedding (OrderIso.withBotCongr e)).toEmbedding a = Option.map ((RelIso.toRelEmbedding e).toEmbedding) a
      def OrderIso.withBotCongr {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] (e : α ≃o β) :

      A version of Equiv.optionCongr for WithBot.

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem OrderIso.withBotCongr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PartialOrder α] [inst : PartialOrder β] [inst : PartialOrder γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) :
      theorem OrderIso.isCompl {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst : Lattice β] [inst : BoundedOrder α] [inst : BoundedOrder β] (f : α ≃o β) {x : α} {y : α} (h : IsCompl x y) :
      IsCompl ((RelIso.toRelEmbedding f).toEmbedding x) ((RelIso.toRelEmbedding f).toEmbedding y)
      theorem OrderIso.isCompl_iff {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst : Lattice β] [inst : BoundedOrder α] [inst : BoundedOrder β] (f : α ≃o β) {x : α} {y : α} :
      IsCompl x y IsCompl ((RelIso.toRelEmbedding f).toEmbedding x) ((RelIso.toRelEmbedding f).toEmbedding y)
      theorem OrderIso.complementedLattice {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst : Lattice β] [inst : BoundedOrder α] [inst : BoundedOrder β] (f : α ≃o β) [inst : ComplementedLattice α] :
      theorem OrderIso.complementedLattice_iff {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst : Lattice β] [inst : BoundedOrder α] [inst : BoundedOrder β] (f : α ≃o β) :