isOpen_of_mem_nhds — Mathlib

English

For any x in G, x ∈ H.comap f hf iff f x ∈ H (additive variant analogous).

Русский

Для любого x в G верно: x ∈ H.comap f hf ⇔ f(x) ∈ H (аддитивный аналог).

LaTeX

$$$$ x \\in H^{\\mathrm{comap} f hf} \\iff f(x) \\in H. $$$$

Lean4

@[to_additive]
theorem isOpen_of_mem_nhds [ContinuousMul G] (H : Subgroup G) {g : G} (hg : (H : Set G) ∈ 𝓝 g) : IsOpen (H : Set G) :=
  by
  refine isOpen_iff_mem_nhds.2 fun x hx ↦ ?_
  have hg' : g ∈ H := SetLike.mem_coe.1 (mem_of_mem_nhds hg)
  have : Filter.Tendsto (fun y ↦ y * (x⁻¹ * g)) (𝓝 x) (𝓝 g) :=
    (continuous_id.mul continuous_const).tendsto' _ _ (mul_inv_cancel_left _ _)
  simpa only [SetLike.mem_coe, Filter.mem_map', H.mul_mem_cancel_right (H.mul_mem (H.inv_mem hx) hg')] using this hg

Похожие утверждения