SelectedClass

Definition

by transmogrifier · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

For a finite set of points A, a source point s, and a radius d, the selected distance class consists of the points of A at distance d from s.

Definition code

import Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
import Mathlib.Geometry.Euclidean.Sphere.Basic
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Data.Real.Basic
noncomputable def Batch3N9.Problem97.SelectedClass (A : Finset (EuclideanSpace ℝ (Fin 2))) (s : EuclideanSpace ℝ (Fin 2)) (d : ℝ) : Finset (EuclideanSpace ℝ (Fin 2)) :=
  A.filter (fun q => dist s q = d)

Source

https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P97/WitnessPacketInterface.lean

View graph