isOpen — Mathlib

English

A set s is open iff its intersections with all compact sets K are open in K, under Hausdorff assumption.

Русский

Множество s открыто тогда и только тогда, когда s ∩ K открыто в K для всех компактных K при предположении гипотезы Хаусдорфа.

LaTeX

$$[CompactlyGeneratedSpace X] {s : Set X} (hs : ∀ ⦃K⦄, IsCompact K → IsOpen (s ∩ K)) : IsOpen s$$

Lean4

/-- In a compactly generated space `X`, a set `s` is open when `s ∩ K` is
closed for every open set `K`. -/
theorem isOpen [CompactlyGeneratedSpace X] {s : Set X} (hs : ∀ ⦃K⦄, IsCompact K → IsOpen (s ∩ K)) : IsOpen s :=
  by
  refine isOpen' fun K _ _ _ f hf ↦ ?_
  rw [← Set.preimage_inter_range]
  exact (hs (isCompact_range hf)).preimage hf

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