pathComponentIn — Mathlib

English

If F is open, then for every x, the path component of F containing x is open in X.

Русский

Если F открыто, то для каждого x путь-компонента F, содержащая x, открыта в X.

LaTeX

$$IsOpen F \rightarrow \forall x, IsOpen( pathComponentIn F x )$$

Lean4

protected theorem pathComponentIn (hF : IsOpen F) (x : X) : IsOpen (pathComponentIn F x) :=
  by
  rw [isOpen_iff_mem_nhds]
  intro y hy
  let ⟨s, hs⟩ := (path_connected_basis y).mem_iff.mp (hF.mem_nhds (pathComponentIn_subset hy))
  exact mem_of_superset hs.1.1 <| pathComponentIn_congr hy ▸ hs.1.2.subset_pathComponentIn (mem_of_mem_nhds hs.1.1) hs.2

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