Theorems · Theorem · geometry

InnerProductGeometry.continuousAt_angle

∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x : V × V},
  x.1 ≠ 0 → x.2 ≠ 0 → ContinuousAt (fun y => InnerProductGeometry.angle y.1 y.2) x

Defined in

Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Cited by

1 results in Mathlib

Foundations

Depth 189 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpace