Finite_Union_of_Bounded_Subsets

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

boundednessproofwiki

Let $M = \left({A, d}\right)$ be a metric space. Then the union of any finite number of bounded subsets of $M$ is itself bounded.

Preamble

import Mathlib.Topology.MetricSpace.Basic

Formal statement

theorem Finite_Union_of_Bounded_Subsets {α : Type _} [PseudoMetricSpace α] {S₁ S₂ : Set α} (h₁ : Bornology.IsBounded S₁) (h₂ : Bornology.IsBounded S₂) : Bornology.IsBounded (S₁ ∪ S₂) := by sorry

Source

https://proofwiki.org/wiki/Finite_Union_of_Bounded_Subsets

View graph