English
For any α small, equality in Shrink(α) is determined by the inverse through the canonical equivalence. Namely, if (equivShrink(α))^{-1} x = (equivShrink(α))^{-1} y, then x = y.
Русский
Для любого α малого первая экстенсиональность Shrink: если (equivShrink(α))^{-1} x = (equivShrink(α))^{-1} y, то x = y.
LaTeX
$$$\\forall x,y \in Shrink(\alpha), (\\mathrm{equivShrink}(\\alpha))^{-1}(x) = (\\mathrm{equivShrink}(\\alpha))^{-1}(y) \\Rightarrow x = y.$$$
Lean4
@[ext]
theorem ext {α : Type v} [Small.{w} α] {x y : Shrink α} (w : (equivShrink _).symm x = (equivShrink _).symm y) : x = y :=
by simpa using w
