English
For finite α, unflip is the inverse operation to flip: unflip(flip f) = f.
Русский
Для конечного множества α операция unflip является обратной к flip: unflip(flip f) = f.
LaTeX
$$$\\text{unflip}: {X,α,β} \\to \\mathrm{LocallyConstant}(X,(α\\to β))$ и $\\text{unflip}(f.flip) = f$ (при конечном α)$$
Lean4
/-- If α is finite, this constructs a locally constant function to `α → β` given a
family of locally constant functions with values in β indexed by α. -/
def unflip {X α β : Type*} [Finite α] [TopologicalSpace X] (f : α → LocallyConstant X β) : LocallyConstant X (α → β)
where
toFun x a := f a x
isLocallyConstant :=
IsLocallyConstant.iff_isOpen_fiber.2 fun g =>
by
have : (fun (x : X) (a : α) => f a x) ⁻¹' { g } = ⋂ a : α, f a ⁻¹' {g a} := by ext; simp [funext_iff]
rw [this]
exact isOpen_iInter_of_finite fun a => (f a).isLocallyConstant _
