Order homomorphisms and sets #
noncomputable def
StrictMonoOn.orderIso
{α : Type u_3}
{β : Type u_4}
[LinearOrder α]
[Preorder β]
(f : α → β)
(s : Set α)
(hf : StrictMonoOn 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
Instances For
noncomputable def
StrictMono.orderIso
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[Preorder β]
(f : α → β)
(h_mono : StrictMono f)
:
A strictly monotone function from a linear order is an order isomorphism between its domain and its range.
Equations
Instances For
@[simp]
theorem
StrictMono.orderIso_apply
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[Preorder β]
(f : α → β)
(h_mono : StrictMono f)
(a : α)
:
noncomputable def
StrictMono.orderIsoOfSurjective
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[Preorder β]
(f : α → β)
(h_mono : StrictMono f)
(h_surj : Function.Surjective f)
:
A strictly monotone surjective function from a linear order is an order isomorphism.
Equations
Instances For
@[simp]
theorem
StrictMono.coe_orderIsoOfSurjective
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[Preorder β]
(f : α → β)
(h_mono : StrictMono f)
(h_surj : Function.Surjective 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 : α)
:
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 : β)
:
theorem
OrderEmbedding.range_inj
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[WellFoundedLT α]
[Preorder β]
{f g : α ↪o β}
:
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 β)
Equations
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 β)
Equations
Taking complements as an order isomorphism to the order dual.
Equations
Instances For
@[simp]
@[simp]