Commit 2025-04-01 16:01 ab0e2d8c
View on Github →chore: make sure that simp can prove that a finite set is relatively compact (#23105)
Make Set.Finite.isClosed, IsClosed.closure_eq and Set.Finite.isCompact simp lemmas so that the following works:
import Mathlib
example {X : Type*} [TopologicalSpace X] {s : Set X} (hs : s.Finite) : IsCompact (closure s) := by simp
From my PhD (MiscYD)