inter_isOpen — Mathlib

English

If s is retrocompact, t is retrocompact, and t is open, then s ∩ t is retrocompact.

Русский

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

LaTeX

$$IsRetrocompact(s) → IsRetrocompact(t) → IsOpen(t) → IsRetrocompact(s ∩ t)$$

Lean4

theorem inter_isOpen (hs : IsRetrocompact s) (ht : IsRetrocompact t) (htopen : IsOpen t) :
    IsRetrocompact (s ∩ t : Set X) := fun _U hUcomp hUopen ↦
  inter_assoc .. ▸ hs (ht hUcomp hUopen) (htopen.inter hUopen)

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