Theorems · Theorem · geometry

Filter.Tendsto.inversion

∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {α : Type u_3} {x c : P} {R : ℝ} {l : Filter α} {fc fx : α → P} {fR : α → ℝ},
  Filter.Tendsto fc l (nhds c) →
    Filter.Tendsto fR l (nhds R) →
      Filter.Tendsto fx l (nhds x) →
        x ≠ c →
          Filter.Tendsto (fun a => EuclideanGeometry.inversion (fc a) (fR a) (fx a)) l
            (nhds (EuclideanGeometry.inversion c R x))

Defined in

Mathlib.Geometry.Euclidean.Inversion.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsor