Documentation

Mathlib.Init.Data.Sigma.Basic

Lemmas about Sigma from Lean 3 core. #

theorem ex_of_psig {α : Sort u_1} {p : αProp} :
(x : α) ×' p x∃ (x : α), p x
theorem Sigma.eq {α : Type u_1} {β : αType v} {p₁ : (a : α) × β a} {p₂ : (a : α) × β a} (h₁ : p₁.fst = p₂.fst) :
Eq.recOn h₁ p₁.snd = p₂.sndp₁ = p₂
theorem PSigma.eq {α : Sort u_1} {β : αSort v} {p₁ : (a : α) ×' β a} {p₂ : (a : α) ×' β a} (h₁ : p₁.fst = p₂.fst) :
Eq.recOn h₁ p₁.snd = p₂.sndp₁ = p₂