Finite_Intersection_of_Open_Sets_of_Metric_Space_is_Open

Proved

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

open-setsproofwikiset-intersection

Let $M = \struct {A, d}$ be a metric space. Let $U_1, U_2, \ldots, U_n$ be open in $M$ . Then $\ds \bigcap_{i \mathop = 1}^n U_i$ is open in $M$ . That is, a finite intersection of open subsets is open.

Preamble

import Mathlib.Topology.MetricSpace.Basic

Formal statement

theorem Finite_Intersection_of_Open_Sets_of_Metric_Space_is_Open {α : Type _} [MetricSpace α] (S₁ S₂ : Set α) (h₁ : IsOpen S₁) (h₂ : IsOpen S₂) : IsOpen (S₁ ∩ S₂) := by sorry

Source

https://proofwiki.org/wiki/Finite_Intersection_of_Open_Sets_of_Metric_Space_is_Open

View graph