English
An extensionality principle for PSigma over an indexed subtype: two PSigma elements are equal if their first components are equal and their second components are equal after transporting along that equality.
Русский
Принцип экстенсивности для PSigma над индексированным подтипом: две элементы равны, если их первые координаты равны и вторые после переноса по этому равенству равны.
LaTeX
$$$\\forall {x_0 x_1 : \\Sigma' a, Subtype (p a)},\\ x_0.\\mathrm{fst} = x_1.\\mathrm{fst} \\rightarrow (x_0.\\mathrm snd) = (x_1.\\mathrm snd) \\Rightarrow x_0 = x_1$$$
Lean4
/-- A specialized ext lemma for equality of `PSigma` types over an indexed subtype. -/
@[ext]
theorem subtype_ext {β : Sort*} {p : α → β → Prop} :
∀ {x₀ x₁ : Σ' a, Subtype (p a)}, x₀.fst = x₁.fst → (x₀.snd : β) = x₁.snd → x₀ = x₁
| ⟨_, _, _⟩, ⟨_, _, _⟩, rfl, rfl => rfl
