English
If t is closed and s is compact, then the product s•t is closed.
Русский
Если t замкнутое, а s компактно, то произведение s·t замкнуто.
LaTeX
$$$\\text{If } (t\\text{ closed}) \\land (s\\text{ compact}):\\ IsClosed(s\\cdot t).$$$
Lean4
@[to_additive]
theorem smul_left_of_isCompact (ht : IsClosed t) (hs : IsCompact s) : IsClosed (s • t) :=
by
have : ∀ x ∈ s • t, ∃ g ∈ s, g⁻¹ • x ∈ t :=
by
rintro x ⟨g, hgs, y, hyt, rfl⟩
refine ⟨g, hgs, ?_⟩
rwa [inv_smul_smul]
choose! f hf using this
refine isClosed_of_closure_subset (fun x hx ↦ ?_)
rcases mem_closure_iff_ultrafilter.mp hx with ⟨u, hust, hux⟩
have : Ultrafilter.map f u ≤ 𝓟 s :=
calc
Ultrafilter.map f u ≤ map f (𝓟 (s • t)) := map_mono (le_principal_iff.mpr hust)
_ = 𝓟 (f '' (s • t)) := map_principal
_ ≤ 𝓟 s := principal_mono.mpr (image_subset_iff.mpr (fun x hx ↦ (hf x hx).1))
rcases hs.ultrafilter_le_nhds (Ultrafilter.map f u) this with ⟨g, hg, hug⟩
suffices g⁻¹ • x ∈ t from ⟨g, hg, g⁻¹ • x, this, smul_inv_smul _ _⟩
exact ht.mem_of_tendsto ((Tendsto.inv hug).smul hux) (Eventually.mono hust (fun y hy ↦ (hf y hy).2))
