mem_coe' — Mathlib

English

A point lies on a sphere iff its distance to the center equals the radius: dist(p, s.center) = s.radius ⇔ p ∈ s.

Русский

Точка лежит на сфере тогда и только тогда, когда расстояние до центра сферы равно радиусу: dist(p, s.center) = s.radius ⇔ p ∈ s.

LaTeX

$$$$ \operatorname{dist}(p, s.center) = s.radius \;\iff\; p \in s. $$$$

Lean4

@[simp]
theorem mem_coe' {p : P} {s : Sphere P} : dist p s.center = s.radius ↔ p ∈ s :=
  Iff.rfl

Похожие утверждения