MathlibAnnex.symmetricLens
def
Names the intersection of two closed balls with a common radius.
Statement
Let be a normed additive commutative group, let , and let . The symmetric lens with foci and radius is the set defined below.
Definition
Write . Then Thus membership imposes both closed distance bounds with the same radius.
Assumptions
Only the normed additive commutative group , two points , and a real number are required. The foci may coincide, and need not be positive.
Conclusion
The output is a subset of , symmetric in its two foci: . If , it is empty because norms are nonnegative. No midpoint or reflection assertion is part of this definition.
Main citations
Lean source signature (exact)
The complete declaration below is a separate exact source excerpt; the original header record is retained with the manuscript.
/-- The intersection of two closed balls with the same radius. -/
def symmetricLens (x y : E) (r : ℝ) : Set E :=
closedBall x r ∩ closedBall y r| In the source | Mathematical meaning |
|---|---|
(x y : E) (r : ℝ) |
The two points of the normed additive commutative group , and their common real radius . No real scalar multiplication or positive-radius hypothesis is required. |
: Set E |
The output is a set whose elements are points . |
closedBall x r ∩ closedBall y r |
The complete right-hand side: exactly when and . |
Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project
Exact content identity
Declaration: MathlibAnnex.symmetricLens
Accepted content SHA-256: 4b43206779c0b263bb6797dac39922b99d2b9f426f345630054bf01c568c436c
Accepted source guide SHA-256: 6cdfcba722a5b82d71ca123ad300523dc190c4dd9c6a7bb96a6bfb9d4672bc2f
Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73