induced

Mathlib.Topology.EMetricSpace.Defs

URI: https://scilib.ai/kg/mathlib#EMetricSpace.induced

Lean4

/-- The extended metric induced by an injective function taking values in an emetric space.
See Note [reducible non-instances]. -/
abbrev induced {γ β} (f : γ → β) (hf : Function.Injective f) (m : EMetricSpace β) : EMetricSpace γ :=
  { PseudoEMetricSpace.induced f m.toPseudoEMetricSpace with eq_of_edist_eq_zero := fun h => hf (edist_eq_zero.1 h) }

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru