Metric_Space_is_Hausdorff

Proved

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

hausdorff-spacesmetric-spacesproofwiki

Let $M = \struct {A, d}$ be a metric space. Then $M$ is a Hausdorff space.

Preamble

import Mathlib.Topology.MetricSpace.Basic

Formal statement

theorem Metric_Space_is_Hausdorff {α : Type _} [MetricSpace α] : T2Space α := by sorry

Source