English
For any function f: α → β, there is a natural equivalence between the fibered total space Σ y∈β { x ∈ α | f x = y } and α, given by projection to x and its inverse x ↦ (f x, x).
Русский
Для любой функции f: α → β существует естественная эквивалентность между суммой-файбером и α, задаваемая проекцией на x и обратной связью x ↦ (f x, x).
LaTeX
$$$$\Bigl(\Sigma_{y:\beta} \{ x:\alpha \mid f(x)=y \} \Bigr) \simeq \alpha.$$$$
Lean4
/-- `sigmaFiberEquiv f` for `f : α → β` is the natural equivalence between
the type of all fibres of `f` and the total space `α`. -/
@[simps]
def sigmaFiberEquiv {α β : Type*} (f : α → β) : (Σ y : β, { x // f x = y }) ≃ α :=
⟨fun x => ↑x.2, fun x => ⟨f x, x, rfl⟩, fun ⟨_, _, rfl⟩ => rfl, fun _ => rfl⟩
