ball

Stream: new members

[BANGJI HU]

hi,everyone my problem is how to proove An object with a circle on any slice is a ball,and i d like hint,

[BANGJI HU]

import Mathlib.Geometry.Euclidean.Basic
def is_sphere (S : set ℝ³) : Prop :=
∃ (c : ℝ³) (r : ℝ), S = {x : ℝ³ | ∥x - c∥ = r}


def is_circle (C : set ℝ³) : Prop :=
∃ (p : plane ℝ³) (c : ℝ³) (r : ℝ), C = {x : ℝ³ | x ∈ p ∧ ∥x - c∥ = r}


def all_sections_are_circles (S : set ℝ³) : Prop :=
∀ (p : plane ℝ³), is_circle (S ∩ p.to_set)

theorem sections_are_circles_iff_sphere (S : set ℝ³) :
  all_sections_are_circles S ↔ is_sphere S :=

[Damiano Testa]

Opening this, I get expected token.