alexandrovDiscrete — Mathlib

English

If α is Alexandrov-discrete and f: β → α is an inducing map, then β is Alexandrov-discrete.

Русский

Если α является Александрово-дискретным пространством и f: β → α индуктивно отображает β в α, то β также Александрово-дискретно.

LaTeX

$$AlexandrovDiscrete β$$

Lean4

theorem alexandrovDiscrete [AlexandrovDiscrete α] {f : β → α} (h : IsInducing f) : AlexandrovDiscrete β where
  isOpen_sInter S
    hS := by
    simp_rw [h.isOpen_iff] at hS ⊢
    choose U hU htU using hS
    refine ⟨_, isOpen_iInter₂ hU, ?_⟩
    simp_rw [preimage_iInter, htU, sInter_eq_biInter]

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