English
In a preconnected space, for a relation P, if for every x with membership in s, eventually P x y, and P is transitive and symmetric, then P x y for all x,y in s.
Русский
В предсвязанном пространстве для отношения P, если для каждого x из s верно P x y и P симметрично и транзитивно, то P x y для любых x,y из s.
LaTeX
$$$[IsPreconnected\;\alpha] (P:\alpha\to\alpha\to Prop)\; (\forall x, \forall y \in s, \text{Eventually } P x y) (\text{Transitive } P) (\text{Symmetric } P) \to \forall x,y \in s, P x y$$$
Lean4
/-- In a preconnected space, if a symmetric transitive relation `P x y` is true for `y` close
enough to `x`, then it holds for all `x, y`. This is a version of the fact that, if an equivalence
relation has open classes, then it has a single equivalence class. -/
theorem induction₂ [PreconnectedSpace α] (P : α → α → Prop) (h : ∀ x, ∀ᶠ y in 𝓝 x, P x y) (h' : Transitive P)
(h'' : Symmetric P) (x y : α) : P x y :=
by
refine PreconnectedSpace.induction₂' P (fun z ↦ ?_) h' x y
filter_upwards [h z] with a ha
exact ⟨ha, h'' ha⟩
