Theorems · Inductive type · general topology

IsometryClass

(F : Type u_3) →
  (α : outParam (Type u_4)) →
    (β : outParam (Type u_5)) → [PseudoEMetricSpace α] → [PseudoEMetricSpace β] → [FunLike F α β] → Prop

IsometryClass F α β states that F is a type of isometries.

Defined in

Mathlib.Topology.MetricSpace.Isometry

Cited by

19 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

PseudoEMetricSpacePseudoEMetricSpaceFunLike