English
In a preconnected space, for a transitive relation P, if for every x in the space, P x y holds eventually with y near x in both directions, then P x y holds for all x,y.
Русский
В предсвязном пространстве для транзитивного отношения P, если для каждого x существенна локальная ассоциация P x y и P y x для близких y, тогда P x y выполняется для всех x,y.
LaTeX
$$$[PreconnectedSpace\;\alpha] (P:\alpha\to\alpha\to Prop)\; (\forall x, \forall y, \text{ Eventually } P x y) \to (\forall x y, P x y)$$$
Lean4
/-- In a preconnected space, 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₂' [PreconnectedSpace α] (P : α → α → Prop) (h : ∀ x, ∀ᶠ y in 𝓝 x, P x y ∧ P y x) (h' : Transitive P)
(x y : α) : P x y := by
let u := {z | P x z}
have A : IsClosed u := by
apply isClosed_iff_nhds.2 (fun z hz ↦ ?_)
rcases hz _ (h z) with ⟨t, ht, h't⟩
exact h' h't ht.2
have B : IsOpen u := by
apply isOpen_iff_mem_nhds.2 (fun z hz ↦ ?_)
filter_upwards [h z] with t ht
exact h' hz ht.1
have C : u.Nonempty := ⟨x, (mem_of_mem_nhds (h x)).1⟩
have D : u = Set.univ := IsClopen.eq_univ ⟨A, B⟩ C
change y ∈ u
simp [D]
