English
If a symmetric transitive relation P is eventually true between nearby points in a preconnected space, then P holds for all pairwise.
Русский
Если симметричное транзитивное отношение P истинно между близкими точками в предсвязанном пространстве, то P справедлива для любых пар точек.
LaTeX
$$$[IsPreconnected]\; (P) \; (\forall x, \text{ Eventually } P x y) \to (\text{Transitive } P) \to (\text{Symmetric } P) \to \forall x,y, P x y$$$
Lean4
/-- In a preconnected set, given a transitive relation `P`, if `P x y` and `P y x` are true
for `y` close enough to `x`, then `P x y` 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 ∧ P y x)
(h' : ∀ x y z, x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z) {x y : α} (hx : x ∈ s) (hy : y ∈ s) : P x y :=
by
let Q : s → s → Prop := fun a b ↦ P a b
change Q ⟨x, hx⟩ ⟨y, hy⟩
have : PreconnectedSpace s := Subtype.preconnectedSpace hs
apply PreconnectedSpace.induction₂'
· rintro ⟨x, hx⟩
have Z := h x hx
rwa [nhdsWithin_eq_map_subtype_coe] at Z
· rintro ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩ hab hbc
exact h' a b c ha hb hc hab hbc
