English
The specialized form of ker_nhds equals the specialized set; simplified.
Русский
Упрощенная форма ядра nhds равна множеству специализаций.
LaTeX
$$$ (\mathcal{N}(x)).ker = \{ y \mid y \;⤳\; x \}$$$
Lean4
/-- A collection of equivalent definitions of `x ⤳ y`. The public API is given by `iff` lemmas
below. -/
theorem specializes_TFAE (x y : X) :
List.TFAE
[x ⤳ y, pure x ≤ 𝓝 y, ∀ s : Set X, IsOpen s → y ∈ s → x ∈ s, ∀ s : Set X, IsClosed s → x ∈ s → y ∈ s,
y ∈ closure ({ x } : Set X), closure ({ y } : Set X) ⊆ closure { x }, ClusterPt y (pure x)] :=
by
tfae_have 1 → 2 := (pure_le_nhds _).trans
tfae_have 2 → 3 := fun h s hso hy => h (hso.mem_nhds hy)
tfae_have 3 → 4 := fun h s hsc hx => of_not_not fun hy => h sᶜ hsc.isOpen_compl hy hx
tfae_have 4 → 5 := fun h => h _ isClosed_closure (subset_closure <| mem_singleton _)
tfae_have 6 ↔ 5 := isClosed_closure.closure_subset_iff.trans singleton_subset_iff
tfae_have 5 ↔ 7 := by rw [mem_closure_iff_clusterPt, principal_singleton]
tfae_have 5 → 1 := by
refine fun h => (nhds_basis_opens _).ge_iff.2 ?_
rintro s ⟨hy, ho⟩
rcases mem_closure_iff.1 h s ho hy with ⟨z, hxs, rfl : z = x⟩
exact ho.mem_nhds hxs
tfae_finish
