Grace/Cumulus/Metric/Open.g17

Open in Workbench Download source

Imports

Ball

Declarations

Source

1-- The metric topology: open sets are those containing a ball around each of2-- their points; they form a Hausdorff topology in which balls are open3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Metric.Open9import Ball1011predicate MetricOpen (X d U : Set) :=12  (U ⊆ X) ∧ (∀ x ∈ U, ∃ r ∈ ℝ, 0 < r ∧ ball(X, d, x, r) ⊆ U)1314def metricTopology (X d : Set) : Set :=15  { U ∈ 𝒫(X) | ∀ x ∈ U, ∃ r ∈ ℝ, 0 < r ∧ ball(X, d, x, r) ⊆ U }1617theorem MetricOpen.subset (X d U : Set)18  requires open : MetricOpen(X, d, U)19  shows U ⊆ X20proof21  exact open.left2223theorem MetricOpen.ball_inside (X d U x : Set)24  requires open : MetricOpen(X, d, U)25  requires hx : x ∈ U26  shows ∃ r ∈ ℝ, 0 < r ∧ ball(X, d, x, r) ⊆ U27proof28  exact open.right with x, hx2930theorem metricTopology.of_open (X d U : Set)31  requires open : MetricOpen(X, d, U)32  shows U ∈ metricTopology(X, d)33proof34  obtain ⟨inside, balls⟩ := open35  apply metricTopology.membership.backward36  exact ⟨(powerset.membership_iff.backward with inside), balls⟩3738theorem metricTopology.open (X d U : Set)39  requires member : U ∈ metricTopology(X, d)40  shows MetricOpen(X, d, U)41proof42  obtain ⟨bound, balls⟩ := metricTopology.membership.forward with member43  exact ⟨(powerset.membership_iff.forward with bound), balls⟩4445theorem metricTopology.iff (X d U : Set)46  shows U ∈ metricTopology(X, d) ↔ MetricOpen(X, d, U)47proof48  constructor49  . intro member50    exact metricTopology.open with member51  . intro open52    exact metricTopology.of_open with open5354theorem metricTopology.subset (X d U : Set)55  requires member : U ∈ metricTopology(X, d)56  shows U ⊆ X57proof58  exact MetricOpen.subset with (metricTopology.open with member)5960theorem metricTopology.ball_inside (X d U x : Set)61  requires member : U ∈ metricTopology(X, d)62  requires hx : x ∈ U63  shows ∃ r ∈ ℝ, 0 < r ∧ ball(X, d, x, r) ⊆ U64proof65  exact MetricOpen.ball_inside with (metricTopology.open with member), hx6667theorem metricTopology.subset_powerset (X d : Set)68  shows metricTopology(X, d) ⊆ 𝒫(X)69proof70  intros U hU71  exact powerset.membership_iff.backward with (metricTopology.subset with hU)7273theorem MetricOpen.whole (X d : Set)74  shows MetricOpen(X, d, X)75proof76  constructor77  . exact Subset.reflexive at X78  . intros x hx79    have one : (1:R) ∈ ℝ by typecheck80    have positive : (0:R) < 1 by linarith81    exact ⟨(1:R), one, positive, (ball.subset at X, d, x, (1:R))⟩8283theorem MetricOpen.empty (X d : Set)84  shows MetricOpen(X, d, ∅)85proof86  constructor87  . exact empty.subset at X88  . intros x hx89    exfalso90    exact empty.membership with hx9192theorem MetricOpen.union (X d S : Set)93  requires open : ∀ U ∈ S, MetricOpen(X, d, U)94  shows MetricOpen(X, d, ⋃(S))95proof96  constructor97  . apply union.subset98    intros U hU99    exact MetricOpen.subset with (open with U, hU)100  . intros x hx101    obtain ⟨U, hU, hxU⟩ := union.membership.forward with hx102    obtain ⟨r, hr, positive, inside⟩ :=103      MetricOpen.ball_inside with (open with U, hU), hxU104    refine ⟨r, hr, positive, ?_⟩105    exact Subset.transitive with inside, (union.subset_of_member with hU)106107theorem MetricOpen.union2 (X d U V : Set)108  requires openU : MetricOpen(X, d, U)109  requires openV : MetricOpen(X, d, V)110  shows MetricOpen(X, d, U ∪ V)111proof112  constructor113  . exact union2.subset with openU.left, openV.left114  . intros x hx115    have split := union2.membership.forward with hx116    cases split with inU | inV117    . obtain ⟨r, hr, positive, inside⟩ := MetricOpen.ball_inside with openU, inU118      refine ⟨r, hr, positive, ?_⟩119      exact Subset.transitive with inside, (union2.subset_left at U, V)120    . obtain ⟨r, hr, positive, inside⟩ := MetricOpen.ball_inside with openV, inV121      refine ⟨r, hr, positive, ?_⟩122      exact Subset.transitive with inside, (union2.subset_right at U, V)123124theorem MetricOpen.intersection2 (X d U V : Set)125  requires metric : IsMetric(X, d)126  requires openU : MetricOpen(X, d, U)127  requires openV : MetricOpen(X, d, V)128  shows MetricOpen(X, d, U ∩ V)129proof130  constructor131  . exact Subset.transitive with (intersection.subset_left at U, V), openU.left132  . intros x hx133    have both := intersection.membership.forward with hx134    have hxX := openU.left with x, both.left135    obtain ⟨r, hr, positiveR, insideU⟩ :=136      MetricOpen.ball_inside with openU, both.left137    obtain ⟨s, hs, positiveS, insideV⟩ :=138      MetricOpen.ball_inside with openV, both.right139    have centerR := ball.center with metric, hxX, positiveR140    have centerS := ball.center with metric, hxX, positiveS141    obtain ⟨t, ht, positiveT, inR, inS⟩ :=142      ball.common_radius with metric, hxX, hxX, centerR, centerS143    refine ⟨t, ht, positiveT, ?_⟩144    apply intersection.greatest145    . exact Subset.transitive with inR, insideU146    . exact Subset.transitive with inS, insideV147148theorem metricTopology.topology (X d : Set)149  requires metric : IsMetric(X, d)150  shows IsTopology(X, metricTopology(X, d))151proof152  constructor153  . exact metricTopology.subset_powerset at X, d154  . constructor155    . exact metricTopology.of_open with (MetricOpen.whole at X, d)156    . constructor157      . intros S hS158        apply metricTopology.of_open159        apply MetricOpen.union160        intros U hU161        exact metricTopology.open with (hS with U, hU)162      . intros U hU V hV163        have openU := metricTopology.open with hU164        have openV := metricTopology.open with hV165        exact metricTopology.of_open with (MetricOpen.intersection2 with166          metric, openU, openV)167168theorem metricTopology.empty (X d : Set)169  shows ∅ ∈ metricTopology(X, d)170proof171  exact metricTopology.of_open with (MetricOpen.empty at X, d)172173theorem metricTopology.whole (X d : Set)174  shows X ∈ metricTopology(X, d)175proof176  exact metricTopology.of_open with (MetricOpen.whole at X, d)177178-- Balls are open.179theorem ball.open (X d x : Set, r : Real)180  requires metric : IsMetric(X, d)181  requires hx : x ∈ X182  shows MetricOpen(X, d, ball(X, d, x, r))183proof184  constructor185  . exact ball.subset at X, d, x, r186  . intros y hy187    have hyX := ball.point with hy188    have dxy := IsMetric.real with metric, hx, hyX189    have positive := ball.inside_radius_positive with metric, hx, hy190    have inside := ball.inside with metric, hx, hy191    have radiusReal : r - d(x, y) ∈ ℝ by typecheck192    exact ⟨r - d(x, y), radiusReal, positive, inside⟩193194theorem ball.member_topology (X d x : Set, r : Real)195  requires metric : IsMetric(X, d)196  requires hx : x ∈ X197  shows ball(X, d, x, r) ∈ metricTopology(X, d)198proof199  exact metricTopology.of_open with (ball.open with metric, hx)200201-- Distinct points are separated by disjoint balls, so the metric topology202-- is Hausdorff.203theorem metricTopology.hausdorff (X d : Set)204  requires metric : IsMetric(X, d)205  shows IsHausdorff(X, metricTopology(X, d))206proof207  intros x hx y hy distinct208  have dxy := IsMetric.real with metric, hx, hy209  have positive := ball.half_positive with metric, hx, hy, distinct210  have disjoint := ball.half_disjoint with metric, hx, hy, distinct211  refine ⟨ball(X, d, x, half(d(x, y))), (ball.member_topology with metric, hx),212    ball(X, d, y, half(d(x, y))), (ball.member_topology with213      metric, hy), ?_, ?_, disjoint⟩214  . exact ball.center with metric, hx, positive215  . exact ball.center with metric, hy, positive216217-- A point is interior to A exactly when some ball around it lies in A.218theorem metricInterior.membership (X d A x : Set)219  requires metric : IsMetric(X, d)220  shows x ∈ interiorIn(metricTopology(X, d), A) ↔221    x ∈ X ∧ (∃ r ∈ ℝ, 0 < r ∧ ball(X, d, x, r) ⊆ A)222proof223  constructor224  . intro hx225    unfold interiorIn at hx226    obtain ⟨U, hU, hxU⟩ := union.membership.forward with hx227    obtain ⟨openU, inside⟩ := openSubsets.membership.forward with hU228    have hxX := metricTopology.subset with openU, x, hxU229    obtain ⟨r, hr, positive, ballInside⟩ :=230      metricTopology.ball_inside with openU, hxU231    exact ⟨hxX, r, hr, positive, (Subset.transitive with ballInside, inside)⟩232  . intro data233    obtain ⟨hxX, r, hr, positive, inside⟩ := data234    have openBall := ball.member_topology at X, d, x, r with metric, hxX235    have greatest := interiorIn.greatest with openBall, inside236    exact greatest with x, (ball.center with metric, hxX, positive)237