English
Two topologies on a group G are equal if their neighborhoods at 1 agree; equivalence via nhds at 1.
Русский
Две топологии на группе равны, если совпадают окрестности единицы; эквивалентность через nhds(1).
LaTeX
$$$IsTopologicalGroup.ext \;\text{lemma: }\;\text{nhds}_1$-based equality$$
Lean4
@[to_additive]
theorem isOpenMap_iff_nhds_one {H : Type*} [Monoid H] [TopologicalSpace H] [ContinuousConstSMul H H] {F : Type*}
[FunLike F G H] [MonoidHomClass F G H] {f : F} : IsOpenMap f ↔ 𝓝 1 ≤ .map f (𝓝 1) :=
by
refine ⟨fun H ↦ map_one f ▸ H.nhds_le 1, fun h ↦ IsOpenMap.of_nhds_le fun x ↦ ?_⟩
have : Filter.map (f x * ·) (𝓝 1) = 𝓝 (f x) := by
simpa [-Homeomorph.map_nhds_eq, Units.smul_def] using
(Homeomorph.smul ((toUnits x).map (MonoidHomClass.toMonoidHom f))).map_nhds_eq (1 : H)
rw [← map_mul_left_nhds_one x, Filter.map_map, Function.comp_def, ← this]
refine (Filter.map_mono h).trans ?_
simp [Function.comp_def]
