Theorems · Definition · general topology

IsometryClass.casesOn

{F : Type u_3} →
  {α : Type u_4} →
    {β : Type u_5} →
      [inst : PseudoEMetricSpace α] →
        [inst_1 : PseudoEMetricSpace β] →
          [inst_2 : FunLike F α β] →
            {motive : IsometryClass F α β → Sort u} →
              (t : IsometryClass F α β) → ((isometry : ∀ (f : F), Isometry ⇑f) → motive ⋯) → motive t

Defined in

Mathlib.Topology.MetricSpace.Isometry

Cited by

0 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpacePseudoEMetricSpaceFunLike