Documentation
Foundation
.
Vorspiel
.
Small
Search
return to top
source
Imports
Init
Mathlib.Logic.Small.Basic
Imported by
small_preimage_of_injective
source
theorem
small_preimage_of_injective
{
α
:
Type
u_1}
{
β
:
Type
u_2}
(
f
:
α
→
β
)
(
h
:
Function.Injective
f
)
(
s
:
Set
β
)
[
Small.{u, u_2}
↑
s
]
:
Small.{u, u_1}
↑(
f
⁻¹'
s
)