α : Type u_1
m : Set α → ℝ≥0∞
⊢ ∀ (s : Set α), Set.Nonempty s → ↑⊤ s ≤ ⊤ s
α : Type u_1
m : Set α → ℝ≥0∞
⊢ boundedBy ⊤ = ⊤
rw [eq_top_iff, le_boundedBy']
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : Set.Nonempty s
⊢ ↑⊤ s ≤ ⊤ s
α : Type u_1
m : Set α → ℝ≥0∞
⊢ ∀ (s : Set α), Set.Nonempty s → ↑⊤ s ≤ ⊤ s
intro s hs
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : Set.Nonempty s
⊢ ⊤ ≤ ⊤ s
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : Set.Nonempty s
⊢ ↑⊤ s ≤ ⊤ s
rw [top_apply hs]
no goals
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : Set.Nonempty s
⊢ ⊤ ≤ ⊤ s
exact le_rfl