order.bounds.order_iso - mathlib3 docs

theorem order_iso.upper_bounds_image {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) {s : set α} :

theorem order_iso.lower_bounds_image {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) {s : set α} :

@[simp]

theorem order_iso.is_lub_image {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) {s : set α} {x : β} :

theorem order_iso.is_lub_image' {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) {s : set α} {x : α} :

@[simp]

theorem order_iso.is_glb_image {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) {s : set α} {x : β} :

theorem order_iso.is_glb_image' {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) {s : set α} {x : α} :

@[simp]

theorem order_iso.is_lub_preimage {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) {s : set β} {x : α} :

theorem order_iso.is_lub_preimage' {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) {s : set β} {x : β} :

@[simp]

theorem order_iso.is_glb_preimage {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) {s : set β} {x : α} :

theorem order_iso.is_glb_preimage' {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) {s : set β} {x : β} :

mathlib3 documentation