mathlib3 documentation

order.bounds.order_iso

Order isomorhpisms and bounds. #

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

source
theorem order_iso.upper_bounds_image {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) {s : set α} :
upper_bounds (⇑f '' s) = ⇑f '' upper_bounds s
source
theorem order_iso.lower_bounds_image {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) {s : set α} :
lower_bounds (⇑f '' s) = ⇑f '' lower_bounds s
source
@[simp]
theorem order_iso.is_lub_image {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) {s : set α} {x : β} :
is_lub (⇑f '' s) x ↔ is_lub s (⇑(f.symm) x)
source
theorem order_iso.is_lub_image' {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) {s : set α} {x : α} :
is_lub (⇑f '' s) (⇑f x) ↔ is_lub s x
source
@[simp]
theorem order_iso.is_glb_image {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) {s : set α} {x : β} :
is_glb (⇑f '' s) x ↔ is_glb s (⇑(f.symm) x)
source
theorem order_iso.is_glb_image' {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) {s : set α} {x : α} :
is_glb (⇑f '' s) (⇑f x) ↔ is_glb s x
source
@[simp]
theorem order_iso.is_lub_preimage {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) {s : set β} {x : α} :
is_lub (⇑f ⁻¹' s) x ↔ is_lub s (⇑f x)
source
theorem order_iso.is_lub_preimage' {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) {s : set β} {x : β} :
is_lub (⇑f ⁻¹' s) (⇑(f.symm) x) ↔ is_lub s x
source
@[simp]
theorem order_iso.is_glb_preimage {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) {s : set β} {x : α} :
is_glb (⇑f ⁻¹' s) x ↔ is_glb s (⇑f x)
source
theorem order_iso.is_glb_preimage' {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) {s : set β} {x : β} :
is_glb (⇑f ⁻¹' s) (⇑(f.symm) x) ↔ is_glb s x