case intro
F : Type ?u.11263
α : Type u_2
β : Type u_1
γ : Type ?u.11272
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b : β
q✝ : ℚ
inst✝ : Archimedean α
a : α
q : ℚ
hq : a < ↑q
⊢ BddAbove (cutMap β a)
F : Type ?u.11263
α : Type u_2
β : Type u_1
γ : Type ?u.11272
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b : β
q : ℚ
inst✝ : Archimedean α
a : α
⊢ BddAbove (cutMap β a)
obtain ⟨q, hq⟩ := exists_rat_gt a
no goals
case intro
F : Type ?u.11263
α : Type u_2
β : Type u_1
γ : Type ?u.11272
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b : β
q✝ : ℚ
inst✝ : Archimedean α
a : α
q : ℚ
hq : a < ↑q
⊢ BddAbove (cutMap β a)
exact ⟨q, ball_image_iff.2 fun r hr => by exact_mod_cast (hq.trans' hr).le⟩
no goals
F : Type ?u.11263
α : Type u_2
β : Type u_1
γ : Type ?u.11272
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b : β
q✝ : ℚ
inst✝ : Archimedean α
a : α
q : ℚ
hq : a < ↑q
r : ℚ
hr : r ∈ {t | ↑t < a}
⊢ ↑r ≤ ↑q
exact_mod_cast (hq.trans' hr).le