Order homomorphisms and sets

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Order isomorphism between two equal sets.

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

Order isomorphism between univ : Set α and α.

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

@[simp]

theorem StrictMono.orderIso_apply {α : Type u_2} {β : Type u_3} [LinearOrder α] [Preorder β] (f : α → β) (h_mono : StrictMono f) (a : α) : ↑(StrictMono.orderIso f h_mono) a = { val := f a, property := (_ : ∃ y, f y = f a) }

noncomputable def StrictMono.orderIso {α : Type u_2} {β : Type u_3} [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.

noncomputable def StrictMono.orderIsoOfSurjective {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [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_2} {β : Type u_3} [LinearOrder α] [Preorder β] (f : α → β) (h_mono : StrictMono f) (h_surj : Function.Surjective f) (a : α) : ↑(OrderIso.symm (StrictMono.orderIsoOfSurjective f h_mono h_surj)) (f a) = a

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

@[simp]

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

@[simp]

theorem OrderIso.compl_apply (α : Type u_2) [BooleanAlgebra α] : ∀ (a : α), ↑(OrderIso.compl α) a = (↑OrderDual.toDual ∘ compl) a

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

Taking complements as an order isomorphism to the order dual.

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

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