Theorems · Definition · general topology

IsometryEquiv.sumArrowIsometryEquivProdArrow

{α : Type u} →
  {β : Type v} →
    {γ : Type w} →
      [inst : PseudoEMetricSpace γ] → [inst_1 : Fintype α] → [inst_2 : Fintype β] → (α ⊕ β → γ) ≃ᵢ (α → γ) × (β → γ)

The natural isometry (α ⊕ β → γ) ≃ᵢ (α → γ) × (β → γ) between the type of maps on a sum of fintypes α ⊕ β and the pairs of functions on the types α and β. Equiv.sumArrowEquivProdArrow as an IsometryEquiv.

Defined in

Mathlib.Topology.MetricSpace.Isometry

Cited by

3 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpaceFintypeFintype