Equivalences and sigma types

def Equiv.Set.sigma {α : Type u_2} {β : α → Type u_1} (s : Set α) (t : (i : α) → Set (β i)) : ↑(s.sigma t) ≃ (i : ↑s) × ↑(t ↑i)

The indexed sum of sets is equivalent to the sigma-type of their coercions to types.

Equations

• Equiv.Set.sigma s t = Equiv.subtypeSigmaEquivSigma