open_inter — Mathlib

English

The intersection of a preperfect set with an open set is preperfect.

Русский

Пересечение предперфектного множества с открытым множеством — предперфектно.

LaTeX

$$$\text{Preperfect}(U) \land \text{IsOpen}(U) \Rightarrow \text{Preperfect}(U \cap C).$$$

Lean4

/-- The intersection of a preperfect set and an open set is preperfect. -/
theorem open_inter {U : Set α} (hC : Preperfect C) (hU : IsOpen U) : Preperfect (U ∩ C) :=
  by
  rintro x ⟨xU, xC⟩
  apply (hC _ xC).nhds_inter
  exact hU.mem_nhds xU

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