bijective_cast

Mathlib.Topology.Path

URI: https://scilib.ai/kg/mathlib#Path.bijective_cast

English

The map x' ↦ Path.cast hx hy is a bijection on the space of paths; in particular, Path.cast hx hy is bijective.

Русский

Приведение пути образует биекцию на множество путей; в частности, Path.cast hx hy биективно.

LaTeX

$$Bijective (Path.cast hx hy)$$

Lean4

theorem bijective_cast {x' y' : X} (hx : x' = x) (hy : y' = y) : Bijective (Path.cast · hx hy) := by subst_vars;
  exact bijective_id

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

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

Разделы

Аффилиация

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