inter — Mathlib

English

The intersection of two retrocompact sets is retrocompact (in a T2 space).

Русский

Пересечение двух ретро-компактных множеств является ретро-компактным (в пространстве T2).

LaTeX

$$$\text{IsRetrocompact}(s) \land \text{IsRetrocompact}(t) \Rightarrow \text{IsRetrocompact}(s \cap t)$$$

Lean4

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

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