English
A set s has a compact superset if and only if closure(s) is compact.
Русский
Существует компактное надмножество K, содержащее s, тогда и только тогда closure(s) компактно.
LaTeX
$$(∃ K, IsCompact K ∧ s ⊆ K) ⇔ IsCompact(closure(s))$$
Lean4
protected theorem inf {X : Type*} {t₁ t₂ : TopologicalSpace X} (h₁ : @R1Space X t₁) (h₂ : @R1Space X t₂) :
@R1Space X (t₁ ⊓ t₂) := by
rw [inf_eq_iInf]
apply R1Space.iInf
simp [*]