Symmetric lens

MathlibAnnex.symmetricLens

Names the reflection-symmetric bounded region used to force preservation of a midpoint.

Statement

`symmetricLens x y r` is the intersection of the two closed balls of radius r centered at x and y.

Definition

A point lies in the symmetric lens exactly when its distance from each focus is at most r. The common midpoint is the center of the point-reflection symmetry that exchanges the two foci.

Assumptions

A normed additive commutative group E; points x and y; a real radius r.

Conclusion

The symmetric lens is the intersection of the closed radius-r balls centered at x and y. This definition needs no positivity assumption.

Main citations

Lean source signature (exact)

def symmetricLens (x y : E) (r : ℝ) : Set E

Read exact source with highlighted declaration