Grace/Cumulus/Metric/Closed.g17

Open in Workbench Download source

Imports

Open

Declarations

Source

1-- Closed sets in a metric space: closed balls, spheres, and points are2-- closed; a point lies in the closure of a set exactly when every ball3-- around it meets the set4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Metric.Closed10import Open1112predicate MetricClosed (X d C : Set) := IsClosed(X, metricTopology(X, d), C)1314theorem MetricClosed.subset (X d C : Set)15  requires closed : MetricClosed(X, d, C)16  shows C ⊆ X17proof18  unfold MetricClosed at closed19  exact closed.left2021theorem MetricClosed.complement_open (X d C : Set)22  requires closed : MetricClosed(X, d, C)23  shows MetricOpen(X, d, complement(X, C))24proof25  unfold MetricClosed at closed26  exact metricTopology.open with closed.right2728theorem MetricClosed.of_complement_open (X d C : Set)29  requires inside : C ⊆ X30  requires open : MetricOpen(X, d, complement(X, C))31  shows MetricClosed(X, d, C)32proof33  unfold MetricClosed34  exact ⟨inside, (metricTopology.of_open with open)⟩3536theorem MetricOpen.complement_closed (X d U : Set)37  requires metric : IsMetric(X, d)38  requires open : MetricOpen(X, d, U)39  shows MetricClosed(X, d, complement(X, U))40proof41  have topology := metricTopology.topology with metric42  exact Open.complement_closed with topology, (metricTopology.of_open with open)4344theorem MetricClosed.whole (X d : Set)45  requires metric : IsMetric(X, d)46  shows MetricClosed(X, d, X)47proof48  exact IsClosed.whole with (metricTopology.topology with metric)4950theorem MetricClosed.empty (X d : Set)51  requires metric : IsMetric(X, d)52  shows MetricClosed(X, d, ∅)53proof54  exact IsClosed.empty with (metricTopology.topology with metric)5556theorem MetricClosed.union2 (X d C D : Set)57  requires metric : IsMetric(X, d)58  requires hC : MetricClosed(X, d, C)59  requires hD : MetricClosed(X, d, D)60  shows MetricClosed(X, d, C ∪ D)61proof62  have topology := metricTopology.topology with metric63  unfold MetricClosed at hC64  unfold MetricClosed at hD65  exact IsClosed.union2 with topology, hC, hD6667theorem MetricClosed.intersection2 (X d C D : Set)68  requires metric : IsMetric(X, d)69  requires hC : MetricClosed(X, d, C)70  requires hD : MetricClosed(X, d, D)71  shows MetricClosed(X, d, C ∩ D)72proof73  have topology := metricTopology.topology with metric74  unfold MetricClosed at hC75  unfold MetricClosed at hD76  exact IsClosed.intersection2 with topology, hC, hD7778theorem MetricClosed.family_intersection (X d S : Set)79  requires metric : IsMetric(X, d)80  requires nonempty : Nonempty(S)81  requires closed : ∀ C ∈ S, MetricClosed(X, d, C)82  shows MetricClosed(X, d, ⋂(S))83proof84  have topology := metricTopology.topology with metric85  have members : ∀ C ∈ S, IsClosed(X, metricTopology(X, d), C)86    intros C hC87    have closedC := closed with C, hC88    unfold MetricClosed at closedC89    exact closedC90  exact IsClosed.family_intersection with topology, nonempty, members9192-- A point outside a closed set has a ball missing the set.93theorem MetricClosed.ball_disjoint (X d C x : Set)94  requires closed : MetricClosed(X, d, C)95  requires hx : x ∈ X96  requires outside : ¬x ∈ C97  shows ∃ r ∈ ℝ, 0 < r ∧ Disjoint(ball(X, d, x, r), C)98proof99  have open := MetricClosed.complement_open with closed100  have member : x ∈ complement(X, C) := complement.membership.backward with101    ⟨hx, outside⟩102  obtain ⟨r, hr, positive, inside⟩ := MetricOpen.ball_inside with open, member103  refine ⟨r, hr, positive, ?_⟩104  apply Disjoint.iff.backward105  intros y hy hyC106  have away := complement.membership.forward with (inside with y, hy)107  exact away.right with hyC108109theorem MetricClosed.of_ball_disjoint (X d C : Set)110  requires inside : C ⊆ X111  requires separated :112    ∀ x ∈ X, ¬x ∈ C → ∃ r ∈ ℝ, 0 < r ∧ Disjoint(ball(X, d, x, r), C)113  shows MetricClosed(X, d, C)114proof115  apply MetricClosed.of_complement_open with inside116  constructor117  . exact complement.subset at X, C118  . intros x hx119    have parts := complement.membership.forward with hx120    obtain ⟨r, hr, positive, disjoint⟩ :=121      separated with x, parts.left, parts.right122    refine ⟨r, hr, positive, ?_⟩123    intros y hy124    have hyX := ball.point with hy125    have away := Disjoint.iff.forward with disjoint126    exact complement.membership.backward with ⟨hyX, (away with y, hy)⟩127128-- A point of X every ball around which meets a closed set belongs to it.129theorem MetricClosed.of_balls_meet (X d C x : Set)130  requires closed : MetricClosed(X, d, C)131  requires hx : x ∈ X132  requires meets : ∀ r ∈ ℝ, 0 < r → Nonempty(ball(X, d, x, r) ∩ C)133  shows x ∈ C134proof135  by_contra outside136  obtain ⟨r, hr, positive, disjoint⟩ :=137    MetricClosed.ball_disjoint with closed, hx, outside138  obtain ⟨y, hy⟩ := meets with r, hr, positive139  have both := intersection.membership.forward with hy140  have away := Disjoint.iff.forward with disjoint141  exact away with y, both.left, both.right142143theorem MetricClosed.of_limit_points (X d C : Set)144  requires inside : C ⊆ X145  requires limits : ∀ x ∈ X,146    (∀ r ∈ ℝ, 0 < r → Nonempty(ball(X, d, x, r) ∩ C)) → x ∈ C147  shows MetricClosed(X, d, C)148proof149  apply MetricClosed.of_ball_disjoint with inside150  intros x hx outside151  by_contra none152  apply outside153  apply limits with x, hx154  intros r hr positive155  by_contra empty156  apply none157  refine ⟨r, hr, positive, ?_⟩158  apply Disjoint.iff.backward159  intros y hy hyC160  apply empty161  witness y162  exact intersection.membership.backward with ⟨hy, hyC⟩163164theorem closedBall.closed (X d x : Set, r : Real)165  requires metric : IsMetric(X, d)166  requires hx : x ∈ X167  shows MetricClosed(X, d, closedBall(X, d, x, r))168proof169  apply MetricClosed.of_ball_disjoint with (closedBall.subset at X, d, x, r)170  intros y hy outside171  have dxy := IsMetric.real with metric, hx, hy172  have far : r < d(x, y)173    have order := realLess.trichotomy at r, d(x, y)174    rcases order with less | equal | greater175    . exact less176    . exfalso177      apply outside178      apply closedBall.of_distance with hy179      rw ← equal180      exact realLe.reflexive181    . exfalso182      apply outside183      exact closedBall.of_distance with hy, (realLess.implies_le with greater)184  have radiusReal : d(x, y) - r ∈ ℝ by typecheck185  have positive : (0:R) < d(x, y) - r by linarith186  refine ⟨d(x, y) - r, radiusReal, positive, ?_⟩187  apply Disjoint.iff.backward188  intros z hz inBall189  have hzX := ball.point with hz190  have near := ball.distance with hz191  have close := closedBall.distance with inBall192  have triangle := IsMetric.triangle_to with metric, hx, hy, hzX193  have dyz := IsMetric.real with metric, hy, hzX194  have dxz := IsMetric.real with metric, hx, hzX195  linarith196197theorem ball.complement_closed (X d x : Set, r : Real)198  requires metric : IsMetric(X, d)199  requires hx : x ∈ X200  shows MetricClosed(X, d, complement(X, ball(X, d, x, r)))201proof202  exact MetricOpen.complement_closed with metric, (ball.open with metric, hx)203204theorem closedBall.complement_open (X d x : Set, r : Real)205  requires metric : IsMetric(X, d)206  requires hx : x ∈ X207  shows MetricOpen(X, d, complement(X, closedBall(X, d, x, r)))208proof209  exact MetricClosed.complement_open with (closedBall.closed with metric, hx)210211theorem sphere.closed (X d x : Set, r : Real)212  requires metric : IsMetric(X, d)213  requires hx : x ∈ X214  shows MetricClosed(X, d, sphere(X, d, x, r))215proof216  apply MetricClosed.of_ball_disjoint with (sphere.subset at X, d, x, r)217  intros y hy outside218  have dxy := IsMetric.real with metric, hx, hy219  have order := realLess.trichotomy at d(x, y), r220  rcases order with less | equal | greater221  . have radiusReal : r - d(x, y) ∈ ℝ by typecheck222    have positive : (0:R) < r - d(x, y) by linarith223    refine ⟨r - d(x, y), radiusReal, positive, ?_⟩224    apply Disjoint.iff.backward225    intros z hz onSphere226    have hzX := ball.point with hz227    have near := ball.distance with hz228    obtain ⟨hzX2, equal⟩ := sphere.membership.forward with onSphere229    have triangle := IsMetric.triangle with metric, hx, hy, hzX230    have dyz := IsMetric.real with metric, hy, hzX231    have dxz := IsMetric.real with metric, hx, hzX232    linarith233  . exfalso234    apply outside235    exact sphere.membership.backward with ⟨hy, equal⟩236  . have radiusReal : d(x, y) - r ∈ ℝ by typecheck237    have positive : (0:R) < d(x, y) - r by linarith238    refine ⟨d(x, y) - r, radiusReal, positive, ?_⟩239    apply Disjoint.iff.backward240    intros z hz onSphere241    have hzX := ball.point with hz242    have near := ball.distance with hz243    obtain ⟨hzX2, equal⟩ := sphere.membership.forward with onSphere244    have triangle := IsMetric.triangle_to with metric, hx, hy, hzX245    have dyz := IsMetric.real with metric, hy, hzX246    have dxz := IsMetric.real with metric, hx, hzX247    linarith248249theorem singleton.metric_closed (X d x : Set)250  requires metric : IsMetric(X, d)251  requires hx : x ∈ X252  shows MetricClosed(X, d, {x})253proof254  have topology := metricTopology.topology with metric255  have hausdorff := metricTopology.hausdorff with metric256  exact IsHausdorff.singleton_closed with topology, hausdorff, hx257258theorem sphere.eq_difference (X d x : Set, r : Real)259  requires metric : IsMetric(X, d)260  requires hx : x ∈ X261  shows sphere(X, d, x, r) = closedBall(X, d, x, r) ∖ ball(X, d, x, r)262proof263  have disjoint := sphere.disjoint_ball at X, d, x, r264  have separated := Disjoint.iff.forward with disjoint265  ext y266  constructor267  . intro hy268    have inside := sphere.subset_closedBall with metric, hx269    have inClosed := inside with y, hy270    apply difference.membership.backward271    exact ⟨inClosed, (separated with y, hy)⟩272  . intro hy273    have parts := difference.membership.forward with hy274    have split := closedBall.eq_ball_union_sphere with metric, hx275    rw split at parts276    have cases := union2.membership.forward with parts.left277    cases cases with inBall | onSphere278    . exfalso279      exact parts.right with inBall280    . exact onSphere281282-- Closure: a point is in the closure of A exactly when every ball around283-- it meets A.284theorem metricClosure.membership (X d A x : Set)285  requires metric : IsMetric(X, d)286  requires hA : A ⊆ X287  shows x ∈ closure(X, metricTopology(X, d), A) ↔288    x ∈ X ∧ (∀ r ∈ ℝ, 0 < r → Nonempty(ball(X, d, x, r) ∩ A))289proof290  have topology := metricTopology.topology with metric291  have characterization :=292    closure.membership at X, metricTopology(X, d), A, x with293    topology, hA294  constructor295  . intro hx296    obtain ⟨hxX, touches⟩ := characterization.forward with hx297    refine ⟨hxX, ?_⟩298    intros r hr positive299    have openBall := ball.member_topology at X, d, x, r with metric, hxX300    have center := ball.center with metric, hxX, positive301    exact touches with ball(X, d, x, r), openBall, center302  . intro data303    obtain ⟨hxX, meets⟩ := data304    apply characterization.backward305    refine ⟨hxX, ?_⟩306    intros U hU hxU307    obtain ⟨r, hr, positive, inside⟩ := metricTopology.ball_inside with hU, hxU308    obtain ⟨y, hy⟩ := meets with r, hr, positive309    have both := intersection.membership.forward with hy310    witness y311    exact intersection.membership.backward with ⟨(inside with312      y, both.left), both.right⟩313314theorem metricClosure.ball_meets (X d A x : Set, r : Real)315  requires metric : IsMetric(X, d)316  requires hA : A ⊆ X317  requires hx : x ∈ closure(X, metricTopology(X, d), A)318  requires positive : 0 < r319  shows Nonempty(ball(X, d, x, r) ∩ A)320proof321  have characterization := metricClosure.membership at X, d, A, x with322    metric, hA323  obtain ⟨hxX, meets⟩ := characterization.forward with hx324  have realR : r ∈ ℝ by typecheck325  exact meets with r, realR, positive326327theorem metricClosure.of_balls_meet (X d A x : Set)328  requires metric : IsMetric(X, d)329  requires hA : A ⊆ X330  requires hx : x ∈ X331  requires meets : ∀ r ∈ ℝ, 0 < r → Nonempty(ball(X, d, x, r) ∩ A)332  shows x ∈ closure(X, metricTopology(X, d), A)333proof334  have characterization := metricClosure.membership at X, d, A, x with335    metric, hA336  exact characterization.backward with ⟨hx, meets⟩337338theorem ball.closure_subset_closedBall (X d x : Set, r : Real)339  requires metric : IsMetric(X, d)340  requires hx : x ∈ X341  shows342    closure(X, metricTopology(X, d), ball(X, d, x, r)) ⊆ closedBall(X, d, x, r)343proof344  have topology := metricTopology.topology with metric345  have closed := closedBall.closed at X, d, x, r with metric, hx346  have inside := ball.subset_closedBall with metric, hx347  unfold MetricClosed at closed348  exact closure.least with closed, inside349350theorem closedBall.closure (X d x : Set, r : Real)351  requires metric : IsMetric(X, d)352  requires hx : x ∈ X353  shows closure(X, metricTopology(X, d), closedBall(X, d, x, r)) =354    closedBall(X, d, x, r)355proof356  have topology := metricTopology.topology with metric357  have closed := closedBall.closed at X, d, x, r with metric, hx358  unfold MetricClosed at closed359  exact closure.of_closed with topology, closed360361-- A set is dense exactly when every ball meets it.362theorem metricDense.iff (X d A : Set)363  requires metric : IsMetric(X, d)364  requires hA : A ⊆ X365  shows IsDense(X, metricTopology(X, d), A) ↔366    (∀ x ∈ X, ∀ r ∈ ℝ, 0 < r → Nonempty(ball(X, d, x, r) ∩ A))367proof368  have topology := metricTopology.topology with metric369  constructor370  . intro dense371    intros x hx r hr positive372    unfold IsDense at dense373    have inClosure : x ∈ closure(X, metricTopology(X, d), A)374      rw dense375      exact hx376    exact metricClosure.ball_meets with metric, hA, inClosure, positive377  . intro meets378    unfold IsDense379    apply Subset.antisymmetric380    . exact closure.subset with topology, hA381    . intros x hx382      exact metricClosure.of_balls_meet with metric, hA, hx, (meets with x, hx)383384theorem metricDense.whole (X d : Set)385  requires metric : IsMetric(X, d)386  shows IsDense(X, metricTopology(X, d), X)387proof388  have topology := metricTopology.topology with metric389  unfold IsDense390  exact closure.of_closed with topology, (IsClosed.whole with topology)391