English
The product over Option α of β a is the product of β none with the function space α → β (some a).
Русский
Произведение по Option α для β является произведением β none и функции α → β (some a).
LaTeX
$$$ (\\forall a:\\text{Option }\\alpha, \\beta(a)) \\simeq \\beta(\\text{none}) \\times \\forall a:\\alpha, \\beta(\\text{some}(a)). $$$
Lean4
/-- The product over `Option α` of `β a` is the binary product of the
product over `α` of `β (some α)` and `β none` -/
@[simps]
def piOptionEquivProd {α} {β : Option α → Type*} : (∀ a : Option α, β a) ≃ β none × ∀ a : α, β (some a)
where
toFun f := (f none, fun a => f (some a))
invFun x a := Option.casesOn a x.fst x.snd
left_inv f := funext fun a => by cases a <;> rfl
