Documentation

Mathlib.Order.Hom.Set

Order homomorphisms and sets #

theorem OrderIso.range_eq {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (e : α ≃o β) :
Set.range (RelIso.toRelEmbedding e).toEmbedding = Set.univ
@[simp]
theorem OrderIso.symm_image_image {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (e : α ≃o β) (s : Set α) :
(RelIso.toRelEmbedding (OrderIso.symm e)).toEmbedding '' ((RelIso.toRelEmbedding e).toEmbedding '' s) = s
@[simp]
theorem OrderIso.image_symm_image {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (e : α ≃o β) (s : Set β) :
(RelIso.toRelEmbedding e).toEmbedding '' ((RelIso.toRelEmbedding (OrderIso.symm e)).toEmbedding '' s) = s
theorem OrderIso.image_eq_preimage {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (e : α ≃o β) (s : Set α) :
(RelIso.toRelEmbedding e).toEmbedding '' s = (RelIso.toRelEmbedding (OrderIso.symm e)).toEmbedding ⁻¹' s
@[simp]
theorem OrderIso.preimage_symm_preimage {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (e : α ≃o β) (s : Set α) :
(RelIso.toRelEmbedding e).toEmbedding ⁻¹' ((RelIso.toRelEmbedding (OrderIso.symm e)).toEmbedding ⁻¹' s) = s
@[simp]
theorem OrderIso.symm_preimage_preimage {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (e : α ≃o β) (s : Set β) :
(RelIso.toRelEmbedding (OrderIso.symm e)).toEmbedding ⁻¹' ((RelIso.toRelEmbedding e).toEmbedding ⁻¹' s) = s
@[simp]
theorem OrderIso.image_preimage {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (e : α ≃o β) (s : Set β) :
(RelIso.toRelEmbedding e).toEmbedding '' ((RelIso.toRelEmbedding e).toEmbedding ⁻¹' s) = s
@[simp]
theorem OrderIso.preimage_image {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (e : α ≃o β) (s : Set α) :
(RelIso.toRelEmbedding e).toEmbedding ⁻¹' ((RelIso.toRelEmbedding e).toEmbedding '' s) = s
def OrderIso.setCongr {α : Type u_1} [inst : Preorder α] (s : Set α) (t : Set α) (h : s = t) :
s ≃o t

Order isomorphism between two equal sets.

Equations
  • One or more equations did not get rendered due to their size.
def OrderIso.Set.univ {α : Type u_1} [inst : Preorder α] :
Set.univ ≃o α

Order isomorphism between univ : Set α and α.

Equations
  • One or more equations did not get rendered due to their size.
noncomputable def StrictMonoOn.orderIso {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst : 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
@[simp]
theorem StrictMono.orderIso_apply {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst : Preorder β] (f : αβ) (h_mono : StrictMono f) (a : α) :
(RelIso.toRelEmbedding (StrictMono.orderIso f h_mono)).toEmbedding a = { val := f a, property := (_ : y, f y = f a) }
noncomputable def StrictMono.orderIso {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst : 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
noncomputable def StrictMono.orderIsoOfSurjective {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst : 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
  • One or more equations did not get rendered due to their size.
@[simp]
theorem StrictMono.coe_orderIsoOfSurjective {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst : Preorder β] (f : αβ) (h_mono : StrictMono f) (h_surj : Function.Surjective f) :
(RelIso.toRelEmbedding (StrictMono.orderIsoOfSurjective f h_mono h_surj)).toEmbedding = f
@[simp]
theorem StrictMono.orderIsoOfSurjective_symm_apply_self {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst : Preorder β] (f : αβ) (h_mono : StrictMono f) (h_surj : Function.Surjective f) (a : α) :
(RelIso.toRelEmbedding (OrderIso.symm (StrictMono.orderIsoOfSurjective f h_mono h_surj))).toEmbedding (f a) = a
theorem StrictMono.orderIsoOfSurjective_self_symm_apply {α : Type u_2} {β : Type u_1} [inst : LinearOrder α] [inst : Preorder β] (f : αβ) (h_mono : StrictMono f) (h_surj : Function.Surjective f) (b : β) :
f ((RelIso.toRelEmbedding (OrderIso.symm (StrictMono.orderIsoOfSurjective f h_mono h_surj))).toEmbedding b) = b
@[simp]
theorem OrderIso.compl_symm_apply (α : Type u_1) [inst : BooleanAlgebra α] :
∀ (a : αᵒᵈ), (RelIso.toRelEmbedding (RelIso.symm (OrderIso.compl α))).toEmbedding a = (compl OrderDual.ofDual) a
@[simp]
theorem OrderIso.compl_apply (α : Type u_1) [inst : BooleanAlgebra α] :
∀ (a : α), (RelIso.toRelEmbedding (OrderIso.compl α)).toEmbedding a = (OrderDual.toDual compl) a
def OrderIso.compl (α : Type u_1) [inst : BooleanAlgebra α] :

Taking complements as an order isomorphism to the order dual.

Equations
  • One or more equations did not get rendered due to their size.
theorem compl_strictAnti (α : Type u_1) [inst : BooleanAlgebra α] :
theorem compl_antitone (α : Type u_1) [inst : BooleanAlgebra α] :
Antitone compl