mathlib documentation

core.init.data.sigma.basic

source
theorem ex_of_psig {α : Type u} {p : α → Prop} (a : Σ' (x : α), p x) :
∃ (x : α), p x

source
theorem sigma.eq {α : Type u} {β : α → Type v} {p₁ p₂ : Σ (a : α), β a} (h₁ : p₁.fst = p₂.fst) (a : h₁.rec_on p₁.snd = p₂.snd) :
p₁ = p₂

source
theorem psigma.eq {α : Sort u} {β : α → Sort v} {p₁ p₂ : psigma β} (h₁ : p₁.fst = p₂.fst) (a : h₁.rec_on p₁.snd = p₂.snd) :
p₁ = p₂