flip — Mathlib

English

If f is a locally constant function to α → β, then for any a ∈ α, the map x ↦ f(x)(a) is locally constant.

Русский

Если f — локально константная функция в α → β, то для каждого a ∈ α отображение x ↦ f(x)(a) локально константно.

LaTeX

$$$\\text{flip}: {X,α,β} \\, (f: \\mathrm{LocallyConstant}(X,(α\\to β))) \\to (α \\to \\mathrm{LocallyConstant}(X,β))$ с $\text{flip}(f,a)(x) = f(x)(a)$$$

Lean4

/-- Given a locally constant function to `α → β`, construct a family of locally constant
functions with values in β indexed by α. -/
def flip {X α β : Type*} [TopologicalSpace X] (f : LocallyConstant X (α → β)) (a : α) : LocallyConstant X β :=
  f.map fun f => f a

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