coe_coeHom

Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

URI: https://scilib.ai/kg/mathlib#Real.Angle.coe_coeHom

English

The two representations of the real→angle coercion agree pointwise.

Русский

Две трактовки отображения ℝ → Angle совпадают на каждой точке.

LaTeX

$$$$ \forall r\in\mathbb{R},\ \mathrm{coeHom}(r) = \mathrm{coe}(r). $$$$

Lean4

@[simp]
theorem coe_coeHom : (coeHom : ℝ → Angle) = ((↑) : ℝ → Angle) :=
  rfl

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

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

Разделы

Аффилиация

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