Documentation
Mathlib
.
Order
.
Set
Search
return to top
source
Imports
Init
Mathlib.Order.TypeTags
Mathlib.Data.Set.Image
Imported by
WithBot
.
range_eq
WithTop
.
range_eq
Set.range
on
WithBot
and
WithTop
#
source
theorem
WithBot
.
range_eq
{
α
:
Type
u_1}
{
β
:
Type
u_2}
(
f
:
WithBot
α
→
β
)
:
Set.range
f
=
insert
(
f
⊥
)
(
Set.range
(
f
∘
some
))
source
theorem
WithTop
.
range_eq
{
α
:
Type
u_1}
{
β
:
Type
u_2}
(
f
:
WithTop
α
→
β
)
:
Set.range
f
=
insert
(
f
⊤
)
(
Set.range
(
f
∘
WithBot.some
))