flip_unflip — Mathlib

English

Let α be finite and f: α → LocallyConstant(X, β). Then (unflip f).flip = f; i.e., flipping twice on a finite-index family returns the original family.

Русский

Пусть α конечно и f: α → LocallyConstant(X, β). Тогда (unflip f).flip = f; то есть дважды выполнить операцию flip возвращает исходную семью.

LaTeX

$$$ (\\mathrm{unflip}\\, f).\\mathrm{flip} = f $$$

Lean4

@[simp]
theorem flip_unflip {X α β : Type*} [Finite α] [TopologicalSpace X] (f : α → LocallyConstant X β) :
    (unflip f).flip = f :=
  rfl

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