ofFun

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

URI: https://scilib.ai/kg/mathlib#UniformFun.ofFun

English

Equivalence between α → β and UniformFun α β.

Русский

Эквиваленция между множеством функций α → β и UniformFun α β.

LaTeX

$$$\\mathrm{UniformFun}(α,β) \\cong (α \\to β)$$$

Lean4

/-- Reinterpret `f : α → β` as an element of `α →ᵤ β`. -/
def ofFun : (α → β) ≃ (α →ᵤ β) :=
  ⟨fun x => x, fun x => x, fun _ => rfl, fun _ => rfl⟩

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

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

Разделы

Аффилиация

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