English
Given a compact set K and a neighborhood U of 0 in a topological monoid with continuous multiplication, there exists a neighborhood V of 0 such that K V ⊆ U.
Русский
Для компактного множества K и окрестности U нуля в топологическом моноиде с непрерывным умножением существует окрестность V нуля такая, что KV ⊆ U.
LaTeX
$$Exists V ∈ 𝓝 0, K * V ⊆ U$$
Lean4
theorem exists_mem_nhds_zero_mul_subset {K U : Set M} (hK : IsCompact K) (hU : U ∈ 𝓝 0) : ∃ V ∈ 𝓝 0, K * V ⊆ U :=
by
refine hK.induction_on ?_ ?_ ?_ ?_
· exact ⟨univ, by simp⟩
· rintro s t hst ⟨V, hV, hV'⟩
exact ⟨V, hV, (mul_subset_mul_right hst).trans hV'⟩
· rintro s t ⟨V, V_in, hV'⟩ ⟨W, W_in, hW'⟩
use V ∩ W, inter_mem V_in W_in
rw [union_mul]
exact
union_subset ((mul_subset_mul_left V.inter_subset_left).trans hV')
((mul_subset_mul_left V.inter_subset_right).trans hW')
· intro x hx
have := tendsto_mul (show U ∈ 𝓝 (x * 0) by simpa using hU)
rw [nhds_prod_eq, mem_map, mem_prod_iff] at this
rcases this with ⟨t, ht, s, hs, h⟩
rw [← image_subset_iff, image_mul_prod] at h
exact ⟨t, mem_nhdsWithin_of_mem_nhds ht, s, hs, h⟩
