instDilationEquivClass

Mathlib.Topology.MetricSpace.DilationEquiv

URI: https://scilib.ai/kg/mathlib#DilationEquiv.instDilationEquivClass

English

If two DilationEquiv maps agree on every input, they are equal as maps.

Русский

Если две дилатационные эквивалентности согласуются при каждом аргументе, то они равны как отображения.

LaTeX

$$$\forall e \, e' : X \simeq^{\mathrm{d}} Y,\ (\forall x, e(x) = e'(x)) \Rightarrow e = e'$$$

Lean4

instance : DilationEquivClass (X ≃ᵈ Y) X Y where edist_eq' f := f.edist_eq'

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

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

Разделы

Аффилиация

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