English
There is a natural equivalence between the dependent sum (PSigma) over α with fibers β i and the ordinary Sigma type: (Σ' i, β i) ≃ Σ i, β i, given by (i, b) ↦ ⟨i, b⟩ and ⟨i, b⟩ ↦ (i, b).
Русский
Существует естественная эквивалентность между зависимой суммой (PSigma) над α с волокнами β(i) и обычной сигмой: (Σ' i, β i) ≃ Σ i, β i, задаваемая отображениями (i, b) ↦ ⟨i, b⟩ и ⟨i, b⟩ ↦ (i, b).
LaTeX
$$$$(\Sigma' i:\alpha,\beta(i)) \cong \Sigma i:\alpha,\beta(i).$$$$
Lean4
/-- A `PSigma`-type is equivalent to the corresponding `Sigma`-type. -/
@[simps (attr := grind =) apply symm_apply]
def psigmaEquivSigma {α} (β : α → Type*) : (Σ' i, β i) ≃ Σ i, β i
where
toFun a := ⟨a.1, a.2⟩
invFun a := ⟨a.1, a.2⟩
