x y : ℝ
S : Set ℝ
h₁ : Set.Nonempty S
h₂ : BddBelow S
⊢ IsLUB (-S) (sSup (-S))
x y : ℝ
S : Set ℝ
h₁ : Set.Nonempty S
h₂ : BddBelow S
⊢ IsGLB S (sInf S)
rw [sInf_def, ← isLUB_neg', neg_neg]
no goals
x y : ℝ
S : Set ℝ
h₁ : Set.Nonempty S
h₂ : BddBelow S
⊢ IsLUB (-S) (sSup (-S))
exact Real.isLUB_sSup _ h₁.neg h₂.neg