Grace/Cumulus/Metric/Subspace.g17

Open in Workbench Download source

Imports

Discrete

Declarations

Source

1-- Subspaces of a metric space: the restricted metric, its balls as traces2-- of balls, open and closed sets, convergence and Cauchy sequences, closed3-- subspaces of complete spaces, restricted maps, and the inclusion isometry4-- 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.Subspace10import Discrete1112def subspaceMetric (d S : Set) : Set := restrict(d, S × S)1314theorem subspaceMetric.function (X d S : Set)15  requires metric : IsMetric(X, d)16  requires inside : S ⊆ X17  shows subspaceMetric(d, S) : S × S → ℝ18proof19  have function := IsMetric.function with metric20  have product := product.monotone with inside, inside21  unfold subspaceMetric22  exact restrict.domain_function with function, product2324theorem subspaceMetric.apply (X d S x y : Set)25  requires metric : IsMetric(X, d)26  requires inside : S ⊆ X27  requires hx : x ∈ S28  requires hy : y ∈ S29  shows subspaceMetric(d, S)(x, y) = d(x, y)30proof31  have function := IsMetric.function with metric32  have product := product.monotone with inside, inside33  have pair := product.pair at x, y, S, S with hx, hy34  unfold call235  unfold subspaceMetric36  exact restrict.domain_apply with function, product, pair3738theorem subspaceMetric.metric (X d S : Set)39  requires metric : IsMetric(X, d)40  requires inside : S ⊆ X41  shows IsMetric(S, subspaceMetric(d, S))42proof43  constructor44  . exact subspaceMetric.function with metric, inside45  . constructor46    . intros x hx y hy47      have value := subspaceMetric.apply with metric, inside, hx, hy48      rw value49      exact IsMetric.nonnegative with metric, (inside with x, hx), (inside with50        y, hy)51    . constructor52      . intros x hx y hy53        have value := subspaceMetric.apply with metric, inside, hx, hy54        rw value55        exact IsMetric.eq_zero_iff with metric, (inside with x, hx),56          (inside with57          y, hy)58      . constructor59        . intros x hx y hy60          have valueXY := subspaceMetric.apply with metric, inside, hx, hy61          have valueYX := subspaceMetric.apply with metric, inside, hy, hx62          rw [valueXY, valueYX]63          exact IsMetric.symmetric with metric, (inside with x, hx),64            (inside with65            y, hy)66        . intros x hx y hy z hz67          have valueXZ := subspaceMetric.apply with metric, inside, hx, hz68          have valueXY := subspaceMetric.apply with metric, inside, hx, hy69          have valueYZ := subspaceMetric.apply with metric, inside, hy, hz70          rw [valueXZ, valueXY, valueYZ]71          exact IsMetric.triangle with metric, (inside with x, hx), (inside with72            y, hy),73            (inside with z, hz)7475theorem subspaceMetric.whole (X d : Set)76  requires metric : IsMetric(X, d)77  shows subspaceMetric(d, X) = d78proof79  have function := IsMetric.function with metric80  have restricted := subspaceMetric.function with81    metric, (Subset.reflexive at X)82  apply FunctionBetween.ext with restricted, function83  intros p hp84  obtain ⟨bound, x, hx, y, hy, rfl⟩ := product.membership.forward with hp85  have value := subspaceMetric.apply with86    metric, (Subset.reflexive at X), hx, hy87  unfold call2 at value88  exact value8990theorem subspaceMetric.nested (d S T : Set)91  requires inside : T ⊆ S92  shows subspaceMetric(subspaceMetric(d, S), T) = subspaceMetric(d, T)93proof94  have product := product.monotone with inside, inside95  unfold subspaceMetric96  exact restrict.nested with product9798-- Balls of the subspace are traces of balls of the space.99theorem subspaceMetric.ball (X d S x : Set, r : Real)100  requires metric : IsMetric(X, d)101  requires inside : S ⊆ X102  requires hx : x ∈ S103  shows ball(S, subspaceMetric(d, S), x, r) = ball(X, d, x, r) ∩ S104proof105  ext y106  constructor107  . intro hy108    have hyS := ball.point with hy109    have near := ball.distance with hy110    have value := subspaceMetric.apply with metric, inside, hx, hyS111    rw value at near112    apply intersection.membership.backward113    exact ⟨(ball.of_distance with (inside with y, hyS), near), hyS⟩114  . intro hy115    have both := intersection.membership.forward with hy116    have near := ball.distance with both.left117    have value := subspaceMetric.apply with metric, inside, hx, both.right118    apply ball.of_distance with both.right119    rw value120    exact near121122theorem subspaceMetric.closedBall (X d S x : Set, r : Real)123  requires metric : IsMetric(X, d)124  requires inside : S ⊆ X125  requires hx : x ∈ S126  shows closedBall(S, subspaceMetric(d, S), x, r) = closedBall(X, d, x, r) ∩ S127proof128  ext y129  constructor130  . intro hy131    have hyS := closedBall.point with hy132    have near := closedBall.distance with hy133    have value := subspaceMetric.apply with metric, inside, hx, hyS134    rw value at near135    apply intersection.membership.backward136    exact ⟨(closedBall.of_distance with (inside with y, hyS), near), hyS⟩137  . intro hy138    have both := intersection.membership.forward with hy139    have near := closedBall.distance with both.left140    have value := subspaceMetric.apply with metric, inside, hx, both.right141    apply closedBall.of_distance with both.right142    rw value143    exact near144145theorem subspaceMetric.open_of_open (X d S U : Set)146  requires metric : IsMetric(X, d)147  requires inside : S ⊆ X148  requires open : MetricOpen(X, d, U)149  shows MetricOpen(S, subspaceMetric(d, S), U ∩ S)150proof151  constructor152  . exact intersection.subset_right at U, S153  . intros x hx154    have both := intersection.membership.forward with hx155    obtain ⟨r, hr, positive, ballInside⟩ :=156      MetricOpen.ball_inside with open, both.left157    refine ⟨r, hr, positive, ?_⟩158    have typedR : Real(r) by exact hr159    have trace := subspaceMetric.ball at X, d, S, x, r with160      metric, inside, both.right161    rw trace162    exact intersection.monotone_left with ballInside163164theorem subspaceMetric.closed_of_closed (X d S C : Set)165  requires metric : IsMetric(X, d)166  requires inside : S ⊆ X167  requires closed : MetricClosed(X, d, C)168  shows MetricClosed(S, subspaceMetric(d, S), C ∩ S)169proof170  apply MetricClosed.of_ball_disjoint with (intersection.subset_right at C, S)171  intros x hx outside172  have hxX := inside with x, hx173  have away : ¬x ∈ C174    intro hxC175    apply outside176    exact intersection.membership.backward with ⟨hxC, hx⟩177  obtain ⟨r, hr, positive, disjoint⟩ :=178    MetricClosed.ball_disjoint with closed, hxX, away179  refine ⟨r, hr, positive, ?_⟩180  have typedR : Real(r) by exact hr181  have trace := subspaceMetric.ball at X, d, S, x, r with metric, inside, hx182  rw trace183  have separated := Disjoint.iff.forward with disjoint184  apply Disjoint.iff.backward185  intros y hy hyC186  have inBall := intersection.membership.forward with hy187  have inC := intersection.membership.forward with hyC188  exact separated with y, inBall.left, inC.left189190-- Convergence and the Cauchy property are the same in the subspace.191theorem subspaceMetric.converges_iff (X d S u x : Set)192  requires metric : IsMetric(X, d)193  requires inside : S ⊆ X194  requires sequence : SequenceIn(S, u)195  requires hx : x ∈ S196  shows ConvergesIn(S, subspaceMetric(d, S), u, x) ↔ ConvergesIn(X, d, u, x)197proof198  have uFunction := SequenceIn.function with sequence199  have ambient : SequenceIn(X, u)200    have closed : ∀ n ∈ ℕ, u(n) ∈ X201      intros n hn202      exact inside with u(n), (SequenceIn.term_of_member with sequence, hn)203    exact FunctionBetween.codomain_of_values with uFunction, closed204  constructor205  . intro converges206    apply ConvergesIn.of_eventually with ambient, (inside with x, hx)207    intros ε hε positive208    obtain ⟨N, hN, near⟩ := ConvergesIn.eventually with converges, positive209    refine ⟨N, hN, ?_⟩210    intros n hn le211    have term := SequenceIn.term_of_member with sequence, hn212    have value := subspaceMetric.apply with metric, inside, hx, term213    have close := near with n, hn, le214    rwa value at close215  . intro converges216    apply ConvergesIn.of_eventually with sequence, hx217    intros ε hε positive218    obtain ⟨N, hN, near⟩ := ConvergesIn.eventually with converges, positive219    refine ⟨N, hN, ?_⟩220    intros n hn le221    have term := SequenceIn.term_of_member with sequence, hn222    have value := subspaceMetric.apply with metric, inside, hx, term223    rw value224    exact near with n, hn, le225226theorem subspaceMetric.cauchy_iff (X d S u : Set)227  requires metric : IsMetric(X, d)228  requires inside : S ⊆ X229  requires sequence : SequenceIn(S, u)230  shows IsCauchy(S, subspaceMetric(d, S), u) ↔ IsCauchy(X, d, u)231proof232  have uFunction := SequenceIn.function with sequence233  have ambient : SequenceIn(X, u)234    have closed : ∀ n ∈ ℕ, u(n) ∈ X235      intros n hn236      exact inside with u(n), (SequenceIn.term_of_member with sequence, hn)237    exact FunctionBetween.codomain_of_values with uFunction, closed238  constructor239  . intro cauchy240    apply IsCauchy.of_eventually with ambient241    intros ε hε positive242    obtain ⟨N, hN, close⟩ := IsCauchy.eventually with cauchy, positive243    refine ⟨N, hN, ?_⟩244    intros m hm n hn leM leN245    have termM := SequenceIn.term_of_member with sequence, hm246    have termN := SequenceIn.term_of_member with sequence, hn247    have value := subspaceMetric.apply with metric, inside, termM, termN248    have near := close with m, hm, n, hn, leM, leN249    rwa value at near250  . intro cauchy251    apply IsCauchy.of_eventually with sequence252    intros ε hε positive253    obtain ⟨N, hN, close⟩ := IsCauchy.eventually with cauchy, positive254    refine ⟨N, hN, ?_⟩255    intros m hm n hn leM leN256    have termM := SequenceIn.term_of_member with sequence, hm257    have termN := SequenceIn.term_of_member with sequence, hn258    have value := subspaceMetric.apply with metric, inside, termM, termN259    rw value260    exact close with m, hm, n, hn, leM, leN261262-- A closed subspace of a complete space is complete.263theorem IsComplete.closed_subspace (X d S : Set)264  requires complete : IsComplete(X, d)265  requires closed : MetricClosed(X, d, S)266  shows IsComplete(S, subspaceMetric(d, S))267proof268  have metric := IsComplete.metric with complete269  have inside := MetricClosed.subset with closed270  apply IsComplete.of_limits with (subspaceMetric.metric with metric, inside)271  intros u cauchy272  have sequence := IsCauchy.sequence with cauchy273  have bridge := subspaceMetric.cauchy_iff at X, d, S, u with274    metric, inside, sequence275  have ambient := bridge.forward with cauchy276  obtain ⟨x, hx, converges⟩ := IsComplete.limit with complete, ambient277  have terms : ∀ n ∈ ℕ, u(n) ∈ S278    intros n hn279    exact SequenceIn.term_of_member with sequence, hn280  have hxS := ConvergesIn.limit_in_closed with closed, terms, converges281  have same := subspaceMetric.converges_iff at X, d, S, u, x with282    metric, inside, sequence, hxS283  exact ⟨x, hxS, (same.backward with converges)⟩284285theorem IsBounded.subspace (X d S T : Set)286  requires metric : IsMetric(X, d)287  requires inside : S ⊆ X288  requires bounded : IsBounded(X, d, T)289  requires hT : T ⊆ S290  shows IsBounded(S, subspaceMetric(d, S), T)291proof292  obtain ⟨insideT, r, hr, bound⟩ := bounded293  refine ⟨hT, r, hr, ?_⟩294  intros x hx y hy295  have value :=296    subspaceMetric.apply with metric, inside, (hT with x, hx), (hT with y, hy)297  rw value298  exact bound with x, hx, y, hy299300-- Restricting a continuous map to a subspace keeps it continuous.301theorem IsMetricContinuous.restrict (f X d Y e S : Set)302  requires metric : IsMetric(X, d)303  requires inside : S ⊆ X304  requires continuous : IsMetricContinuous(f, X, d, Y, e)305  shows IsMetricContinuous(restrict(f, S), S, subspaceMetric(d, S), Y, e)306proof307  have function := IsMetricContinuous.function with continuous308  have restricted := restrict.domain_function with function, inside309  apply IsMetricContinuous.of_pointwise with restricted310  intros x hx311  have hxX := inside with x, hx312  have atX := IsMetricContinuous.at with continuous, hxX313  apply MetricContinuousAt.of_control with restricted, hx314  intros ε hε positive315  obtain ⟨δ, hδ, positiveD, maps⟩ :=316    MetricContinuousAt.control with atX, positive317  refine ⟨δ, hδ, positiveD, ?_⟩318  intros y hy near319  have valueX := restrict.domain_apply with function, inside, hx320  have valueY := restrict.domain_apply with function, inside, hy321  have distance := subspaceMetric.apply with metric, inside, hx, hy322  rw distance at near323  rw [valueX, valueY]324  exact maps with y, (inside with y, hy), near325326theorem inclusionMap.isometry (X d S : Set)327  requires metric : IsMetric(X, d)328  requires inside : S ⊆ X329  shows IsIsometry(inclusionMap(S, X), S, subspaceMetric(d, S), X, d)330proof331  have function := inclusionMap.function at S, X with inside332  constructor333  . exact function334  . intros x hx y hy335    have valueX := inclusionMap.value at S, X, x with inside, hx336    have valueY := inclusionMap.value at S, X, y with inside, hy337    rw [valueX, valueY]338    have value := subspaceMetric.apply with metric, inside, hx, hy339    symm at value340    exact value341342theorem inclusionMap.metric_continuous (X d S : Set)343  requires metric : IsMetric(X, d)344  requires inside : S ⊆ X345  shows IsMetricContinuous(inclusionMap(S, X), S, subspaceMetric(d, S), X, d)346proof347  exact IsIsometry.continuous with (inclusionMap.isometry with metric, inside)348