Documentation Verification Report

Sphere

📁 Source: Mathlib/Topology/Compactification/OnePoint/Sphere.lean

Statistics

MetricCount
DefinitionsSphere, onePointEquivSphereOfFinrankEq, onePointHyperplaneHomeoUnitSphere
3
Theorems0
Total3

EuclideanGeometry

Definitions

NameCategoryTheorems
Sphere 📖CompData
41 mathmath: subset_sphere, Sphere.thales_theorem, Sphere.isDiameter_iff_right_mem_and_midpoint_eq_center, Sphere.secondInter_mem, Sphere.IsExtTangentAt.mem_left, Affine.Simplex.mem_circumsphere, Sphere.isTangent_orthRadius_iff_mem, Sphere.isDiameter_iff_right_mem_and_pointReflection_center_right, Sphere.isTangentAt_orthRadius_iff_mem, instNonemptySphere, Sphere.IsDiameter.right_mem, Sphere.IsDiameter.left_mem, Affine.Triangle.altitudeFoot_mem_ninePointCircle, Affine.Simplex.eulerPoint_mem_ninePointCircle, Sphere.isExtTangentAt_center_iff, Affine.Simplex.ExcenterExists.touchpoint_mem_exsphere, Affine.Triangle.mem_circumsphere_of_two_zsmul_oangle_eq, Sphere.power_eq_zero_iff_mem_sphere, Sphere.IsTangentAt.mem_and_mem_iff_eq, Sphere.isIntTangentAt_self_iff_mem, mem_sphere, Sphere.IsIntTangentAt.mem_left, mem_sphere', Sphere.mem_coe, Sphere.isDiameter_iff_mem_and_mem_and_dist, Sphere.IsTangentAt.mem_sphere, Sphere.isDiameter_iff_mem_and_mem_and_wbtw, Sphere.IsExtTangentAt.mem_right, Affine.Simplex.faceOppositeCentroid_mem_ninePointCircle, Sphere.isIntTangentAt_center_iff, Sphere.mem_tangentSet_iff, Sphere.mem_coe', Affine.Simplex.orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle, Sphere.IsIntTangentAt.mem_right, Sphere.center_mem_iff, Sphere.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter, AffineIndependent.existsUnique_dist_eq, Sphere.isDiameter_iff_left_mem_and_midpoint_eq_center, Sphere.angle_eq_pi_div_two_iff_mem_sphere_ofDiameter, Sphere.isDiameter_iff_left_mem_and_pointReflection_center_left, Affine.Simplex.touchpoint_mem_insphere

(root)

Definitions

NameCategoryTheorems
onePointEquivSphereOfFinrankEq 📖CompOp
onePointHyperplaneHomeoUnitSphere 📖CompOp

---

← Back to Index