mathlib3 documentation

order.hom.set

Order homomorphisms and sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem order_iso.range_eq {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) :
@[simp]
theorem order_iso.symm_image_image {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) (s : set α) :
(e.symm) '' (e '' s) = s
@[simp]
theorem order_iso.image_symm_image {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) (s : set β) :
e '' ((e.symm) '' s) = s
theorem order_iso.image_eq_preimage {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) (s : set α) :
e '' s = (e.symm) ⁻¹' s
@[simp]
theorem order_iso.preimage_symm_preimage {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) (s : set α) :
@[simp]
theorem order_iso.symm_preimage_preimage {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) (s : set β) :
@[simp]
theorem order_iso.image_preimage {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) (s : set β) :
e '' (e ⁻¹' s) = s
@[simp]
theorem order_iso.preimage_image {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) (s : set α) :
e ⁻¹' (e '' s) = s
def order_iso.set_congr {α : Type u_2} [preorder α] (s t : set α) (h : s = t) :

Order isomorphism between two equal sets.

Equations
def order_iso.set.univ {α : Type u_2} [preorder α] :

Order isomorphism between univ : set α and α.

Equations
@[protected]
noncomputable def strict_mono_on.order_iso {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] (f : α β) (s : set α) (hf : strict_mono_on 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 strict_mono.order_iso_apply {α : Type u_2} {β : Type u_3} [linear_order α] [preorder β] (f : α β) (h_mono : strict_mono f) (a : α) :
(strict_mono.order_iso f h_mono) a = f a, _⟩
@[protected]
noncomputable def strict_mono.order_iso {α : Type u_2} {β : Type u_3} [linear_order α] [preorder β] (f : α β) (h_mono : strict_mono f) :

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

Equations
noncomputable def strict_mono.order_iso_of_surjective {α : Type u_2} {β : Type u_3} [linear_order α] [preorder β] (f : α β) (h_mono : strict_mono f) (h_surj : function.surjective f) :
α ≃o β

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

Equations
@[simp]
theorem strict_mono.coe_order_iso_of_surjective {α : Type u_2} {β : Type u_3} [linear_order α] [preorder β] (f : α β) (h_mono : strict_mono f) (h_surj : function.surjective f) :
@[simp]
theorem strict_mono.order_iso_of_surjective_symm_apply_self {α : Type u_2} {β : Type u_3} [linear_order α] [preorder β] (f : α β) (h_mono : strict_mono f) (h_surj : function.surjective f) (a : α) :
((strict_mono.order_iso_of_surjective f h_mono h_surj).symm) (f a) = a
theorem strict_mono.order_iso_of_surjective_self_symm_apply {α : Type u_2} {β : Type u_3} [linear_order α] [preorder β] (f : α β) (h_mono : strict_mono f) (h_surj : function.surjective f) (b : β) :
f (((strict_mono.order_iso_of_surjective f h_mono h_surj).symm) b) = b
@[simp]
def order_iso.compl (α : Type u_2) [boolean_algebra α] :

Taking complements as an order isomorphism to the order dual.

Equations