English
Let p be a predicate on X and consider two points x and y in the subspace {u in X | p(u)}. Then x and y are inseparable in this subspace if and only if their underlying points in X are inseparable.
Русский
Пусть p — предикат на X и возьмём две точки x и y в подпространстве {u ∈ X | p(u)}. Тогда x и y неразделимы в этом подпространстве тогда и только тогда, когда их проекции в X неразделимы.
LaTeX
$$$\\text{Let } x=(a,\\,\\alpha)\\text{ and } y=(b,\\,\\beta)\\text{ with } p(a), p(b)\\text{. Then }(a,\\alpha) \\sim_i (b,\\beta) \\iff a \\sim_i b.$$$
Lean4
theorem subtype_inseparable_iff {p : X → Prop} (x y : Subtype p) : (x ~ᵢ y) ↔ ((x : X) ~ᵢ y) :=
IsInducing.subtypeVal.inseparable_iff.symm
