locPathConnectedSpace — Mathlib

English

If X has Alexandrov-discrete topology, then X is LocPathConnected.

Русский

Если топология X александрово-дискретна, то X локально путеподключено.

LaTeX

$$AlexandrovDiscrete.locPathConnectedSpace$$

Lean4

instance locPathConnectedSpace [AlexandrovDiscrete X] : LocPathConnectedSpace X :=
  by
  apply LocPathConnectedSpace.of_bases nhds_basis_nhdsKer_singleton
  simp only [forall_const, IsPathConnected, mem_nhdsKer_singleton]
  intro x
  exists x, specializes_rfl
  intro y hy
  symm
  apply hy.joinedIn <;> rewrite [mem_nhdsKer_singleton] <;> [assumption; rfl]

Похожие утверждения