English
Bijection obtained by separating the term at index none of a dfinsupp over Option ι.
Русский
Перебрасывание dfinsupp через разбиение по индексу none в над Option ι.
LaTeX
$$$\\mathrm{equivProdDFinsupp} : (\\Pi_0 i, \\alpha i) \\simeq \\alpha(\\mathrm{none}) \\times (\\Pi_0 i, \\alpha(\\mathrm{some}~i))$$$
Lean4
/-- Bijection obtained by separating the term of index `none` of a dfinsupp over `Option ι`.
This is the dfinsupp version of `Equiv.piOptionEquivProd`. -/
@[simps]
noncomputable def equivProdDFinsupp [∀ i, Zero (α i)] : (Π₀ i, α i) ≃ α none × Π₀ i, α (some i)
where
toFun f := (f none, comapDomain some (Option.some_injective _) f)
invFun f := f.2.extendWith f.1
left_inv
f := by
ext i; obtain - | i := i
· rw [extendWith_none]
· rw [extendWith_some, comapDomain_apply]
right_inv
x := by
dsimp only
ext
· exact extendWith_none x.snd _
· rw [comapDomain_apply, extendWith_some]
