---
tag: 045DN06F3S
kind: definition
name: Circle
msc: [51M04]
defines: 060W5CBZP6
uses: [0XW7V9ZZ05, 0NPPGHQNXQ]
sources:
  - url: https://en.wikipedia.org/wiki/Circle
    locator: lead section
  - url: https://en.wikipedia.org/wiki/Circle
    locator: Terminology
  - url: https://en.wikipedia.org/wiki/Circle
    locator: Equation of a circle
---

## Definition

Let $d$ be the [[Euclidean distance|0NPPGHQNXQ]] on the [[Euclidean plane|0XW7V9ZZ05]] $\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$.