coe_toOrderIso

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

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

English

Two CircleDeg1Lift maps are equal if they agree on all inputs.

Русский

Две отображения CircleDeg1Lift равны, если они совпадают на всех аргументах.

LaTeX

$$$\\forall \\{f,g : CircleDeg1Lift\\}, (\\forall x, f x = g x) \\Rightarrow f = g$$$

Lean4

@[simp]
theorem coe_toOrderIso (f : CircleDeg1Liftˣ) : ⇑(toOrderIso f) = f :=
  rfl

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

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

Разделы

Аффилиация

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