English
Given a compact K and an open U with K ⊆ U, there exists V near 1 such that K · V ⊆ U.
Русский
Пусть K компактно, U открыто и K ⊆ U; существует окрестность V(1) такая, что K · V ⊆ U.
LaTeX
$$$\\exists V \\in \\mathcal{N}(1),\\; K \\cdot V \\subseteq U.$$$
Lean4
/-- Given a compact set `K` inside an open set `U`, there is an open neighborhood `V` of `1`
such that `K * V ⊆ U`. -/
@[to_additive /-- Given a compact set `K` inside an open set `U`, there is an open neighborhood `V` of
`0` such that `K + V ⊆ U`. -/
]
theorem compact_open_separated_mul_right {K U : Set G} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) :
∃ V ∈ 𝓝 (1 : G), 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 * 1) by simpa using hU.mem_nhds (hKU hx))
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⟩
