English
Two points x,y in OnePoint X are inseparable iff either both are ∞, or they come from x',y' ∈ X with x=x', y=y' and x',y' inseparable in X.
Русский
Два элемента x,y ∈ OnePoint X неразделимы тогда и только тогда, когда либо оба равны ∞, либо существует x', y' ∈ X такие, что x = x' и y = y', и x', y' неразделимы в X.
LaTeX
$$$\\operatorname{Inseparable}(x,y) \\iff \\bigl(x=\\infty \\land y=\\infty\\bigr) \\lor \\exists x'\\in X, \\exists y'\\in X, x=x' \\land y=y' \\land \\operatorname{Inseparable}(x',y').$$$
Lean4
theorem inseparable_iff {x y : OnePoint X} :
Inseparable x y ↔ x = ∞ ∧ y = ∞ ∨ ∃ x' : X, x = x' ∧ ∃ y' : X, y = y' ∧ Inseparable x' y' := by
induction x using OnePoint.rec <;> induction y using OnePoint.rec <;>
simp [not_inseparable_infty_coe, not_inseparable_coe_infty, coe_eq_coe, Inseparable.refl]
