English
Let α be a type. The set of all functions from Bool to α is naturally isomorphic to the product α × α; specifically, f ↦ (f(false), f(true)) gives the isomorphism, with the inverse (a, b) ↦ (λ b' , if b' then b else a).
Русский
Пусть α — множество. Пространство функций из Bool в α естественно гомотетично произведению α × α: отображение f ↦ (f(false), f(true)) задаёт изоморфизм, а обратное отображение (a, b) ↦ (λ b', если b' тогда b иначе a) задаёт обратное.
LaTeX
$$$ (\\mathrm{Bool} \\to α) \\cong α \\times α $$$
Lean4
/-- The function type `Bool → α` is equivalent to `α × α`. -/
@[simps]
def boolArrowEquivProd (α : Type*) : (Bool → α) ≃ α × α
where
toFun f := (f false, f true)
invFun p b := if b then p.2 else p.1
left_inv _ := by grind
