bijective

Mathlib.Topology.MetricSpace.DilationEquiv

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

English

A DilationEquiv map e is bijective as a function.

Русский

DilationEquiv e является биективным отображением.

LaTeX

$$$\forall e : X \simeq^{\mathrm{d}} Y,\ Function.Bijective (e)$$$

Lean4

protected theorem bijective (e : X ≃ᵈ Y) : Bijective e :=
  e.1.bijective

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

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

Разделы

Аффилиация

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