isOpenEmbedding_inclusion_principal

English

The neighborhood filter of the inclusion equals the map of the neighborhood filter (nhds_eq_map_inclusion).

Русский

Фильтр окрестностей включения равен отображению фильтра окрестностей (nhds_eq_map_inclusion).

LaTeX

$$$\\mathcal{nhds}\\bigl(\\text{inclusion } R A hS\\, x\\bigr) = \\mathrm{map}\\bigl(\\text{inclusion } R A hS\\bigr) \\bigl( \\mathcal{nhds}(x) \\bigr)$$$

Lean4

theorem isOpenEmbedding_inclusion_principal {S : Set ι} (hS : cofinite ≤ 𝓟 S) : IsOpenEmbedding (inclusion R A hS)
    where
  toIsEmbedding := isEmbedding_inclusion_principal hS
  isOpen_range := by
    rw [range_inclusion]
    exact isOpen_forall_imp_mem hAopen

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