instPathConnectedSpace — Mathlib

English

Let 𝕜 be a nontrivially normed field that is real-complex-like; then the underlying topological space of 𝕜 is path-connected.

Русский

Пусть 𝕜 — ненулево-нормированное поле, которое является реальноподобным или комплексоподобным; тогда топологическое пространство над 𝕜 является связным по пути.

LaTeX

$$$\mathbb{K}$ is path-connected.$$

Lean4

instance (priority := 100) : PathConnectedSpace 𝕜 :=
  by
  letI : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
  infer_instance

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