isOpen_inter — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem isOpen_inter (hs : IsRetrocompact s) (ht : IsRetrocompact t) (hsopen : IsOpen s) :
    IsRetrocompact (s ∩ t : Set X) :=
  inter_comm .. ▸ ht.inter_isOpen hs hsopen

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