-- Closed sets in a metric space: closed balls, spheres, and points are
-- closed; a point lies in the closure of a set exactly when every ball
-- around it meets the set
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Metric.Closed
import Open

predicate MetricClosed (X d C : Set) := IsClosed(X, metricTopology(X, d), C)

theorem MetricClosed.subset (X d C : Set)
  requires closed : MetricClosed(X, d, C)
  shows C ⊆ X
proof
  unfold MetricClosed at closed
  exact closed.left

theorem MetricClosed.complement_open (X d C : Set)
  requires closed : MetricClosed(X, d, C)
  shows MetricOpen(X, d, complement(X, C))
proof
  unfold MetricClosed at closed
  exact metricTopology.open with closed.right

theorem MetricClosed.of_complement_open (X d C : Set)
  requires inside : C ⊆ X
  requires open : MetricOpen(X, d, complement(X, C))
  shows MetricClosed(X, d, C)
proof
  unfold MetricClosed
  exact ⟨inside, (metricTopology.of_open with open)⟩

theorem MetricOpen.complement_closed (X d U : Set)
  requires metric : IsMetric(X, d)
  requires open : MetricOpen(X, d, U)
  shows MetricClosed(X, d, complement(X, U))
proof
  have topology := metricTopology.topology with metric
  exact Open.complement_closed with topology, (metricTopology.of_open with open)

theorem MetricClosed.whole (X d : Set)
  requires metric : IsMetric(X, d)
  shows MetricClosed(X, d, X)
proof
  exact IsClosed.whole with (metricTopology.topology with metric)

theorem MetricClosed.empty (X d : Set)
  requires metric : IsMetric(X, d)
  shows MetricClosed(X, d, ∅)
proof
  exact IsClosed.empty with (metricTopology.topology with metric)

theorem MetricClosed.union2 (X d C D : Set)
  requires metric : IsMetric(X, d)
  requires hC : MetricClosed(X, d, C)
  requires hD : MetricClosed(X, d, D)
  shows MetricClosed(X, d, C ∪ D)
proof
  have topology := metricTopology.topology with metric
  unfold MetricClosed at hC
  unfold MetricClosed at hD
  exact IsClosed.union2 with topology, hC, hD

theorem MetricClosed.intersection2 (X d C D : Set)
  requires metric : IsMetric(X, d)
  requires hC : MetricClosed(X, d, C)
  requires hD : MetricClosed(X, d, D)
  shows MetricClosed(X, d, C ∩ D)
proof
  have topology := metricTopology.topology with metric
  unfold MetricClosed at hC
  unfold MetricClosed at hD
  exact IsClosed.intersection2 with topology, hC, hD

theorem MetricClosed.family_intersection (X d S : Set)
  requires metric : IsMetric(X, d)
  requires nonempty : Nonempty(S)
  requires closed : ∀ C ∈ S, MetricClosed(X, d, C)
  shows MetricClosed(X, d, ⋂(S))
proof
  have topology := metricTopology.topology with metric
  have members : ∀ C ∈ S, IsClosed(X, metricTopology(X, d), C)
    intros C hC
    have closedC := closed with C, hC
    unfold MetricClosed at closedC
    exact closedC
  exact IsClosed.family_intersection with topology, nonempty, members

-- A point outside a closed set has a ball missing the set.
theorem MetricClosed.ball_disjoint (X d C x : Set)
  requires closed : MetricClosed(X, d, C)
  requires hx : x ∈ X
  requires outside : ¬x ∈ C
  shows ∃ r ∈ ℝ, 0 < r ∧ Disjoint(ball(X, d, x, r), C)
proof
  have open := MetricClosed.complement_open with closed
  have member : x ∈ complement(X, C) := complement.membership.backward with
    ⟨hx, outside⟩
  obtain ⟨r, hr, positive, inside⟩ := MetricOpen.ball_inside with open, member
  refine ⟨r, hr, positive, ?_⟩
  apply Disjoint.iff.backward
  intros y hy hyC
  have away := complement.membership.forward with (inside with y, hy)
  exact away.right with hyC

theorem MetricClosed.of_ball_disjoint (X d C : Set)
  requires inside : C ⊆ X
  requires separated :
    ∀ x ∈ X, ¬x ∈ C → ∃ r ∈ ℝ, 0 < r ∧ Disjoint(ball(X, d, x, r), C)
  shows MetricClosed(X, d, C)
proof
  apply MetricClosed.of_complement_open with inside
  constructor
  . exact complement.subset at X, C
  . intros x hx
    have parts := complement.membership.forward with hx
    obtain ⟨r, hr, positive, disjoint⟩ :=
      separated with x, parts.left, parts.right
    refine ⟨r, hr, positive, ?_⟩
    intros y hy
    have hyX := ball.point with hy
    have away := Disjoint.iff.forward with disjoint
    exact complement.membership.backward with ⟨hyX, (away with y, hy)⟩

-- A point of X every ball around which meets a closed set belongs to it.
theorem MetricClosed.of_balls_meet (X d C x : Set)
  requires closed : MetricClosed(X, d, C)
  requires hx : x ∈ X
  requires meets : ∀ r ∈ ℝ, 0 < r → Nonempty(ball(X, d, x, r) ∩ C)
  shows x ∈ C
proof
  by_contra outside
  obtain ⟨r, hr, positive, disjoint⟩ :=
    MetricClosed.ball_disjoint with closed, hx, outside
  obtain ⟨y, hy⟩ := meets with r, hr, positive
  have both := intersection.membership.forward with hy
  have away := Disjoint.iff.forward with disjoint
  exact away with y, both.left, both.right

theorem MetricClosed.of_limit_points (X d C : Set)
  requires inside : C ⊆ X
  requires limits : ∀ x ∈ X,
    (∀ r ∈ ℝ, 0 < r → Nonempty(ball(X, d, x, r) ∩ C)) → x ∈ C
  shows MetricClosed(X, d, C)
proof
  apply MetricClosed.of_ball_disjoint with inside
  intros x hx outside
  by_contra none
  apply outside
  apply limits with x, hx
  intros r hr positive
  by_contra empty
  apply none
  refine ⟨r, hr, positive, ?_⟩
  apply Disjoint.iff.backward
  intros y hy hyC
  apply empty
  witness y
  exact intersection.membership.backward with ⟨hy, hyC⟩

theorem closedBall.closed (X d x : Set, r : Real)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  shows MetricClosed(X, d, closedBall(X, d, x, r))
proof
  apply MetricClosed.of_ball_disjoint with (closedBall.subset at X, d, x, r)
  intros y hy outside
  have dxy := IsMetric.real with metric, hx, hy
  have far : r < d(x, y)
    have order := realLess.trichotomy at r, d(x, y)
    rcases order with less | equal | greater
    . exact less
    . exfalso
      apply outside
      apply closedBall.of_distance with hy
      rw ← equal
      exact realLe.reflexive
    . exfalso
      apply outside
      exact closedBall.of_distance with hy, (realLess.implies_le with greater)
  have radiusReal : d(x, y) - r ∈ ℝ by typecheck
  have positive : (0:R) < d(x, y) - r by linarith
  refine ⟨d(x, y) - r, radiusReal, positive, ?_⟩
  apply Disjoint.iff.backward
  intros z hz inBall
  have hzX := ball.point with hz
  have near := ball.distance with hz
  have close := closedBall.distance with inBall
  have triangle := IsMetric.triangle_to with metric, hx, hy, hzX
  have dyz := IsMetric.real with metric, hy, hzX
  have dxz := IsMetric.real with metric, hx, hzX
  linarith

theorem ball.complement_closed (X d x : Set, r : Real)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  shows MetricClosed(X, d, complement(X, ball(X, d, x, r)))
proof
  exact MetricOpen.complement_closed with metric, (ball.open with metric, hx)

theorem closedBall.complement_open (X d x : Set, r : Real)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  shows MetricOpen(X, d, complement(X, closedBall(X, d, x, r)))
proof
  exact MetricClosed.complement_open with (closedBall.closed with metric, hx)

theorem sphere.closed (X d x : Set, r : Real)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  shows MetricClosed(X, d, sphere(X, d, x, r))
proof
  apply MetricClosed.of_ball_disjoint with (sphere.subset at X, d, x, r)
  intros y hy outside
  have dxy := IsMetric.real with metric, hx, hy
  have order := realLess.trichotomy at d(x, y), r
  rcases order with less | equal | greater
  . have radiusReal : r - d(x, y) ∈ ℝ by typecheck
    have positive : (0:R) < r - d(x, y) by linarith
    refine ⟨r - d(x, y), radiusReal, positive, ?_⟩
    apply Disjoint.iff.backward
    intros z hz onSphere
    have hzX := ball.point with hz
    have near := ball.distance with hz
    obtain ⟨hzX2, equal⟩ := sphere.membership.forward with onSphere
    have triangle := IsMetric.triangle with metric, hx, hy, hzX
    have dyz := IsMetric.real with metric, hy, hzX
    have dxz := IsMetric.real with metric, hx, hzX
    linarith
  . exfalso
    apply outside
    exact sphere.membership.backward with ⟨hy, equal⟩
  . have radiusReal : d(x, y) - r ∈ ℝ by typecheck
    have positive : (0:R) < d(x, y) - r by linarith
    refine ⟨d(x, y) - r, radiusReal, positive, ?_⟩
    apply Disjoint.iff.backward
    intros z hz onSphere
    have hzX := ball.point with hz
    have near := ball.distance with hz
    obtain ⟨hzX2, equal⟩ := sphere.membership.forward with onSphere
    have triangle := IsMetric.triangle_to with metric, hx, hy, hzX
    have dyz := IsMetric.real with metric, hy, hzX
    have dxz := IsMetric.real with metric, hx, hzX
    linarith

theorem singleton.metric_closed (X d x : Set)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  shows MetricClosed(X, d, {x})
proof
  have topology := metricTopology.topology with metric
  have hausdorff := metricTopology.hausdorff with metric
  exact IsHausdorff.singleton_closed with topology, hausdorff, hx

theorem sphere.eq_difference (X d x : Set, r : Real)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  shows sphere(X, d, x, r) = closedBall(X, d, x, r) ∖ ball(X, d, x, r)
proof
  have disjoint := sphere.disjoint_ball at X, d, x, r
  have separated := Disjoint.iff.forward with disjoint
  ext y
  constructor
  . intro hy
    have inside := sphere.subset_closedBall with metric, hx
    have inClosed := inside with y, hy
    apply difference.membership.backward
    exact ⟨inClosed, (separated with y, hy)⟩
  . intro hy
    have parts := difference.membership.forward with hy
    have split := closedBall.eq_ball_union_sphere with metric, hx
    rw split at parts
    have cases := union2.membership.forward with parts.left
    cases cases with inBall | onSphere
    . exfalso
      exact parts.right with inBall
    . exact onSphere

-- Closure: a point is in the closure of A exactly when every ball around
-- it meets A.
theorem metricClosure.membership (X d A x : Set)
  requires metric : IsMetric(X, d)
  requires hA : A ⊆ X
  shows x ∈ closure(X, metricTopology(X, d), A) ↔
    x ∈ X ∧ (∀ r ∈ ℝ, 0 < r → Nonempty(ball(X, d, x, r) ∩ A))
proof
  have topology := metricTopology.topology with metric
  have characterization :=
    closure.membership at X, metricTopology(X, d), A, x with
    topology, hA
  constructor
  . intro hx
    obtain ⟨hxX, touches⟩ := characterization.forward with hx
    refine ⟨hxX, ?_⟩
    intros r hr positive
    have openBall := ball.member_topology at X, d, x, r with metric, hxX
    have center := ball.center with metric, hxX, positive
    exact touches with ball(X, d, x, r), openBall, center
  . intro data
    obtain ⟨hxX, meets⟩ := data
    apply characterization.backward
    refine ⟨hxX, ?_⟩
    intros U hU hxU
    obtain ⟨r, hr, positive, inside⟩ := metricTopology.ball_inside with hU, hxU
    obtain ⟨y, hy⟩ := meets with r, hr, positive
    have both := intersection.membership.forward with hy
    witness y
    exact intersection.membership.backward with ⟨(inside with
      y, both.left), both.right⟩

theorem metricClosure.ball_meets (X d A x : Set, r : Real)
  requires metric : IsMetric(X, d)
  requires hA : A ⊆ X
  requires hx : x ∈ closure(X, metricTopology(X, d), A)
  requires positive : 0 < r
  shows Nonempty(ball(X, d, x, r) ∩ A)
proof
  have characterization := metricClosure.membership at X, d, A, x with
    metric, hA
  obtain ⟨hxX, meets⟩ := characterization.forward with hx
  have realR : r ∈ ℝ by typecheck
  exact meets with r, realR, positive

theorem metricClosure.of_balls_meet (X d A x : Set)
  requires metric : IsMetric(X, d)
  requires hA : A ⊆ X
  requires hx : x ∈ X
  requires meets : ∀ r ∈ ℝ, 0 < r → Nonempty(ball(X, d, x, r) ∩ A)
  shows x ∈ closure(X, metricTopology(X, d), A)
proof
  have characterization := metricClosure.membership at X, d, A, x with
    metric, hA
  exact characterization.backward with ⟨hx, meets⟩

theorem ball.closure_subset_closedBall (X d x : Set, r : Real)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  shows
    closure(X, metricTopology(X, d), ball(X, d, x, r)) ⊆ closedBall(X, d, x, r)
proof
  have topology := metricTopology.topology with metric
  have closed := closedBall.closed at X, d, x, r with metric, hx
  have inside := ball.subset_closedBall with metric, hx
  unfold MetricClosed at closed
  exact closure.least with closed, inside

theorem closedBall.closure (X d x : Set, r : Real)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  shows closure(X, metricTopology(X, d), closedBall(X, d, x, r)) =
    closedBall(X, d, x, r)
proof
  have topology := metricTopology.topology with metric
  have closed := closedBall.closed at X, d, x, r with metric, hx
  unfold MetricClosed at closed
  exact closure.of_closed with topology, closed

-- A set is dense exactly when every ball meets it.
theorem metricDense.iff (X d A : Set)
  requires metric : IsMetric(X, d)
  requires hA : A ⊆ X
  shows IsDense(X, metricTopology(X, d), A) ↔
    (∀ x ∈ X, ∀ r ∈ ℝ, 0 < r → Nonempty(ball(X, d, x, r) ∩ A))
proof
  have topology := metricTopology.topology with metric
  constructor
  . intro dense
    intros x hx r hr positive
    unfold IsDense at dense
    have inClosure : x ∈ closure(X, metricTopology(X, d), A)
      rw dense
      exact hx
    exact metricClosure.ball_meets with metric, hA, inClosure, positive
  . intro meets
    unfold IsDense
    apply Subset.antisymmetric
    . exact closure.subset with topology, hA
    . intros x hx
      exact metricClosure.of_balls_meet with metric, hA, hx, (meets with x, hx)

theorem metricDense.whole (X d : Set)
  requires metric : IsMetric(X, d)
  shows IsDense(X, metricTopology(X, d), X)
proof
  have topology := metricTopology.topology with metric
  unfold IsDense
  exact closure.of_closed with topology, (IsClosed.whole with topology)