Grace/Cumulus/Metric/Discrete.g17

Open in Workbench Download source

Imports

Line

Declarations

Source

1-- The discrete metric on any set: distinct points are at distance one, so2-- every subset is open, every subset is bounded, every map out of the3-- space is uniformly continuous, and the space is complete4-- 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.Discrete10import Line1112def discreteDistance (X : Set) : Set :=13  { q ∈ (X × X) × ℝ | ∃ x ∈ X, ∃ y ∈ X,14    ((x = y ∧ q = ((x, y) ↦ (0:R))) ∨ (x ≠ y ∧ q = ((x, y) ↦ (1:R)))) }1516theorem discreteDistance.relates_self (X x : Set)17  requires hx : x ∈ X18  shows relates(discreteDistance(X), (x, x), (0:R))19proof20  have zeroReal : (0:R) ∈ ℝ by typecheck21  have pair := product.pair at x, x, X, X with hx, hx22  have entry := product.pair at (x, x), (0:R), X × X, ℝ with pair, zeroReal23  unfold relates24  apply discreteDistance.membership.backward25  refine ⟨entry, x, hx, x, hx, ?_⟩26  left27  constructor28  . rfl29  . rfl3031theorem discreteDistance.relates_distinct (X x y : Set)32  requires hx : x ∈ X33  requires hy : y ∈ X34  requires distinct : x ≠ y35  shows relates(discreteDistance(X), (x, y), (1:R))36proof37  have oneReal : (1:R) ∈ ℝ by typecheck38  have pair := product.pair at x, y, X, X with hx, hy39  have entry := product.pair at (x, y), (1:R), X × X, ℝ with pair, oneReal40  unfold relates41  apply discreteDistance.membership.backward42  refine ⟨entry, x, hx, y, hy, ?_⟩43  right44  constructor45  . exact distinct46  . rfl4748theorem discreteDistance.relation (X : Set)49  shows RelationBetween(discreteDistance(X), X × X, ℝ)50proof51  intros q hq52  have parts := discreteDistance.membership.forward with hq53  exact parts.left5455-- The value at a pair is determined by whether its coordinates coincide.56theorem discreteDistance.value_shape (X p v : Set)57  requires edge : relates(discreteDistance(X), p, v)58  shows59    ∃ x ∈ X, ∃ y ∈ X, p = (x, y) ∧ ((x = y ∧ v = (0:R)) ∨ (x ≠ y ∧ v = (1:R)))60proof61  unfold relates at edge62  obtain ⟨bound, x, hx, y, hy, split⟩ :=63    discreteDistance.membership.forward with edge64  refine ⟨x, hx, y, hy, ?_⟩65  cases split with same | different66  . obtain ⟨equal, shape⟩ := same67    obtain ⟨first, second⟩ := orderedPair.injective with shape68    refine ⟨first, ?_⟩69    left70    exact ⟨equal, second⟩71  . obtain ⟨unequal, shape⟩ := different72    obtain ⟨first, second⟩ := orderedPair.injective with shape73    refine ⟨first, ?_⟩74    right75    exact ⟨unequal, second⟩7677theorem discreteDistance.functional (X : Set)78  shows Functional(discreteDistance(X))79proof80  intros p v first w second81  obtain ⟨x, hx, y, hy, shapeV, splitV⟩ :=82    discreteDistance.value_shape with first83  obtain ⟨a, ha, b, hb, shapeW, splitW⟩ :=84    discreteDistance.value_shape with second85  rw shapeV at shapeW86  obtain ⟨xa, yb⟩ := orderedPair.injective with shapeW87  rw [← xa, ← yb] at splitW88  cases splitV with sameV | differentV89  . cases splitW with sameW | differentW90    . rw [sameV.right, sameW.right]91      rfl92    . exfalso93      exact differentW.left with sameV.left94  . cases splitW with sameW | differentW95    . exfalso96      exact differentV.left with sameW.left97    . rw [differentV.right, differentW.right]98      rfl99100theorem discreteDistance.total (X : Set)101  shows ∀ p ∈ X × X, ∃ v ∈ ℝ, relates(discreteDistance(X), p, v)102proof103  intros p hp104  obtain ⟨bound, x, hx, y, hy, rfl⟩ := product.membership.forward with hp105  have split : x = y ∨ x ≠ y by tauto106  cases split with same | different107  . have zeroReal : (0:R) ∈ ℝ by typecheck108    refine ⟨(0:R), zeroReal, ?_⟩109    rw same110    exact discreteDistance.relates_self with hy111  . have oneReal : (1:R) ∈ ℝ by typecheck112    refine ⟨(1:R), oneReal, ?_⟩113    exact discreteDistance.relates_distinct with hx, hy, different114115theorem discreteDistance.function (X : Set)116  shows discreteDistance(X) : X × X → ℝ117proof118  constructor119  . exact discreteDistance.relation at X120  . constructor121    . exact discreteDistance.functional at X122    . exact discreteDistance.total at X123124theorem discreteDistance.self (X x : Set)125  requires hx : x ∈ X126  shows discreteDistance(X)(x, x) = (0:R)127proof128  have function := discreteDistance.function at X129  have pair := product.pair at x, x, X, X with hx, hx130  have edge := discreteDistance.relates_self with hx131  unfold call2132  exact FunctionBetween.apply_value with function, pair, edge133134theorem discreteDistance.distinct (X x y : Set)135  requires hx : x ∈ X136  requires hy : y ∈ X137  requires distinct : x ≠ y138  shows discreteDistance(X)(x, y) = (1:R)139proof140  have function := discreteDistance.function at X141  have pair := product.pair at x, y, X, X with hx, hy142  have edge := discreteDistance.relates_distinct with hx, hy, distinct143  unfold call2144  exact FunctionBetween.apply_value with function, pair, edge145146theorem discreteDistance.le_one (X x y : Set)147  requires hx : x ∈ X148  requires hy : y ∈ X149  shows discreteDistance(X)(x, y) ≤ (1:R)150proof151  have split : x = y ∨ x ≠ y by tauto152  cases split with same | different153  . rw same154    have self := discreteDistance.self with hy155    rw self156    have one := realZero.lt_one157    linarith158  . have value := discreteDistance.distinct with hx, hy, different159    rw value160    exact realLe.reflexive161162theorem discreteDistance.nonnegative (X x y : Set)163  requires hx : x ∈ X164  requires hy : y ∈ X165  shows (0:R) ≤ discreteDistance(X)(x, y)166proof167  have split : x = y ∨ x ≠ y by tauto168  cases split with same | different169  . rw same170    have self := discreteDistance.self with hy171    rw self172    exact realLe.reflexive173  . have value := discreteDistance.distinct with hx, hy, different174    rw value175    have one := realZero.lt_one176    linarith177178theorem discreteDistance.real (X x y : Set)179  requires hx : x ∈ X180  requires hy : y ∈ X181  shows Real(discreteDistance(X)(x, y))182proof183  have function := discreteDistance.function at X184  have pair := product.pair at x, y, X, X with hx, hy185  unfold Real186  unfold call2187  exact FunctionBetween.apply_closed with function, pair188189theorem discreteDistance.metric (X : Set)190  shows IsMetric(X, discreteDistance(X))191proof192  have one := realZero.lt_one193  constructor194  . exact discreteDistance.function at X195  . constructor196    . intros x hx y hy197      exact discreteDistance.nonnegative with hx, hy198    . constructor199      . intros x hx y hy200        constructor201        . intro zero202          by_contra203          have value := discreteDistance.distinct with hx, hy, this204          rw value at zero205          linarith206        . intro same207          rw same208          exact discreteDistance.self with hy209      . constructor210        . intros x hx y hy211          have split : x = y ∨ x ≠ y by tauto212          cases split with same | different213          . rw same214            rfl215          . have reversed : y ≠ x216              intro equal217              apply different218              symm at equal219              exact equal220            have valueXY := discreteDistance.distinct with hx, hy, different221            have valueYX := discreteDistance.distinct with hy, hx, reversed222            rw [valueXY, valueYX]223            rfl224        . intros x hx y hy z hz225          have nonnegativeXY := discreteDistance.nonnegative with hx, hy226          have nonnegativeYZ := discreteDistance.nonnegative with hy, hz227          have realXY := discreteDistance.real with hx, hy228          have realYZ := discreteDistance.real with hy, hz229          have realXZ := discreteDistance.real with hx, hz230          have splitXZ : x = z ∨ x ≠ z by tauto231          cases splitXZ with sameXZ | differentXZ232          . have self : discreteDistance(X)(x, z) = (0:R)233              rw sameXZ234              exact discreteDistance.self with hz235            rw self236            linarith237          . have valueXZ := discreteDistance.distinct with hx, hz, differentXZ238            rw valueXZ239            have splitXY : x = y ∨ x ≠ y by tauto240            cases splitXY with sameXY | differentXY241            . have differentYZ : y ≠ z242                intro equal243                apply differentXZ244                rw sameXY245                exact equal246              have valueYZ := discreteDistance.distinct with hy, hz, differentYZ247              rw valueYZ248              linarith249            . have valueXY := discreteDistance.distinct with hx, hy, differentXY250              rw valueXY251              linarith252253-- Balls of radius at most one are singletons; larger balls are the space.254theorem discreteDistance.ball_small (X x : Set, r : Real)255  requires hx : x ∈ X256  requires positive : 0 < r257  requires small : r ≤ 1258  shows ball(X, discreteDistance(X), x, r) = {x}259proof260  ext y261  constructor262  . intro hy263    have hyX := ball.point with hy264    have near := ball.distance with hy265    have split : x = y ∨ x ≠ y by tauto266    cases split with same | different267    . rw ← same268      exact singleton.self at x269    . exfalso270      have value := discreteDistance.distinct with hx, hyX, different271      rw value at near272      linarith273  . intro hy274    have same := singleton.membership.forward with hy275    rw same276    apply ball.of_distance with hx277    have self := discreteDistance.self with hx278    rw self279    exact positive280281theorem discreteDistance.ball_large (X x : Set, r : Real)282  requires hx : x ∈ X283  requires large : 1 < r284  shows ball(X, discreteDistance(X), x, r) = X285proof286  apply Subset.antisymmetric287  . exact ball.subset at X, discreteDistance(X), x, r288  . intros y hy289    have bound := discreteDistance.le_one with hx, hy290    have real := discreteDistance.real with hx, hy291    apply ball.of_distance with hy292    linarith293294theorem discreteDistance.open (X U : Set)295  requires inside : U ⊆ X296  shows MetricOpen(X, discreteDistance(X), U)297proof298  constructor299  . exact inside300  . intros x hx301    have hxX := inside with x, hx302    have oneReal : (1:R) ∈ ℝ by typecheck303    have positive : (0:R) < 1 by linarith304    have reflexive : (1:R) ≤ 1 by linarith305    refine ⟨(1:R), oneReal, positive, ?_⟩306    have singleton := discreteDistance.ball_small at X, x, (1:R) with307      hxX, positive, reflexive308    rw singleton309    intros y hy310    have same := singleton.membership.forward with hy311    rw same312    exact hx313314theorem discreteDistance.topology (X : Set)315  shows metricTopology(X, discreteDistance(X)) = 𝒫(X)316proof317  apply Subset.antisymmetric318  . exact metricTopology.subset_powerset at X, discreteDistance(X)319  . intros U hU320    have inside := powerset.membership_iff.forward with hU321    exact metricTopology.of_open with (discreteDistance.open with inside)322323theorem discreteDistance.closed (X C : Set)324  requires inside : C ⊆ X325  shows MetricClosed(X, discreteDistance(X), C)326proof327  apply MetricClosed.of_complement_open with inside328  exact discreteDistance.open with (complement.subset at X, C)329330theorem discreteDistance.bounded (X S : Set)331  requires inside : S ⊆ X332  shows IsBounded(X, discreteDistance(X), S)333proof334  apply IsBounded.of_bound at X, discreteDistance(X), S, (1:R) with inside335  intros x hx y hy336  exact discreteDistance.le_one with (inside with x, hx), (inside with y, hy)337338-- Every map out of a discrete space is uniformly continuous.339theorem discreteDistance.uniformly_continuous (f X Y e : Set)340  requires metric : IsMetric(Y, e)341  requires function : f : X → Y342  shows IsUniformlyContinuous(f, X, discreteDistance(X), Y, e)343proof344  apply IsUniformlyContinuous.of_control with function345  intros ε hε positive346  have oneReal : (1:R) ∈ ℝ by typecheck347  have one : (0:R) < 1 by linarith348  refine ⟨(1:R), oneReal, one, ?_⟩349  intros x hx y hy near350  have split : x = y ∨ x ≠ y by tauto351  cases split with same | different352  . rw same353    have image := FunctionBetween.apply_closed with function, hy354    have self := IsMetric.self with metric, image355    rw self356    exact positive357  . exfalso358    have value := discreteDistance.distinct with hx, hy, different359    rw value at near360    linarith361362theorem discreteDistance.continuous (f X Y e : Set)363  requires metric : IsMetric(Y, e)364  requires function : f : X → Y365  shows IsMetricContinuous(f, X, discreteDistance(X), Y, e)366proof367  have uniform := discreteDistance.uniformly_continuous with metric, function368  exact IsUniformlyContinuous.continuous with uniform369370-- A Cauchy sequence in a discrete space is eventually constant.371theorem discreteDistance.cauchy_eventually_constant (X u : Set)372  requires cauchy : IsCauchy(X, discreteDistance(X), u)373  shows ∃ N ∈ ℕ, ∀ n ∈ ℕ, (N ≤ n → u(n) = u(N))374proof375  have sequence := IsCauchy.sequence with cauchy376  have one : (0:R) < 1 by linarith377  obtain ⟨N, hN, close⟩ := IsCauchy.eventually with cauchy, one378  have natN : Nat(N) by exact hN379  refine ⟨N, hN, ?_⟩380  intros n hn le381  have termN := SequenceIn.term_of_member with sequence, hN382  have termn := SequenceIn.term_of_member with sequence, hn383  have near := close with n, hn, N, hN, le, (LessEqual.reflexive at N)384  by_contra385  have value := discreteDistance.distinct with termn, termN, this386  rw value at near387  linarith388389theorem discreteDistance.complete (X : Set)390  shows IsComplete(X, discreteDistance(X))391proof392  have metric := discreteDistance.metric at X393  apply IsComplete.of_limits with metric394  intros u cauchy395  have sequence := IsCauchy.sequence with cauchy396  obtain ⟨N, hN, constant⟩ :=397    discreteDistance.cauchy_eventually_constant with cauchy398  have termN := SequenceIn.term_of_member with sequence, hN399  refine ⟨u(N), termN, ?_⟩400  apply ConvergesIn.of_eventually with sequence, termN401  intros ε hε positive402  refine ⟨N, hN, ?_⟩403  intros n hn le404  have same := constant with n, hn, le405  rw same406  have self := discreteDistance.self with termN407  rw self408  exact positive409