mathlib3 documentation

core / init.data.sigma.basic

theorem ex_of_psig {α : Type u} {p : α Prop} :
(Σ' (x : α), p x) ( (x : α), p x)
@[protected]
theorem sigma.eq {α : Type u} {β : α Type v} {p₁ p₂ : Σ (a : α), β a} (h₁ : p₁.fst = p₂.fst) :
h₁.rec_on p₁.snd = p₂.snd p₁ = p₂
@[protected]
theorem psigma.eq {α : Sort u} {β : α Sort v} {p₁ p₂ : psigma β} (h₁ : p₁.fst = p₂.fst) :
h₁.rec_on p₁.snd = p₂.snd p₁ = p₂