Documentation

Mathlib.Geometry.Manifold.ConformalGroupoid

Conformal Groupoid #

In this file we define the groupoid of conformal maps on normed spaces.

Main definitions #

Tags #

conformal, groupoid

The pregroupoid of conformal maps.

Equations
  • conformalPregroupoid = { property := fun (f : XX) (u : Set X) => xu, ConformalAt f x, comp := , id_mem := , locality := , congr := }
Instances For

    The groupoid of conformal maps.

    Equations
    • conformalGroupoid = conformalPregroupoid.groupoid
    Instances For