instSDiff — Mathlib

English

In a Hausdorff space, the family of compact-open subsets is closed under set difference: if s and t are compact-open, then s \ t is also compact-open.

Русский

В пространствах Хаусдорфа множество компактно-открытых подмножеств замкнуто относительно разности: если s и t — компактно-открытые, то s \ t тоже компактно-открыто.

LaTeX

$$$\forall \alpha\, [\text{T}_2\text{Space }\alpha],\ s,t \in \mathrm{CompactOpens}(\alpha) \Rightarrow s\setminus t \in \mathrm{CompactOpens}(\alpha).$$$

Lean4

instance instSDiff : SDiff (CompactOpens α) where
  sdiff s t := ⟨⟨s \ t, s.isCompact.diff t.isOpen⟩, s.isOpen.sdiff t.isCompact.isClosed⟩

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