isInducing_iff_nhds_one — Mathlib

English

Simplified variants of split neighborhood lemma: exists V around 1 with v,w in V implies v/w ∈ s.

Русский

Упрощённые варианты леммы про окрестности: существует V вокруг 1, где для любых v,w∈V выполняется v/w ∈ s.

LaTeX

$$$\exists V ∈ 𝓝(1),\; ∀ v ∈ V, ∀ w ∈ V, v/w ∈ s$$$

Lean4

@[to_additive]
theorem isInducing_iff_nhds_one {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {F : Type*}
    [FunLike F G H] [MonoidHomClass F G H] {f : F} : Topology.IsInducing f ↔ 𝓝 (1 : G) = (𝓝 (1 : H)).comap f :=
  by
  rw [Topology.isInducing_iff_nhds]
  refine ⟨(map_one f ▸ · 1), fun hf x ↦ ?_⟩
  rw [← nhds_translation_mul_inv, ← nhds_translation_mul_inv (f x), Filter.comap_comap, hf, Filter.comap_comap]
  congr 1
  ext; simp

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