Open_Sets_in_Metric_Space

Proved

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

metric-spacesopen-setsproofwiki

Let $M = \struct {A, d}$ be a metric space. Then $\O$ and $A$ are both open in $M$ .

Preamble

import Mathlib.Topology.MetricSpace.Basic

Formal statement

theorem Open_Sets_in_Metric_Space {α : Type _} [MetricSpace α] : IsOpen (Set.univ : Set α) ∧ IsOpen (∅ : Set α) := by sorry

Source