coe_toOrderIso_symm

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

URI: https://scilib.ai/kg/mathlib#CircleDeg1Lift.coe_toOrderIso_symm

English

For f ∈ CircleDeg1Liftˣ, ⇑(toOrderIso f) = f.

Русский

Для f ∈ CircleDeg1Liftˣ выполняется ⇑(toOrderIso f) = f.

LaTeX

$$$\\text{coe_toOrderIso}(f) = f$$$

Lean4

@[simp]
theorem coe_toOrderIso_symm (f : CircleDeg1Liftˣ) : ⇑(toOrderIso f).symm = (f⁻¹ : CircleDeg1Liftˣ) :=
  rfl

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

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

Разделы

Аффилиация

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