max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: rename PSigma.exists (#4878)

Browse source
This commit is contained in:
Kim Morrison 2024-07-31 13:26:17 +10:00 • committed by GitHub
parent 81719f94c9
commit a4015ca36c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/Core.lean
View file

@ -1204,12 +1204,12 @@ def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂
/-! # Dependent products -/
theorem PSigma.exists {α : Sort u} {p : α → Prop} : (PSigma (fun x => p x)) → Exists (fun x => p x)
theorem Exists.of_psigma_prop {α : Sort u} {p : α → Prop} : (PSigma (fun x => p x)) → Exists (fun x => p x)
| ⟨x, hx⟩ => ⟨x, hx⟩
@[deprecated PSigma.exists (since := "2024-07-27")]
@[deprecated Exists.of_psigma_prop (since := "2024-07-27")]
theorem ex_of_PSigma {α : Type u} {p : α → Prop} : (PSigma (fun x => p x)) → Exists (fun x => p x) :=
PSigma.exists
Exists.of_psigma_prop
protected theorem PSigma.eta {α : Sort u} {β : α → Sort v} {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂}
(h₁ : a₁ = a₂) (h₂ : Eq.ndrec b₁ h₁ = b₂) : PSigma.mk a₁ b₁ = PSigma.mk a₂ b₂ := by