Union_of_Open_Sets_of_Metric_Space_is_Open

Proved

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

open-setsproofwikiset-union

Let $M = \struct {A, d}$ be a metric space. The union of a set of open sets of $M$ is open in $M$ .

Preamble

import Mathlib.Topology.MetricSpace.Basic

Formal statement

theorem Union_of_Open_Sets_of_Metric_Space_is_Open {α : Type _} [MetricSpace α] {ι : Sort _} (S : ι → Set α) (h : ∀ i, IsOpen (S i)) : IsOpen (⋃ i, S i) := by sorry

Source

https://proofwiki.org/wiki/Union_of_Open_Sets_of_Metric_Space_is_Open

View graph