Order homomorphisms and sets

theorem OrderIso.range_eq {α : Type u_1} {β : Type u_2} [LE α] [LE β] (e : α ≃o β) : Set.range ⇑e = Set.univ

@[simp]

theorem OrderIso.symm_image_image {α : Type u_1} {β : Type u_2} [LE α] [LE β] (e : α ≃o β) (s : Set α) : ⇑e.symm '' (⇑e '' s) = s

@[simp]

theorem OrderIso.image_symm_image {α : Type u_1} {β : Type u_2} [LE α] [LE β] (e : α ≃o β) (s : Set β) : ⇑e '' (⇑e.symm '' s) = s

theorem OrderIso.image_eq_preimage {α : Type u_1} {β : Type u_2} [LE α] [LE β] (e : α ≃o β) (s : Set α) : ⇑e '' s = ⇑e.symm ⁻¹' s

@[simp]

theorem OrderIso.preimage_symm_preimage {α : Type u_1} {β : Type u_2} [LE α] [LE β] (e : α ≃o β) (s : Set α) : ⇑e ⁻¹' (⇑e.symm ⁻¹' s) = s

@[simp]

theorem OrderIso.symm_preimage_preimage {α : Type u_1} {β : Type u_2} [LE α] [LE β] (e : α ≃o β) (s : Set β) : ⇑e.symm ⁻¹' (⇑e ⁻¹' s) = s

@[simp]

theorem OrderIso.image_preimage {α : Type u_1} {β : Type u_2} [LE α] [LE β] (e : α ≃o β) (s : Set β) : ⇑e '' (⇑e ⁻¹' s) = s

@[simp]

theorem OrderIso.preimage_image {α : Type u_1} {β : Type u_2} [LE α] [LE β] (e : α ≃o β) (s : Set α) : ⇑e ⁻¹' (⇑e '' s) = s

def OrderIso.setCongr {α : Type u_1} [Preorder α] (s : Set α) (t : Set α) (h : s = t) : ↑s ≃o ↑t

Order isomorphism between two equal sets.

Equations

• OrderIso.setCongr s t h = { toEquiv := Equiv.setCongr h, map_rel_iff' := ⋯ }

def OrderIso.Set.univ {α : Type u_1} [Preorder α] : ↑Set.univ ≃o α

Order isomorphism between univ : Set α and α.

Equations

• OrderIso.Set.univ = { toEquiv := Equiv.Set.univ α, map_rel_iff' := ⋯ }

@[simp]

theorem OrderEmbedding.orderIso_apply {α : Type u_1} {β : Type u_2} [LE α] [LE β] {f : α ↪o β} (a : α) : OrderEmbedding.orderIso a = ⟨f a, ⋯⟩

noncomputable def OrderEmbedding.orderIso {α : Type u_1} {β : Type u_2} [LE α] [LE β] {f : α ↪o β} : α ≃o ↑(Set.range ⇑f)

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

Equations

• OrderEmbedding.orderIso = { toEquiv := Equiv.ofInjective ⇑f ⋯, map_rel_iff' := ⋯ }

noncomputable def StrictMonoOn.orderIso {α : Type u_3} {β : Type u_4} [LinearOrder α] [Preorder β] (f : α → β) (s : Set α) (hf : StrictMonoOn f s) : ↑s ≃o ↑(f '' s)

If a function f is strictly monotone on a set s, then it defines an order isomorphism between s and its image.

Equations

• StrictMonoOn.orderIso f s hf = { toEquiv := Set.BijOn.equiv f ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem StrictMono.orderIso_apply {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] (f : α → β) (h_mono : StrictMono f) (a : α) : (StrictMono.orderIso f h_mono) a = ⟨f a, ⋯⟩

noncomputable def StrictMono.orderIso {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] (f : α → β) (h_mono : StrictMono f) : α ≃o ↑(Set.range f)

A strictly monotone function from a linear order is an order isomorphism between its domain and its range.

Equations

• StrictMono.orderIso f h_mono = { toEquiv := Equiv.ofInjective f ⋯, map_rel_iff' := ⋯ }

noncomputable def StrictMono.orderIsoOfSurjective {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] (f : α → β) (h_mono : StrictMono f) (h_surj : Function.Surjective f) : α ≃o β

A strictly monotone surjective function from a linear order is an order isomorphism.

Equations

• StrictMono.orderIsoOfSurjective f h_mono h_surj = (StrictMono.orderIso f h_mono).trans ((OrderIso.setCongr (Set.range f) Set.univ ⋯).trans OrderIso.Set.univ)

@[simp]

theorem StrictMono.coe_orderIsoOfSurjective {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] (f : α → β) (h_mono : StrictMono f) (h_surj : Function.Surjective f) : ⇑(StrictMono.orderIsoOfSurjective f h_mono h_surj) = f

@[simp]

theorem StrictMono.orderIsoOfSurjective_symm_apply_self {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] (f : α → β) (h_mono : StrictMono f) (h_surj : Function.Surjective f) (a : α) : (StrictMono.orderIsoOfSurjective f h_mono h_surj).symm (f a) = a

theorem StrictMono.orderIsoOfSurjective_self_symm_apply {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] (f : α → β) (h_mono : StrictMono f) (h_surj : Function.Surjective f) (b : β) : f ((StrictMono.orderIsoOfSurjective f h_mono h_surj).symm b) = b

theorem OrderEmbedding.range_inj {α : Type u_1} {β : Type u_2} [LinearOrder α] [WellFoundedLT α] [Preorder β] {f : α ↪o β} {g : α ↪o β} : Set.range ⇑f = Set.range ⇑g ↔ f = g

Two order embeddings on a well-order are equal provided that their ranges are equal.

instance OrderIso.subsingleton_of_wellFoundedLT {α : Type u_1} {β : Type u_2} [LinearOrder α] [WellFoundedLT α] [Preorder β] : Subsingleton (α ≃o β)

Equations

• ⋯ = ⋯

instance OrderIso.subsingleton_of_wellFoundedLT' {α : Type u_1} {β : Type u_2} [LinearOrder β] [WellFoundedLT β] [Preorder α] : Subsingleton (α ≃o β)

Equations

• ⋯ = ⋯

instance OrderIso.unique_of_wellFoundedLT {α : Type u_1} [LinearOrder α] [WellFoundedLT α] : Unique (α ≃o α)

Equations

• OrderIso.unique_of_wellFoundedLT = Unique.mk' (α ≃o α)

instance OrderIso.subsingleton_of_wellFoundedGT {α : Type u_1} {β : Type u_2} [LinearOrder α] [WellFoundedGT α] [Preorder β] : Subsingleton (α ≃o β)

Equations

• ⋯ = ⋯

instance OrderIso.subsingleton_of_wellFoundedGT' {α : Type u_1} {β : Type u_2} [LinearOrder β] [WellFoundedGT β] [Preorder α] : Subsingleton (α ≃o β)

Equations

• ⋯ = ⋯

instance OrderIso.unique_of_wellFoundedGT {α : Type u_1} [LinearOrder α] [WellFoundedGT α] : Unique (α ≃o α)

Equations

• OrderIso.unique_of_wellFoundedGT = Unique.mk' (α ≃o α)

def OrderIso.Iic {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (e : α ≃o β) (x : α) : ↑(Set.Iic x) ≃o ↑(Set.Iic (e x))

An order isomorphism between lattices induces an order isomorphism between corresponding interval sublattices.

Equations

• e.Iic x = { toFun := fun (y : ↑(Set.Iic x)) => ⟨e ↑y, ⋯⟩, invFun := fun (y : ↑(Set.Iic (e x))) => ⟨e.symm ↑y, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

def OrderIso.Ici {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (e : α ≃o β) (x : α) : ↑(Set.Ici x) ≃o ↑(Set.Ici (e x))

An order isomorphism between lattices induces an order isomorphism between corresponding interval sublattices.

Equations

• e.Ici x = { toFun := fun (y : ↑(Set.Ici x)) => ⟨e ↑y, ⋯⟩, invFun := fun (y : ↑(Set.Ici (e x))) => ⟨e.symm ↑y, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

def OrderIso.Icc {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (e : α ≃o β) (x : α) (y : α) : ↑(Set.Icc x y) ≃o ↑(Set.Icc (e x) (e y))

An order isomorphism between lattices induces an order isomorphism between corresponding interval sublattices.

Equations

• e.Icc x y = { toFun := fun (z : ↑(Set.Icc x y)) => ⟨e ↑z, ⋯⟩, invFun := fun (z : ↑(Set.Icc (e x) (e y))) => ⟨e.symm ↑z, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.compl_symm_apply (α : Type u_1) [BooleanAlgebra α] : ∀ (a : αᵒᵈ), (RelIso.symm (OrderIso.compl α)) a = (OrderDual.ofDual a)ᶜ

@[simp]

theorem OrderIso.compl_apply (α : Type u_1) [BooleanAlgebra α] : ∀ (a : α), (OrderIso.compl α) a = (OrderDual.toDual a)ᶜ

def OrderIso.compl (α : Type u_1) [BooleanAlgebra α] : α ≃o αᵒᵈ

Taking complements as an order isomorphism to the order dual.

Equations

• OrderIso.compl α = { toFun := ⇑OrderDual.toDual ∘ compl, invFun := compl ∘ ⇑OrderDual.ofDual, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

theorem compl_strictAnti (α : Type u_1) [BooleanAlgebra α] : StrictAnti compl

theorem compl_antitone (α : Type u_1) [BooleanAlgebra α] : Antitone compl