closure_nhds_inter — Mathlib

English

If C is perfect and x ∈ C, and U is an open neighborhood of x, then closure(U ∩ C) is perfect and nonempty.

Русский

Если C совершенное и x ∈ C, и U — открытое окрестность x, то closure(U ∩ C) совершенно и непусто.

LaTeX

$$$\text{Perfect}(\overline{U \cap C}) \land (\overline{U \cap C}).\text{Nonempty}.$$$

Lean4

theorem closure_nhds_inter {U : Set α} (hC : Perfect C) (x : α) (xC : x ∈ C) (xU : x ∈ U) (Uop : IsOpen U) :
    Perfect (closure (U ∩ C)) ∧ (closure (U ∩ C)).Nonempty :=
  by
  constructor
  · apply Preperfect.perfect_closure
    exact hC.acc.open_inter Uop
  apply Nonempty.closure
  exact ⟨x, ⟨xU, xC⟩⟩

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