nhdsSet_eq_comap — Mathlib

English

For hf : IsInducing f, and s ⊆ X, 𝓝ˢ s = comap f (𝓝ˢ (f '' s)).

Русский

Для индуциирующего f и множества s выполняется 𝓝ˢ s = comap f (𝓝ˢ (f '' s)).

LaTeX

$$$\operatorname{nhdsSet}(s) = \operatorname{comap}(f)(\operatorname{nhdsSet}(f''s)).$$$

Lean4

theorem nhdsSet_eq_comap (hf : IsInducing f) (s : Set X) : 𝓝ˢ s = comap f (𝓝ˢ (f '' s)) := by
  simp only [nhdsSet, sSup_image, comap_iSup, hf.nhds_eq_comap, iSup_image]

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