Order homomorphisms and sets #
Order isomorphism between two equal sets.
Equations
- OrderIso.setCongr s t h = { toEquiv := Equiv.setCongr h, map_rel_iff' := ⋯ }
Instances For
Order isomorphism between univ : Set α
and α
.
Equations
- OrderIso.Set.univ = { toEquiv := Equiv.Set.univ α, map_rel_iff' := ⋯ }
Instances For
noncomputable def
OrderEmbedding.orderIso
{α : Type u_1}
{β : Type u_2}
[LE α]
[LE β]
{f : α ↪o β}
:
We can regard an order embedding as an order isomorphism to its range.
Equations
- OrderEmbedding.orderIso = { toEquiv := Equiv.ofInjective ⇑f ⋯, map_rel_iff' := ⋯ }
Instances For
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
- StrictMonoOn.orderIso f s hf = { toEquiv := Set.BijOn.equiv f ⋯, map_rel_iff' := ⋯ }
Instances For
@[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.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
- StrictMono.orderIso f h_mono = { toEquiv := Equiv.ofInjective f ⋯, map_rel_iff' := ⋯ }
Instances For
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.
Equations
- StrictMono.orderIsoOfSurjective f h_mono h_surj = (StrictMono.orderIso f h_mono).trans ((OrderIso.setCongr (Set.range f) Set.univ ⋯).trans OrderIso.Set.univ)
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)
:
⇑(StrictMono.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 : α)
:
(StrictMono.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 ((StrictMono.orderIsoOfSurjective f h_mono h_surj).symm b) = b
theorem
OrderEmbedding.range_inj
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[WellFoundedLT α]
[Preorder β]
{f : α ↪o β}
{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 β)
Equations
- ⋯ = ⋯
instance
OrderIso.subsingleton_of_wellFoundedLT'
{α : Type u_1}
{β : Type u_2}
[LinearOrder β]
[WellFoundedLT β]
[Preorder α]
:
Subsingleton (α ≃o β)
Equations
- ⋯ = ⋯
Equations
- OrderIso.unique_of_wellFoundedLT = Unique.mk' (α ≃o α)
instance
OrderIso.subsingleton_of_wellFoundedGT
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[WellFoundedGT α]
[Preorder β]
:
Subsingleton (α ≃o β)
Equations
- ⋯ = ⋯
instance
OrderIso.subsingleton_of_wellFoundedGT'
{α : Type u_1}
{β : Type u_2}
[LinearOrder β]
[WellFoundedGT β]
[Preorder α]
:
Subsingleton (α ≃o β)
Equations
- ⋯ = ⋯
Equations
- OrderIso.unique_of_wellFoundedGT = Unique.mk' (α ≃o α)
@[simp]
theorem
OrderIso.compl_apply
(α : Type u_1)
[BooleanAlgebra α]
:
∀ (a : α), (OrderIso.compl α) a = (OrderDual.toDual a)ᶜ
@[simp]
theorem
OrderIso.compl_symm_apply
(α : Type u_1)
[BooleanAlgebra α]
:
∀ (a : αᵒᵈ), (RelIso.symm (OrderIso.compl α)) a = (OrderDual.ofDual a)ᶜ
Taking complements as an order isomorphism to the order dual.
Equations
- OrderIso.compl α = { toFun := ⇑OrderDual.toDual ∘ compl, invFun := compl ∘ ⇑OrderDual.ofDual, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }