inter_of_isOpen_isCompact — Mathlib

English

If s is locally constructible, t is open, and t is compact, then s ∩ t is constructible.

Русский

Если s локально конструируемо, t открыто и компактно, тогда s ∩ t конструируемо.

LaTeX

$$$\\operatorname{IsConstructible}(s \\cap t) \\;\\text{ when } \\operatorname{IsLocallyConstructible}(s),\\; \\operatorname{IsOpen}(t),\\; \\operatorname{IsCompact}(t).$$$

Lean4

theorem inter_of_isOpen_isCompact [PrespectralSpace X] [QuasiSeparatedSpace X] (hs : IsLocallyConstructible s)
    (ht : IsOpen t) (ht' : IsCompact t) : IsConstructible (s ∩ t) :=
  (hs.inter (ht'.isConstructible ht).isLocallyConstructible).isConstructible_of_subset_of_isCompact
    Set.inter_subset_right ht'

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