English
Let G act minimally on α with continuous constant smul. If K is compact and U is open nonempty, then there exists a finite subset I of G such that K is contained in the union of g·U over g in I.
Русский
Пусть G действует минимально на α и smul непрерывно. Пусть K компактно, U открыто и не пусто. Тогда существует конечное множество I ⊆ G такое, что K ⊆ ⋃_{g∈I} g·U.
LaTeX
$$$$\exists I : \mathrm{Finset}~G,\ K \subseteq \bigcup_{g\in I} g\cdot U.$$$$
Lean4
@[to_additive]
theorem exists_finite_cover_smul [IsMinimal G α] [ContinuousConstSMul G α] {K U : Set α} (hK : IsCompact K)
(hUo : IsOpen U) (hne : U.Nonempty) : ∃ I : Finset G, K ⊆ ⋃ g ∈ I, g • U :=
(hK.elim_finite_subcover (fun g ↦ g • U) fun _ ↦ hUo.smul _) <|
calc
K ⊆ univ := subset_univ K
_ = ⋃ g : G, g • U := (hUo.iUnion_smul G hne).symm
