intro y'
G : Type
inst✝¹ : Group G
X : Type u_1
Y : Type u_2
inst✝ : PartialOrder X
f : Y → X
hf : Function.Injective f
s : Set Y
y : Y
hy : isInf (f '' s) (f y)
⊢ isInf s y
G : Type
inst✝¹ : Group G
X : Type u_1
Y : Type u_2
inst✝ : PartialOrder X
f : Y → X
hf : Function.Injective f
s : Set Y
y : Y
hy : isInf (f '' s) (f y)
y' : Y
⊢ y' ∈ lowerBounds s ↔ y' ≤ y