order.hom.set - mathlib3 docs

source

theorem order_iso.range_eq {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) :

set.range ⇑e = set.univ

source

@[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

source

@[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

source

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

source

@[simp]

theorem order_iso.preimage_symm_preimage {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) (s : set α) :

⇑e ⁻¹' (⇑(e.symm) ⁻¹' s) = s

source

@[simp]

theorem order_iso.symm_preimage_preimage {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) (s : set β) :

⇑(e.symm) ⁻¹' (⇑e ⁻¹' s) = s

source

@[simp]

theorem order_iso.image_preimage {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) (s : set β) :

⇑e '' (⇑e ⁻¹' s) = s

source

@[simp]

theorem order_iso.preimage_image {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) (s : set α) :

⇑e ⁻¹' (⇑e '' s) = s

source

def order_iso.set_congr {α : Type u_2} [preorder α] (s t : set α) (h : s = t) :

↥s ≃o ↥t

Order isomorphism between two equal sets.

Equations

order_iso.set_congr s t h = {to_equiv := equiv.set_congr h, map_rel_iff' := _}

source

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

↥set.univ ≃o α

Order isomorphism between univ : set α and α.

Equations

order_iso.set.univ = {to_equiv := equiv.set.univ α, map_rel_iff' := _}

source

@[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

strict_mono_on.order_iso f s hf = {to_equiv := set.bij_on.equiv f _, map_rel_iff' := _}

source

@[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, _⟩

source

@[protected]

noncomputable def strict_mono.order_iso {α : Type u_2} {β : Type u_3} [linear_order α] [preorder β] (f : α → β) (h_mono : strict_mono f) :

α ≃o ↥(set.range f)

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

Equations

strict_mono.order_iso f h_mono = {to_equiv := equiv.of_injective f _, map_rel_iff' := _}

source

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

strict_mono.order_iso_of_surjective f h_mono h_surj = (strict_mono.order_iso f h_mono).trans ((order_iso.set_congr (set.range f) set.univ _).trans order_iso.set.univ)

source

@[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) :

⇑(strict_mono.order_iso_of_surjective f h_mono h_surj) = f

source

@[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

source

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

source

@[simp]

theorem order_iso.compl_apply (α : Type u_2) [boolean_algebra α] (ᾰ : α) :

⇑(order_iso.compl α) ᾰ = (⇑order_dual.to_dual ∘ has_compl.compl) ᾰ

source

def order_iso.compl (α : Type u_2) [boolean_algebra α] :

α ≃o αᵒᵈ

Taking complements as an order isomorphism to the order dual.

Equations

order_iso.compl α = {to_equiv := {to_fun := ⇑order_dual.to_dual ∘ has_compl.compl, inv_fun := has_compl.compl ∘ ⇑order_dual.of_dual, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

@[simp]

theorem order_iso.compl_symm_apply (α : Type u_2) [boolean_algebra α] (ᾰ : αᵒᵈ) :

⇑(rel_iso.symm (order_iso.compl α)) ᾰ = (has_compl.compl ∘ ⇑order_dual.of_dual) ᾰ

source

theorem compl_strict_anti (α : Type u_2) [boolean_algebra α] :

strict_anti has_compl.compl

source

theorem compl_antitone (α : Type u_2) [boolean_algebra α] :

antitone has_compl.compl

mathlib3 documentation

Order homomorphisms and sets #