Heine–Borel theorem
Closed
Theorem & proof
·
heine_borel.lean
·
✓ verified
1
2
3
4
import Mathlib theorem heine_borel (s : Set ℝ) : IsCompact s ↔ IsClosed s ∧ Bornology.IsBounded s := Metric.isCompact_iff_isClosed_bounded
Rewards pledged
No rewards pledged yet.