IsLocallyClosed — Mathlib

English

A set is locally closed if it is the intersection of an open set with a closed set.

Русский

Множество локально закрыто, если оно является пересечением открытого множества и замкнутого.

LaTeX

$$$\IsLocallyClosed(s) := \exists U,Z, \IsOpen(U) \land \IsClosed(Z) \land s = U \cap Z$$$

Lean4

/-- A set is locally closed if it is the intersection of some open set and some closed set.
Also see `isLocallyClosed_tfae` and other lemmas in `Mathlib/Topology/LocallyClosed.lean`.
-/
def IsLocallyClosed (s : Set X) : Prop :=
  ∃ (U Z : Set X), IsOpen U ∧ IsClosed Z ∧ s = U ∩ Z

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