English
Dually, for a compact K and an open U with K ⊆ U, there exists V near 1 such that V · K ⊆ U.
Русский
Аналогично: компакт K и открытое U с K ⊆ U существуют V около единицы, такие что V · K ⊆ U.
LaTeX
$$$\exists V \in \mathcal{N}(1),\; V \cdot K \subseteq U.$$$
Lean4
/-- Given a compact set `K` inside an open set `U`, there is an open neighborhood `V` of `1`
such that `V * K ⊆ U`. -/
@[to_additive /-- Given a compact set `K` inside an open set `U`, there is an open neighborhood `V` of
`0` such that `V + K ⊆ U`. -/
]
theorem compact_open_separated_mul_left {K U : Set G} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) :
∃ V ∈ 𝓝 (1 : G), V * K ⊆ U :=
by
rcases compact_open_separated_mul_right (hK.image continuous_op) (opHomeomorph.isOpenMap U hU) (image_mono hKU) with
⟨V, hV : V ∈ 𝓝 (op (1 : G)), hV' : op '' K * V ⊆ op '' U⟩
refine ⟨op ⁻¹' V, continuous_op.continuousAt hV, ?_⟩
rwa [← image_preimage_eq V op_surjective, ← image_op_mul, image_subset_iff, preimage_image_eq _ op_injective] at hV'
