instCoeFunElemForallSetOfContinuous

English

Every continuous map is a function via a canonical coercion.

Русский

Каждая непрерывная функция рассматривается как функция посредством канонического приведения типа.

LaTeX

$$The set of continuous maps from α to β is equipped with a canonical coercion to functions, i.e. ContinuousMap α β → (α → β).$$

Lean4

instance : CoeFun {f : α → β | Continuous f} fun _ => α → β :=
  ⟨Subtype.val⟩

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