Circle

Definition

Let $d$ be the Euclidean distance on the Euclidean plane $\mathbb{R}^2$. Let $c \in \mathbb{R}^2$ be a point and $r > 0$ a real number. The circle with the centre $c$ and the radius $r$ is the set $$\{\, x \in \mathbb{R}^2 \;:\; d(x, c) = r \,\}.$$ With $c = (a, b)$, it is the set of the points $(x, y)$ with $(x - a)^2 + (y - b)^2 = r^2$.

Remarks

A chord is a segment between two points of the circle. A diameter is a chord through the centre, and its length is $2r$. The circle has the length $2 \pi r$ and bounds a disc of area $\pi r^2$. A circle in $\mathbb{R}^n$ is a circle in some plane of $\mathbb{R}^n$. Mathlib's EuclideanGeometry.Sphere is the sphere of a centre and a radius in a metric space; in the plane it is a circle.

Explanations

L1 human

A circle is what a compass draws: all the points at one fixed distance from the centre. The unit circle has the centre $(0, 0)$ and the radius $1$. It is the set of the points with $x^2 + y^2 = 1$.