English
A sigma type over a subtype is equivalent to the sigma type over the original type, provided the fiber is inhabited for every element of the subtype.
Русский
Сигма-тип над подмножеством эквивалентен сигма-типу над исходным типом при условии, что волокно непусто для каждого элемента подмножества.
LaTeX
$$$(\\Sigma x : Subtype q, p x) \\simeq (\\Sigma x : \\alpha, p x)$ with h: ∀ x, p x → q x$$
Lean4
/-- A sigma type over a subtype is equivalent to the sigma set over the original type,
if the fiber is empty outside of the subset -/
def sigmaSubtypeEquivOfSubset {α} (p : α → Type v) (q : α → Prop) (h : ∀ x, p x → q x) :
(Σ x : Subtype q, p x) ≃ Σ x : α, p x :=
(subtypeSigmaEquiv p q).symm.trans <| subtypeUnivEquiv fun x => h x.1 x.2
