symm_inj

Mathlib.Topology.UnitInterval

URI: https://scilib.ai/kg/mathlib#unitInterval.symm_inj

English

The map i ↦ 1 − i on the unit interval I is injective.

Русский

Отображение i ↦ 1 − i на I инъективно.

LaTeX

$$$\forall i,j\in I,\ \sigma(i)=\sigma(j) \Rightarrow i=j$$$

Lean4

@[simp]
theorem symm_inj {i j : I} : σ i = σ j ↔ i = j :=
  symm_bijective.injective.eq_iff

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

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

Разделы

Аффилиация

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