mathlib documentation

core.​init.​data.​sigma.​basic

core.​init.​data.​sigma.​basic

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

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

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