mathlib3 documentation

core / init.data.sigma.basic

source
theorem ex_of_psig {α : Type u} {p : α → Prop} :
(Σ' (x : α), p x) → (∃ (x : α), p x)
source
@[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₂
source
@[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₂