inter_left — Mathlib

English

If t is compact and s is closed, then their intersection s ∩ t is compact.

Русский

Если t компактно, а s замкнуто, то их пересечение s ∩ t компактно.

LaTeX

$$$IsCompact(t) \rightarrow IsClosed(s) \rightarrow IsCompact(s \cap t)$$$

Lean4

/-- The intersection of a closed set and a compact set is a compact set. -/
theorem inter_left (ht : IsCompact t) (hs : IsClosed s) : IsCompact (s ∩ t) :=
  inter_comm t s ▸ ht.inter_right hs

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