locallyConnectedSpace — Mathlib

English

If α is locally connected and U is open, then U with the subspace topology is locally connected.

Русский

Если пространство α локально связано, и U открыто, то подпространство U с собственной топологией локально связано.

LaTeX

$$$[LocallyConnectedSpace\;\alpha] \Rightarrow [IsOpen U] \Rightarrow LocallyConnectedSpace U$$$

Lean4

theorem locallyConnectedSpace [LocallyConnectedSpace α] {U : Set α} (hU : IsOpen U) : LocallyConnectedSpace U :=
  hU.isOpenEmbedding_subtypeVal.locallyConnectedSpace

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