Order homomorphisms and sets

def Set.sumEquiv {α : Type u_1} {β : Type u_2} : Set (α ⊕ β) ≃o Set α × Set β

Sets on sum types are order-equivalent to pairs of sets on each summand.

@[simp]

theorem Set.sumEquiv_apply {α : Type u_1} {β : Type u_2} (s : Set (α ⊕ β)) : sumEquiv s = (Sum.inl ⁻¹' s, Sum.inr ⁻¹' s)

@[simp]

theorem Set.sumEquiv_symm_apply {α : Type u_1} {β : Type u_2} {s : Set α × Set β} : sumEquiv.symm s = Sum.inl '' s.1 ∪ Sum.inr '' s.2

theorem Set.MapsTo.sumElim {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → γ} {g : β → γ} {s : Set α × Set β} {t : Set γ} (hf : MapsTo f s.1 t) (hg : MapsTo g s.2 t) : MapsTo (Sum.elim f g) (sumEquiv.symm s) t

theorem Set.InjOn.sumElim {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → γ} {g : β → γ} {s : Set α × Set β} (hf : InjOn f s.1) (hg : InjOn g s.2) (hfg : ∀ (a : α), a ∈ s.1 → ∀ (b : β), b ∈ s.2 → f a ≠ g b) : InjOn (Sum.elim f g) (sumEquiv.symm s)

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

Order isomorphism between two equal sets.

@[simp]

theorem Set.orderIsoOfEq_apply {α : Type u_1} [Preorder α] (s t : Set α) (h : s = t) (a : { a : α // (fun (x : α) => x ∈ s) a }) : (s.orderIsoOfEq t h) a = ⟨↑a, ⋯⟩

@[simp]

theorem Set.orderIsoOfEq_symm_apply {α : Type u_1} [Preorder α] (s t : Set α) (h : s = t) (b : { b : α // (fun (x : α) => x ∈ t) b }) : (RelIso.symm (s.orderIsoOfEq t h)) b = ⟨↑b, ⋯⟩

@[deprecated Set.orderIsoOfEq (since := "2026-08-29")]

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

Alias of Set.orderIsoOfEq.

---

Order isomorphism between two equal sets.

@[deprecated Set.orderIsoOfEq_apply (since := "2026-08-29")]

theorem OrderIso.Set.congr_apply {α : Type u_1} [Preorder α] (s t : Set α) (h : s = t) (a : { a : α // (fun (x : α) => x ∈ s) a }) : (s.orderIsoOfEq t h) a = ⟨↑a, ⋯⟩

Alias of Set.orderIsoOfEq_apply.

@[deprecated Set.orderIsoOfEq_symm_apply (since := "2026-08-29")]

theorem OrderIso.Set.congr_symm_apply {α : Type u_1} [Preorder α] (s t : Set α) (h : s = t) (b : { b : α // (fun (x : α) => x ∈ t) b }) : (RelIso.symm (s.orderIsoOfEq t h)) b = ⟨↑b, ⋯⟩

Alias of Set.orderIsoOfEq_symm_apply.

theorem OrderIso.range_eq {α : Type u_1} {β : Type u_2} [LE α] [LE β] (e : α ≃o β) : Set.range ⇑e = _root_.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_symm {α : 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

@[deprecated Set.orderIsoOfEq (since := "2026-08-21")]

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

Alias of Set.orderIsoOfEq.

---

Order isomorphism between two equal sets.

@[deprecated Set.orderIsoOfEq_apply (since := "2026-08-21")]

theorem OrderIso.setCongr_apply {α : Type u_1} [Preorder α] (s t : Set α) (h : s = t) (a : { a : α // (fun (x : α) => x ∈ s) a }) : (s.orderIsoOfEq t h) a = ⟨↑a, ⋯⟩

Alias of Set.orderIsoOfEq_apply.

@[deprecated Set.orderIsoOfEq_symm_apply (since := "2026-08-21")]

theorem OrderIso.setCongr_symm_apply {α : Type u_1} [Preorder α] (s t : Set α) (h : s = t) (b : { b : α // (fun (x : α) => x ∈ t) b }) : (RelIso.symm (s.orderIsoOfEq t h)) b = ⟨↑b, ⋯⟩

Alias of Set.orderIsoOfEq_symm_apply.

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

Order isomorphism between univ : Set α and α.

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.

@[simp]

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

noncomputable def StrictMonoOn.orderIso {α : Type u_4} {β : Type u_5} [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.

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.

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

@[simp]

theorem StrictMono.coe_orderIsoOfSurjective {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] (f : α → β) (h_mono : StrictMono f) (h_surj : Function.Surjective f) : ⇑(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 : α) : (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 ((orderIsoOfSurjective f h_mono h_surj).symm b) = b

theorem OrderEmbedding.eq_of_range_eq {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [Subsingleton (α ≃o α)] {f g : α ↪o β} (h : Set.range ⇑f = Set.range ⇑g) : f = g

Two order embeddings with the same range are equal if their domain has no nontrivial order automorphisms.

theorem StrictMono.eq_of_range_eq {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] [Subsingleton (α ≃o α)] {f g : α → β} (hf : StrictMono f) (hg : StrictMono g) (h : Set.range f = Set.range g) : f = g

Two strictly monotone functions are equal provided that their ranges are equal, assuming the type of order automorphisms of the domain is a subsingleton.

theorem OrderEmbedding.range_inj_of_wellFoundedLT {α : Type u_1} {β : Type u_2} [LinearOrder α] [WellFoundedLT α] [Preorder β] {f 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.

theorem OrderEmbedding.range_inj_of_wellFoundedGT {α : Type u_1} {β : Type u_2} [LinearOrder α] [WellFoundedGT α] [Preorder β] {f 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.

@[deprecated OrderEmbedding.range_inj_of_wellFoundedLT (since := "2026-08-13")]

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

Alias of OrderEmbedding.range_inj_of_wellFoundedLT.

---

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 β)

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

@[instance_reducible]

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

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

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

@[instance_reducible]

instance OrderIso.unique_of_wellFoundedGT {α : Type u_1} [LinearOrder α] [WellFoundedGT α] : Unique (α ≃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.

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.

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.

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

Taking complements as an order isomorphism to the order dual.

@[simp]

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

@[simp]

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

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

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