infty_mem_opensOfCompl — Mathlib

English

For any closed set s and compact s, the infinity point ∞ belongs to the open set opensOfCompl s h1 h2.

Русский

Для любого замкнутого компактного множества s точка ∞ принадлежит открытому множеству opensOfCompl s h1 h2.

LaTeX

$$$∞ \\in OpensOfCompl(s,h_1,h_2).$$$

Lean4

theorem infty_mem_opensOfCompl {s : Set X} (h₁ : IsClosed s) (h₂ : IsCompact s) : ∞ ∈ opensOfCompl s h₁ h₂ :=
  mem_compl infty_notMem_image_coe

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