sigmaPreimageEquiv — Mathlib

English

There is a natural equivalence between the total space of all preimages (Σ b, f^{-1}({b})) and the domain α, given by (b, x) ↦ x.

Русский

Существует естественная эквивалентность между суммой по всем предобразам и множеством α, заданная отображением (b, x) ↦ x.

LaTeX

$$$(\\Sigma b:\\beta, f^{-1}({b})) \\cong \\alpha$$$

Lean4

/-- `sigmaPreimageEquiv f` for `f : α → β` is the natural equivalence between
the type of all preimages of points under `f` and the total space `α`. -/
@[simps!]
def sigmaPreimageEquiv {α β} (f : α → β) : (Σ b, f ⁻¹' { b }) ≃ α :=
  sigmaFiberEquiv f

Похожие утверждения