English
If p is true for all x in the range of f, then (Σ y : Subtype p, { x : α // f x = y }) ≃ α.
Русский
Если p истинно на диапазоне f, тогда (Σ y : Subtype p, { x : α // f x = y }) эквивалентно α.
LaTeX
$$$(\\Sigma y : Subtype p, { x : \\alpha // f x = y }) \\simeq \\alpha$ given h: ∀ x, p (f x)$$
Lean4
/-- If a predicate `p : β → Prop` is true on the range of a map `f : α → β`, then
`Σ y : {y // p y}, {x // f x = y}` is equivalent to `α`. -/
def sigmaSubtypeFiberEquiv {α β : Type*} (f : α → β) (p : β → Prop) (h : ∀ x, p (f x)) :
(Σ y : Subtype p, { x : α // f x = y }) ≃ α :=
calc
_ ≃ Σ y : β, { x : α // f x = y } := sigmaSubtypeEquivOfSubset _ p fun _ ⟨x, h'⟩ => h' ▸ h x
_ ≃ α := sigmaFiberEquiv f
