English
In a preconnected space, for a relation P, if x and y are connected by a chain of P-relations locally, then P(x,y) holds.
Русский
В предсвязанном пространстве для отношения P, если x и y связаны цепочкой P-отношений локально, то P(x,y) выполняется.
LaTeX
$$$[IsPreconnected]\; (P) \; (\text{locally } P) \to \forall x,y, P x y$$$
Lean4
/-- In a preconnected set, 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₂ {s : Set α} (hs : IsPreconnected s) (P : α → α → Prop) (h : ∀ x ∈ s, ∀ᶠ y in 𝓝[s] x, P x y)
(h' : ∀ x y z, x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z) (h'' : ∀ x y, x ∈ s → y ∈ s → P x y → P y x) {x y : α}
(hx : x ∈ s) (hy : y ∈ s) : P x y :=
by
apply hs.induction₂' P (fun z hz ↦ ?_) h' hx hy
filter_upwards [h z hz, self_mem_nhdsWithin] with a ha h'a
exact ⟨ha, h'' z a hz h'a ha⟩
