# 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:

- `OrderHom α β` a.k.a. `α →o β`: Preorder homomorphism. An `OrderHom α β` is a function `f : α → β` such that `a₁ ≤ a₂ → f a₁ ≤ f a₂`
- `OrderEmbedding α β` a.k.a. `α ↪o β`: Relation embedding. An `OrderEmbedding α β` is an embedding `f : α ↪ β` such that `a ≤ b ↔ f a ≤ f b`. Defined as an abbreviation of `@RelEmbedding α β (≤) (≤)`.
- `OrderIso`: Relation isomorphism. An `OrderIso α β` is an equivalence `f : α ≃ β` such that `a ≤ b ↔ f a ≤ f b`. Defined as an abbreviation of `@RelIso α β (≤) (≤)`.

We also define many `OrderHom`s. 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.

- `OrderHom.id`: identity map as `α →o α`;
- `OrderHom.curry`: an order isomorphism between `α × β →o γ` and `α →o β →o γ`;
- `OrderHom.comp`: composition of two bundled monotone maps;
- `OrderHom.compₘ`: composition of bundled monotone maps as a bundled monotone map;
- `OrderHom.const`: constant function as a bundled monotone map;
- `OrderHom.prod`: combine `α →o β` and `α →o γ` into `α →o β × γ`;
- `OrderHom.prodₘ`: a more bundled version of `OrderHom.prod`;
- `OrderHom.prodIso`: order isomorphism between `α →o β × γ` and `(α →o β) × (α →o γ)`;
- `OrderHom.diag`: diagonal embedding of `α` into `α × α` as a bundled monotone map;
- `OrderHom.onDiag`: restrict a monotone map `α →o α →o β` to the diagonal;
- `OrderHom.fst`: projection `Prod.fst : α × β → α` as a bundled monotone map;
- `OrderHom.snd`: projection `Prod.snd : α × β → β` as a bundled monotone map;
- `OrderHom.prodMap`: `Prod.map f g` as a bundled monotone map;
- `Pi.evalOrderHom`: evaluation of a function at a point `Function.eval i` as a bundled monotone map;
- `OrderHom.coeFnHom`: coercion to function as a bundled monotone map;
- `OrderHom.apply`: application of an `OrderHom` at a point as a bundled monotone map;
- `OrderHom.pi`: combine a family of monotone maps `f i : α →o π i` into a monotone map `α →o Π i, π i`;
- `OrderHom.piIso`: order isomorphism between `α →o Π i, π i` and `Π i, α →o π i`;
- `OrderHom.subtype.val`: embedding `Subtype.val : Subtype p → α` as a bundled monotone map;
- `OrderHom.dual`: reinterpret a monotone map `α →o β` as a monotone map `αᵒᵈ →o βᵒᵈ`;
- `OrderHom.dualIso`: order isomorphism between `α →o β` and `(αᵒᵈ →o βᵒᵈ)ᵒᵈ`;
- `OrderHom.compl`: order isomorphism `α ≃o αᵒᵈ` given by taking complements in a Boolean algebra;

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

- `OrderEmbedding.toOrderHom`: convert `α ↪o β` to `α →o β`;
- `RelHom.toOrderHom`: convert a `RelHom` between strict orders to an `OrderHom`.

## Tags #

monotone map, bundled morphism

source
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

source
def «term_→o_» :
Lean.TrailingParserDescr

Notation for an `OrderHom`.

Equations

- «term_→o_» = Lean.ParserDescr.trailingNode `«term_→o_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →o ") (Lean.ParserDescr.cat `term 25))

Instances For

source
@[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

source
def «term_↪o_» :
Lean.TrailingParserDescr

Notation for an `OrderEmbedding`.

Equations

- «term_↪o_» = Lean.ParserDescr.trailingNode `«term_↪o_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↪o ") (Lean.ParserDescr.cat `term 26))

Instances For

source
@[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

source
def «term_≃o_» :
Lean.TrailingParserDescr

Notation for an `OrderIso`.

Equations

- «term_≃o_» = Lean.ParserDescr.trailingNode `«term_≃o_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃o ") (Lean.ParserDescr.cat `term 26))

Instances For

source
@[reducible, inline]
abbrev OrderHomClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [LE α] [LE β] [FunLike F α β] :
Prop

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

Equations

- OrderHomClass F α β = RelHomClass F (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : β) => x1 ≤ x2

Instances For

source
class OrderIsoClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [LE α] [LE β] [EquivLike F α β] :
Prop

`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

source
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

source
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 }

source
@[instance 100]
instance OrderIsoClass.toOrderHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [LE β] [EquivLike F α β] [OrderIsoClass F α β] :
OrderHomClass F α β
source
theorem OrderHomClass.monotone {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [FunLike F α β] [OrderHomClass F α β] (f : F) :
Monotone ⇑f
source
theorem OrderHomClass.mono {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [FunLike F α β] [OrderHomClass F α β] (f : F) :
Monotone ⇑f
source
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

source
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 }

source
@[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
source
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 : β} :
EquivLike.inv f b ≤ EquivLike.inv f a ↔ b ≤ a
source
@[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
source
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
source
@[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
source
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 : β} :
EquivLike.inv f b < EquivLike.inv f a ↔ b < a
source
@[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
source
instance OrderHom.instFunLike {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] :
FunLike (α →o β) α β
Equations

- OrderHom.instFunLike = { coe := OrderHom.toFun, coe_injective' := ⋯ }

source
instance OrderHom.instOrderHomClass {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] :
OrderHomClass (α →o β) α β
source
@[simp]
theorem OrderHom.coe_mk {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α → β) (hf : Monotone f) :
⇑{ toFun := f, monotone' := hf } = f
source
theorem OrderHom.monotone {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :
Monotone ⇑f
source
theorem OrderHom.mono {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :
Monotone ⇑f
source
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

- OrderHom.Simps.coe f = ⇑f

Instances For

source
@[simp]
theorem OrderHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :
f.toFun = ⇑f
source
theorem OrderHom.ext {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f g : α →o β) (h : ⇑f = ⇑g) :
f = g
source
theorem OrderHom.ext_iff {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {f g : α →o β} :
f = g ↔ ⇑f = ⇑g
source
@[simp]
theorem OrderHom.coe_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :
↑f = f
source
@[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
source
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.

source
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

source
@[simp]
theorem OrderHom.coe_copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) (f' : α → β) (h : f' = ⇑f) :
⇑(f.copy f' h) = f'
source
theorem OrderHom.copy_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) (f' : α → β) (h : f' = ⇑f) :
f.copy f' h = f
source
instance OrderHom.instDecidableEqOfForall {α : Type u_6} (β : Type u_7) [PartialOrder α] [PartialOrder β] [DecidableEq (α → β)] :
DecidableEq (α →o β)
Equations

- OrderHom.instDecidableEqOfForall β a b = decidable_of_iff (a.toFun = b.toFun) ⋯

source
def OrderHom.id {α : Type u_2} [Preorder α] :
α →o α

The identity function as bundled monotone function.

Equations

- OrderHom.id = { toFun := id, monotone' := ⋯ }

Instances For

source
@[simp]
theorem OrderHom.id_coe {α : Type u_2} [Preorder α] :
⇑id = _root_.id
source
instance OrderHom.instInhabited {α : Type u_2} [Preorder α] :
Inhabited (α →o α)
Equations

- OrderHom.instInhabited = { default := OrderHom.id }

source
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

- OrderHom.instPreorder = Preorder.lift OrderHom.toFun

source
instance OrderHom.instPartialOrder {α : Type u_2} [Preorder α] {β : Type u_6} [PartialOrder β] :
PartialOrder (α →o β)
Equations

- OrderHom.instPartialOrder = PartialOrder.lift OrderHom.toFun ⋯

source
theorem OrderHom.le_def {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {f g : α →o β} :
f ≤ g ↔ ∀ (x : α), f x ≤ g x
source
@[simp]
theorem OrderHom.coe_le_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {f g : α →o β} :
⇑f ≤ ⇑g ↔ f ≤ g
source
@[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
source
theorem OrderHom.apply_mono {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {f g : α →o β} {x y : α} (h₁ : f ≤ g) (h₂ : x ≤ y) :
f x ≤ g y
source
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

source
@[simp]
theorem OrderHom.curry_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : α × β →o γ) (x : α) (y : β) :
((curry f) x) y = f (x, y)
source
@[simp]
theorem OrderHom.curry_symm_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : α →o β →o γ) (x : α × β) :
((RelIso.symm curry) f) x = (f x.1) x.2
source
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

source
@[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
source
theorem OrderHom.comp_mono {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] ⦃g₁ g₂ : β →o γ⦄ (hg : g₁ ≤ g₂) ⦃f₁ f₂ : α →o β⦄ (hf : f₁ ≤ f₂) :
g₁.comp f₁ ≤ g₂.comp f₂
source
@[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' := ⋯ }
source
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

source
@[simp]
theorem OrderHom.compₘ_coe_coe_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (x : β →o γ) (a✝ : α →o β) :
⇑((compₘ x) a✝) = ⇑x ∘ ⇑a✝
source
@[simp]
theorem OrderHom.comp_id {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :
f.comp id = f
source
@[simp]
theorem OrderHom.id_comp {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :
id.comp f = f
source
def OrderHom.const (α : Type u_6) [Preorder α] {β : Type u_7} [Preorder β] :
β →o α →o β

Constant function bundled as an `OrderHom`.

Equations

- OrderHom.const α = { toFun := fun (b : β) => { toFun := Function.const α b, monotone' := ⋯ }, monotone' := ⋯ }

Instances For

source
@[simp]
theorem OrderHom.const_coe_coe (α : Type u_6) [Preorder α] {β : Type u_7} [Preorder β] (b : β) :
⇑((const α) b) = Function.const α b
source
@[simp]
theorem OrderHom.const_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : α →o β) (c : γ) :
((const β) c).comp f = (const α) c
source
@[simp]
theorem OrderHom.comp_const {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (γ : Type u_6) [Preorder γ] (f : α →o β) (c : α) :
f.comp ((const γ) c) = (const γ) (f c)
source
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

source
@[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)
source
theorem OrderHom.prod_mono {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] {f₁ f₂ : α →o β} (hf : f₁ ≤ f₂) {g₁ g₂ : α →o γ} (hg : g₁ ≤ g₂) :
f₁.prod g₁ ≤ f₂.prod g₂
source
theorem OrderHom.comp_prod_comp_same {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f₁ f₂ : β →o γ) (g : α →o β) :
(f₁.comp g).prod (f₂.comp g) = (f₁.prod f₂).comp g
source
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

source
@[simp]
theorem OrderHom.prodₘ_coe_coe_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (x : α →o β) (a✝ : α →o γ) (x✝ : α) :
((prodₘ x) a✝) x✝ = (x x✝, a✝ x✝)
source
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

source
@[simp]
theorem OrderHom.diag_coe {α : Type u_2} [Preorder α] (x : α) :
diag x = (x, x)
source
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

source
@[simp]
theorem OrderHom.onDiag_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o α →o β) (a✝ : α) :
f.onDiag a✝ = (f a✝) a✝
source
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

source
@[simp]
theorem OrderHom.fst_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (self : α × β) :
fst self = self.1
source
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

source
@[simp]
theorem OrderHom.snd_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (self : α × β) :
snd self = self.2
source
@[simp]
theorem OrderHom.fst_prod_snd {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] :
fst.prod snd = id
source
@[simp]
theorem OrderHom.fst_comp_prod {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : α →o β) (g : α →o γ) :
fst.comp (f.prod g) = f
source
@[simp]
theorem OrderHom.snd_comp_prod {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : α →o β) (g : α →o γ) :
snd.comp (f.prod g) = g
source
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

source
@[simp]
theorem OrderHom.prodIso_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : α →o β × γ) :
prodIso f = (fst.comp f, snd.comp f)
source
@[simp]
theorem OrderHom.prodIso_symm_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : (α →o β) × (α →o γ)) :
(RelIso.symm prodIso) f = f.1.prod f.2
source
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 `OrderHom`s as an `OrderHom`

Equations

- f.prodMap g = { toFun := Prod.map ⇑f ⇑g, monotone' := ⋯ }

Instances For

source
@[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✝
source
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

- Pi.evalOrderHom i = { toFun := Function.eval i, monotone' := ⋯ }

Instances For

source
@[simp]
theorem Pi.evalOrderHom_coe {ι : Type u_6} {π : ι → Type u_7} [(i : ι) → Preorder (π i)] (i : ι) :
⇑(evalOrderHom i) = Function.eval i
source
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

source
@[simp]
theorem OrderHom.coeFnHom_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] :
⇑coeFnHom = fun (f : α →o β) => ⇑f
source
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

- OrderHom.apply x = (Pi.evalOrderHom x).comp OrderHom.coeFnHom

Instances For

source
@[simp]
theorem OrderHom.apply_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (x : α) :
⇑(apply x) = Function.eval x ∘ fun (f : α →o β) => ⇑f
source
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

source
@[simp]
theorem OrderHom.pi_coe {α : Type u_2} [Preorder α] {ι : Type u_6} {π : ι → Type u_7} [(i : ι) → Preorder (π i)] (f : (i : ι) → α →o π i) (x : α) (i : ι) :
(pi f) x i = (f i) x
source
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

source
@[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 piIso) f = pi f
source
@[simp]
theorem OrderHom.piIso_apply {α : Type u_2} [Preorder α] {ι : Type u_6} {π : ι → Type u_7} [(i : ι) → Preorder (π i)] (f : α →o (i : ι) → π i) (i : ι) :
piIso f i = (Pi.evalOrderHom i).comp f
source
def OrderHom.Subtype.val {α : Type u_2} [Preorder α] (p : α → Prop) :
Subtype p →o α

`Subtype.val` as a bundled monotone function.

Equations

- OrderHom.Subtype.val p = { toFun := Subtype.val, monotone' := ⋯ }

Instances For

source
@[simp]
theorem OrderHom.Subtype.val_coe {α : Type u_2} [Preorder α] (p : α → Prop) :
⇑(val p) = _root_.Subtype.val
source
def Subtype.orderEmbedding {α : Type u_2} [Preorder α] {p q : α → Prop} (h : ∀ (a : α), p a → q a) :
{ x : α // p x } ↪o { x : α // q x }

`Subtype.impEmbedding` as an order embedding.

Equations

- Subtype.orderEmbedding h = { toEmbedding := Subtype.impEmbedding p q h, map_rel_iff' := ⋯ }

Instances For

source
@[simp]
theorem Subtype.orderEmbedding_apply_coe {α : Type u_2} [Preorder α] {p q : α → Prop} (h : ∀ (a : α), p a → q a) (x : { x : α // p x }) :
↑((orderEmbedding h) x) = ↑x
source
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 := ⋯ }

source
theorem OrderHom.orderHom_eq_id {α : Type u_2} [Preorder α] [Subsingleton α] (g : α →o α) :
g = id
source
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

source
@[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✝
source
@[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✝
source
@[simp]
theorem OrderHom.dual_id {α : Type u_2} [Preorder α] :
OrderHom.dual id = id
source
@[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)
source
@[simp]
theorem OrderHom.symm_dual_id {α : Type u_2} [Preorder α] :
OrderHom.dual.symm id = id
source
@[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)
source
def OrderHom.dualIso (α : Type u_8) (β : Type u_9) [Preorder α] [Preorder β] :
(α →o β) ≃o (α ᵒᵈ →o β ᵒᵈ)ᵒᵈ

`OrderHom.dual` as an order isomorphism.

Equations

- OrderHom.dualIso α β = { toEquiv := OrderHom.dual.trans OrderDual.toDual, map_rel_iff' := ⋯ }

Instances For

source
def OrderHom.uliftMap {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :
ULift.{u_8, u_2} α →o ULift.{u_9, u_3} β

Lift an order homomorphism `f : α →o β` to an order homomorphism `ULift α →o ULift β` in a higher universe.

Equations

- f.uliftMap = { toFun := fun (i : ULift.{?u.25, ?u.27} α) => { down := f i.down }, monotone' := ⋯ }

Instances For

source
@[simp]
theorem OrderHom.uliftMap_coe_down {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) (i : ULift.{u_8, u_2} α) :
(f.uliftMap i).down = f i.down
source
def OrderHom.uliftRightMap {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :
α →o ULift.{u_8, u_3} β

Lift an order homomorphism `f : α →o β` to an order homomorphism `α →o ULift β` in a higher universe.

Equations

- f.uliftRightMap = { toFun := fun (i : α) => { down := f i }, monotone' := ⋯ }

Instances For

source
@[simp]
theorem OrderHom.uliftRightMap_coe_down {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) (i : α) :
(f.uliftRightMap i).down = f i
source
def OrderHom.uliftLeftMap {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :
ULift.{u_8, u_2} α →o β

Lift an order homomorphism `f : α →o β` to an order homomorphism `ULift α →o β` in a higher universe.

Equations

- f.uliftLeftMap = { toFun := fun (i : ULift.{?u.24, ?u.26} α) => f i.down, monotone' := ⋯ }

Instances For

source
@[simp]
theorem OrderHom.uliftLeftMap_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) (i : ULift.{u_8, u_2} α) :
f.uliftLeftMap i = f i.down
source
@[simp]
theorem OrderHom.uliftLeftMap_uliftRightMap_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :
f.uliftLeftMap.uliftRightMap = f.uliftMap
source
@[simp]
theorem OrderHom.uliftRightMap_uliftLeftMap_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) :
f.uliftRightMap.uliftLeftMap = f.uliftMap
source
@[instance 90]
instance OrderHomClass.toOrderHomClassOrderDual {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [LE β] [FunLike F α β] [OrderHomClass F α β] :
OrderHomClass F α ᵒᵈ β ᵒᵈ
source
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

source
@[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
source
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

source
@[simp]
theorem OrderEmbedding.ltEmbedding_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) (x : α) :
f.ltEmbedding x = f x
source
@[simp]
theorem OrderEmbedding.le_iff_le {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) {a b : α} :
f a ≤ f b ↔ a ≤ b
source
@[simp]
theorem OrderEmbedding.lt_iff_lt {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) {a b : α} :
f a < f b ↔ a < b
source
theorem OrderEmbedding.eq_iff_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) {a b : α} :
f a = f b ↔ a = b
source
theorem OrderEmbedding.monotone {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) :
Monotone ⇑f
source
theorem OrderEmbedding.strictMono {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) :
StrictMono ⇑f
source
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
source
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
source
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
source
def OrderEmbedding.dual {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) :
α ᵒᵈ ↪o β ᵒᵈ

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

Equations

- f.dual = { toEmbedding := f.toEmbedding, map_rel_iff' := ⋯ }

Instances For

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

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

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

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

source
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

- OrderEmbedding.ofMapLEIff f hf = RelEmbedding.ofMapRelIff f hf

Instances For

source
@[simp]
theorem OrderEmbedding.coe_ofMapLEIff {α : Type u_6} {β : Type u_7} [PartialOrder α] [Preorder β] {f : α → β} (h : ∀ (a b : α), f a ≤ f b ↔ a ≤ b) :
⇑(ofMapLEIff f h) = f
source
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

- OrderEmbedding.ofStrictMono f h = OrderEmbedding.ofMapLEIff f ⋯

Instances For

source
@[simp]
theorem OrderEmbedding.coe_ofStrictMono {α : Type u_6} {β : Type u_7} [LinearOrder α] [Preorder β] {f : α → β} (h : StrictMono f) :
⇑(ofStrictMono f h) = f
source
def OrderEmbedding.subtype {α : Type u_2} [Preorder α] (p : α → Prop) :
Subtype p ↪o α

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

Equations

- OrderEmbedding.subtype p = { toEmbedding := Function.Embedding.subtype p, map_rel_iff' := ⋯ }

Instances For

source
@[simp]
theorem OrderEmbedding.subtype_apply {α : Type u_2} [Preorder α] {p : α → Prop} (x : Subtype p) :
(subtype p) x = ↑x
source
theorem OrderEmbedding.subtype_injective {α : Type u_2} [Preorder α] (p : α → Prop) :
Function.Injective ⇑(subtype p)
source
@[simp]
theorem OrderEmbedding.coe_subtype {α : Type u_2} [Preorder α] (p : α → Prop) :
⇑(subtype p) = Subtype.val
source
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

source
@[simp]
theorem OrderEmbedding.toOrderHom_coe {X : Type u_6} {Y : Type u_7} [Preorder X] [Preorder Y] (f : X ↪o Y) :
⇑f.toOrderHom = ⇑f
source
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

source
@[simp]
theorem OrderEmbedding.ofIsEmpty_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [IsEmpty α] (a : α) :
ofIsEmpty a = isEmptyElim a
source
@[simp]
theorem OrderEmbedding.coe_ofIsEmpty {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [IsEmpty α] :
⇑ofIsEmpty = fun (a : α) => isEmptyElim a
source
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.

source
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.

source
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.

source
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

source
@[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
source
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
source
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' := ⋯ }

source
instance OrderIso.instOrderIsoClass {α : Type u_2} {β : Type u_3} [LE α] [LE β] :
OrderIsoClass (α ≃o β) α β
source
@[simp]
theorem OrderIso.toFun_eq_coe {α : Type u_2} {β : Type u_3} [LE α] [LE β] {f : α ≃o β} :
f.toFun = ⇑f
source
theorem OrderIso.ext {α : Type u_2} {β : Type u_3} [LE α] [LE β] {f g : α ≃o β} (h : ⇑f = ⇑g) :
f = g
source
theorem OrderIso.ext_iff {α : Type u_2} {β : Type u_3} [LE α] [LE β] {f g : α ≃o β} :
f = g ↔ ⇑f = ⇑g
source
def OrderIso.toOrderEmbedding {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
α ↪o β

Reinterpret an order isomorphism as an order embedding.

Equations

- e.toOrderEmbedding = RelIso.toRelEmbedding e

Instances For

source
@[simp]
theorem OrderIso.coe_toOrderEmbedding {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
⇑e.toOrderEmbedding = ⇑e
source
theorem OrderIso.bijective {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
Function.Bijective ⇑e
source
theorem OrderIso.injective {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
Function.Injective ⇑e
source
theorem OrderIso.surjective {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
Function.Surjective ⇑e
source
theorem OrderIso.apply_eq_iff_eq {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x y : α} :
e x = e y ↔ x = y
source
def OrderIso.refl (α : Type u_6) [LE α] :
α ≃o α

Identity order isomorphism.

Equations

- OrderIso.refl α = RelIso.refl fun (x1 x2 : α) => x1 ≤ x2

Instances For

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

Inverse of an order isomorphism.

Equations

- e.symm = RelIso.symm e

Instances For

source
@[simp]
theorem OrderIso.symm_mk {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃ β) (map_rel_iff' : ∀ {a b : α}, e a ≤ e b ↔ a ≤ b) :
symm { toEquiv := e, map_rel_iff' := map_rel_iff' } = { toEquiv := e.symm, map_rel_iff' := ⋯ }
source
@[simp]
theorem OrderIso.apply_symm_apply {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) (x : β) :
e (e.symm x) = x
source
@[simp]
theorem OrderIso.symm_apply_apply {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) (x : α) :
e.symm (e x) = x
source
@[simp]
theorem OrderIso.symm_refl (α : Type u_6) [LE α] :
(refl α).symm = refl α
source
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
source
theorem OrderIso.symm_apply_eq {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x : α} {y : β} :
e.symm y = x ↔ y = e x
source
@[simp]
theorem OrderIso.symm_symm {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
e.symm.symm = e
source
theorem OrderIso.symm_bijective {α : Type u_2} {β : Type u_3} [LE α] [LE β] :
Function.Bijective symm
source
theorem OrderIso.symm_injective {α : Type u_2} {β : Type u_3} [LE α] [LE β] :
Function.Injective symm
source
@[simp]
theorem OrderIso.toEquiv_symm {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
e.symm.toEquiv = e.symm
source
@[simp]
theorem OrderIso.coe_toEquiv {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
⇑e.toEquiv = ⇑e
source
@[simp]
theorem OrderIso.coe_symm_toEquiv {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
⇑e.symm = ⇑e.symm
source
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

- e.trans e' = RelIso.trans e e'

Instances For

source
@[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
source
@[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)
source
@[simp]
theorem OrderIso.refl_trans {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
(refl α).trans e = e
source
@[simp]
theorem OrderIso.trans_refl {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
e.trans (refl β) = e
source
@[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)
source
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
source
@[simp]
theorem OrderIso.self_trans_symm {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
e.trans e.symm = refl α
source
@[simp]
theorem OrderIso.symm_trans_self {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
e.symm.trans e = refl β
source
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

source
@[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)
source
@[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)
source
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

source
@[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)
source
@[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✝
source
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

source
@[simp]
theorem OrderIso.coe_prodComm {α : Type u_2} {β : Type u_3} [LE α] [LE β] :
⇑prodComm = Prod.swap
source
@[simp]
theorem OrderIso.prodComm_symm {α : Type u_2} {β : Type u_3} [LE α] [LE β] :
prodComm.symm = prodComm
source
def OrderIso.dualDual (α : Type u_2) [LE α] :
α ≃o α ᵒᵈ ᵒᵈ

The order isomorphism between a type and its double dual.

Equations

- OrderIso.dualDual α = OrderIso.refl α

Instances For

source
@[simp]
theorem OrderIso.coe_dualDual (α : Type u_2) [LE α] :
⇑(dualDual α) = ⇑OrderDual.toDual ∘ ⇑OrderDual.toDual
source
@[simp]
theorem OrderIso.coe_dualDual_symm (α : Type u_2) [LE α] :
⇑(dualDual α).symm = ⇑OrderDual.ofDual ∘ ⇑OrderDual.ofDual
source
@[simp]
theorem OrderIso.dualDual_apply {α : Type u_2} [LE α] (a : α) :
(dualDual α) a = OrderDual.toDual (OrderDual.toDual a)
source
@[simp]
theorem OrderIso.dualDual_symm_apply {α : Type u_2} [LE α] (a : α ᵒᵈ ᵒᵈ) :
(dualDual α).symm a = OrderDual.ofDual (OrderDual.ofDual a)
source
theorem OrderIso.le_iff_le {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x y : α} :
e x ≤ e y ↔ x ≤ y
source
theorem OrderIso.GCongr.orderIso_apply_le_apply {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x y : α} :
x ≤ y → e x ≤ e y

Alias of the reverse direction of `OrderIso.le_iff_le`.

source
theorem OrderIso.le_symm_apply {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x : α} {y : β} :
x ≤ e.symm y ↔ e x ≤ y
source
theorem OrderIso.symm_apply_le {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x : α} {y : β} :
e.symm y ≤ x ↔ y ≤ e x
source
theorem OrderIso.monotone {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) :
Monotone ⇑e
source
theorem OrderIso.strictMono {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) :
StrictMono ⇑e
source
@[simp]
theorem OrderIso.lt_iff_lt {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) {x y : α} :
e x < e y ↔ x < y
source
theorem OrderIso.GCongr.orderIso_apply_lt_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) {x y : α} :
x < y → e x < e y

Alias of the reverse direction of `OrderIso.lt_iff_lt`.

source
theorem OrderIso.lt_symm_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) {x : α} {y : β} :
x < e.symm y ↔ e x < y
source
theorem OrderIso.symm_apply_lt {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) {x : α} {y : β} :
e.symm y < x ↔ y < e x
source
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

source
@[simp]
theorem OrderIso.toRelIsoLT_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) (x : α) :
e.toRelIsoLT x = e x
source
@[simp]
theorem OrderIso.toRelIsoLT_symm {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) :
e.symm.toRelIsoLT = e.toRelIsoLT.symm
source
@[simp]
theorem OrderIso.coe_toRelIsoLT {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) :
⇑e.toRelIsoLT = ⇑e
source
@[simp]
theorem OrderIso.coe_symm_toRelIsoLT {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) :
⇑e.toRelIsoLT.symm = ⇑e.symm
source
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

- OrderIso.ofRelIsoLT e = { toEquiv := e.toEquiv, map_rel_iff' := ⋯ }

Instances For

source
@[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 : α) :
(ofRelIsoLT e) x = e x
source
@[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) :
(ofRelIsoLT e).symm = ofRelIsoLT e.symm
source
@[simp]
theorem OrderIso.ofRelIsoLT_toRelIsoLT {α : Type u_6} {β : Type u_7} [PartialOrder α] [PartialOrder β] (e : α ≃o β) :
ofRelIsoLT e.toRelIsoLT = e
source
@[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) :
(ofRelIsoLT e).toRelIsoLT = e
source
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

source
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

source
@[simp]
theorem OrderIso.ofHomInv_apply {α : 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) (a : α) :
(ofHomInv f g h₁ h₂) a = f a
source
@[simp]
theorem OrderIso.ofHomInv_symm_apply {α : 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) (a : β) :
(ofHomInv f g h₁ h₂).symm a = g a
source
def OrderIso.funUnique (α : Type u_6) (β : Type u_7) [Unique α] [Preorder β] :
(α → β) ≃o β

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

Equations

- OrderIso.funUnique α β = { toEquiv := Equiv.funUnique α β, map_rel_iff' := ⋯ }

Instances For

source
@[simp]
theorem OrderIso.funUnique_apply (α : Type u_6) (β : Type u_7) [Unique α] [Preorder β] (f : (i : α) → (fun (a : α) => β) i) :
(funUnique α β) f = f default
source
@[simp]
theorem OrderIso.funUnique_toEquiv (α : Type u_6) (β : Type u_7) [Unique α] [Preorder β] :
(funUnique α β).toEquiv = Equiv.funUnique α β
source
@[simp]
theorem OrderIso.funUnique_symm_apply {α : Type u_6} {β : Type u_7} [Unique α] [Preorder β] :
⇑(funUnique α β).symm = Function.const α
source
noncomputable def OrderIso.ofUnique (α : Type u_6) (β : Type u_7) [Unique α] [Unique β] [Preorder α] [Preorder β] :
α ≃o β

The order isomorphism `α ≃o β` when `α` and `β` are preordered types containing unique elements.

Equations

- OrderIso.ofUnique α β = { toEquiv := Equiv.ofUnique α β, map_rel_iff' := ⋯ }

Instances For

source
@[simp]
theorem OrderIso.ofUnique_symm_apply (α : Type u_6) (β : Type u_7) [Unique α] [Unique β] [Preorder α] [Preorder β] (a✝ : β) :
(RelIso.symm (ofUnique α β)) a✝ = default
source
@[simp]
theorem OrderIso.ofUnique_apply (α : Type u_6) (β : Type u_7) [Unique α] [Unique β] [Preorder α] [Preorder β] (a✝ : α) :
(ofUnique α β) a✝ = default
source
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

source
@[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
source
@[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
source
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

- StrictMono.orderIsoOfRightInverse f h_mono g hg = { toFun := f, invFun := g, left_inv := ⋯, right_inv := hg, map_rel_iff' := ⋯ }

Instances For

source
@[simp]
theorem StrictMono.orderIsoOfRightInverse_apply {α : Type u_2} {β : Type u_3} [LinearOrder α] [Preorder β] (f : α → β) (h_mono : StrictMono f) (g : β → α) (hg : Function.RightInverse g f) :
⇑(orderIsoOfRightInverse f h_mono g hg) = f
source
@[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) :
⇑(RelIso.symm (orderIsoOfRightInverse f h_mono g hg)) = g
source
def OrderIso.dual {α : Type u_2} {β : Type u_3} [LE α] [LE β] (f : α ≃o β) :
α ᵒᵈ ≃o β ᵒᵈ

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

Equations

- f.dual = { toEquiv := f.toEquiv, map_rel_iff' := ⋯ }

Instances For

source
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
source
theorem OrderIso.map_bot {α : Type u_2} {β : Type u_3} [LE α] [PartialOrder β] [OrderBot α] [OrderBot β] (f : α ≃o β) :
f ⊥ = ⊥
source
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
source
theorem OrderIso.map_top {α : Type u_2} {β : Type u_3} [LE α] [PartialOrder β] [OrderTop α] [OrderTop β] (f : α ≃o β) :
f ⊤ = ⊤
source
theorem OrderEmbedding.map_inf_le {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [SemilatticeInf β] (f : α ↪o β) (x y : α) :
f (x ⊓ y) ≤ f x ⊓ f y
source
theorem OrderEmbedding.le_map_sup {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [SemilatticeSup β] (f : α ↪o β) (x y : α) :
f x ⊔ f y ≤ f (x ⊔ y)
source
theorem OrderIso.map_inf {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [SemilatticeInf β] (f : α ≃o β) (x y : α) :
f (x ⊓ y) = f x ⊓ f y
source
theorem OrderIso.map_sup {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [SemilatticeSup β] (f : α ≃o β) (x y : α) :
f (x ⊔ y) = f x ⊔ f y
source
theorem OrderIso.isMax_apply {α : Type u_6} {β : Type u_7} [Preorder α] [Preorder β] (f : α ≃o β) {x : α} :
IsMax (f x) ↔ IsMax x
source
theorem OrderIso.isMin_apply {α : Type u_6} {β : Type u_7} [Preorder α] [Preorder β] (f : α ≃o β) {x : α} :
IsMin (f x) ↔ IsMin x
source
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`

source
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`

source
@[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
source
@[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
source
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)
source
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)
source
theorem OrderIso.complementedLattice {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [ComplementedLattice α] (f : α ≃o β) :
ComplementedLattice β
source
theorem OrderIso.complementedLattice_iff {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : α ≃o β) :
ComplementedLattice α ↔ ComplementedLattice β
source
@[instance 90]
instance OrderIsoClass.toOrderIsoClassOrderDual {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [LE β] [EquivLike F α β] [OrderIsoClass F α β] :
OrderIsoClass F α ᵒᵈ β ᵒᵈ
source
theorem StrictMono.denselyOrdered_range {X : Type u_6} {Y : Type u_7} [LinearOrder X] [DenselyOrdered X] [Preorder Y] {f : X → Y} (hf : StrictMono f) :
DenselyOrdered ↑(Set.range f)
source
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) :
DenselyOrdered X ↔ DenselyOrdered Y
source
theorem denselyOrdered_iff_of_strictAnti {X : Type u_6} {Y : Type u_7} {F : Type u_8} [LinearOrder X] [Preorder Y] [EquivLike F X Y] (f : F) (hf : StrictAnti ⇑f) :
DenselyOrdered X ↔ DenselyOrdered Y
source
def ULift.orderIso {α : Type u} [Preorder α] :
ULift.{v, u} α ≃o α

The bijection `ULift.{v} α ≃ α` as an isomorphism of orders.

Equations

- ULift.orderIso.{?u.11, ?u.10} = Equiv.ulift.toOrderIso ⋯ ⋯

Instances For

source
@[simp]
theorem ULift.orderIso_apply {α : Type u} [Preorder α] (self : ULift.{v, u} α) :
orderIso.{v, u} self = self.down
source
@[simp]
theorem ULift.orderIso_symm_apply_down {α : Type u} [Preorder α] (down : α) :
((RelIso.symm orderIso.{v, u}) down).down = down