Documentation
Mathlib
.
Order
.
Bounds
.
OrderIso
Search
return to top
source
Imports
Init
Mathlib.Order.Bounds.Image
Mathlib.Order.Hom.Set
Imported by
OrderIso
.
upperBounds_image
OrderIso
.
lowerBounds_image
OrderIso
.
isLUB_image
OrderIso
.
isLUB_image'
OrderIso
.
isGLB_image
OrderIso
.
isGLB_image'
OrderIso
.
isLUB_preimage
OrderIso
.
isLUB_preimage'
OrderIso
.
isGLB_preimage
OrderIso
.
isGLB_preimage'
Order isomorphisms and bounds.
#
source
theorem
OrderIso
.
upperBounds_image
{α :
Type
u_1}
{β :
Type
u_2}
[
Preorder
α
]
[
Preorder
β
]
(f :
α
≃o
β
)
{s :
Set
α
}
:
upperBounds
(
⇑
f
''
s
)
=
⇑
f
''
upperBounds
s
source
theorem
OrderIso
.
lowerBounds_image
{α :
Type
u_1}
{β :
Type
u_2}
[
Preorder
α
]
[
Preorder
β
]
(f :
α
≃o
β
)
{s :
Set
α
}
:
lowerBounds
(
⇑
f
''
s
)
=
⇑
f
''
lowerBounds
s
source
@[simp]
theorem
OrderIso
.
isLUB_image
{α :
Type
u_1}
{β :
Type
u_2}
[
Preorder
α
]
[
Preorder
β
]
(f :
α
≃o
β
)
{s :
Set
α
}
{x :
β
}
:
IsLUB
(
⇑
f
''
s
)
x
↔
IsLUB
s
(
f
.
symm
x
)
source
theorem
OrderIso
.
isLUB_image'
{α :
Type
u_1}
{β :
Type
u_2}
[
Preorder
α
]
[
Preorder
β
]
(f :
α
≃o
β
)
{s :
Set
α
}
{x :
α
}
:
IsLUB
(
⇑
f
''
s
)
(
f
x
)
↔
IsLUB
s
x
source
@[simp]
theorem
OrderIso
.
isGLB_image
{α :
Type
u_1}
{β :
Type
u_2}
[
Preorder
α
]
[
Preorder
β
]
(f :
α
≃o
β
)
{s :
Set
α
}
{x :
β
}
:
IsGLB
(
⇑
f
''
s
)
x
↔
IsGLB
s
(
f
.
symm
x
)
source
theorem
OrderIso
.
isGLB_image'
{α :
Type
u_1}
{β :
Type
u_2}
[
Preorder
α
]
[
Preorder
β
]
(f :
α
≃o
β
)
{s :
Set
α
}
{x :
α
}
:
IsGLB
(
⇑
f
''
s
)
(
f
x
)
↔
IsGLB
s
x
source
@[simp]
theorem
OrderIso
.
isLUB_preimage
{α :
Type
u_1}
{β :
Type
u_2}
[
Preorder
α
]
[
Preorder
β
]
(f :
α
≃o
β
)
{s :
Set
β
}
{x :
α
}
:
IsLUB
(
⇑
f
⁻¹'
s
)
x
↔
IsLUB
s
(
f
x
)
source
theorem
OrderIso
.
isLUB_preimage'
{α :
Type
u_1}
{β :
Type
u_2}
[
Preorder
α
]
[
Preorder
β
]
(f :
α
≃o
β
)
{s :
Set
β
}
{x :
β
}
:
IsLUB
(
⇑
f
⁻¹'
s
)
(
f
.
symm
x
)
↔
IsLUB
s
x
source
@[simp]
theorem
OrderIso
.
isGLB_preimage
{α :
Type
u_1}
{β :
Type
u_2}
[
Preorder
α
]
[
Preorder
β
]
(f :
α
≃o
β
)
{s :
Set
β
}
{x :
α
}
:
IsGLB
(
⇑
f
⁻¹'
s
)
x
↔
IsGLB
s
(
f
x
)
source
theorem
OrderIso
.
isGLB_preimage'
{α :
Type
u_1}
{β :
Type
u_2}
[
Preorder
α
]
[
Preorder
β
]
(f :
α
≃o
β
)
{s :
Set
β
}
{x :
β
}
:
IsGLB
(
⇑
f
⁻¹'
s
)
(
f
.
symm
x
)
↔
IsGLB
s
x