nhds_mul_nhds_one — Mathlib

English

In a topological monoid with continuous multiplication, for any a, nhds a multiplied by nhds 1 equals nhds a.

Русский

В топологической моноиде с непрерывным умножением для любого a справедливо nhds a · nhds 1 = nhds a.

LaTeX

$$$\nhds a \cdot \nhds 1 = \nhds a$$$

Lean4

@[to_additive (attr := simp)]
theorem nhds_mul_nhds_one {M} [MulOneClass M] [TopologicalSpace M] [ContinuousMul M] (a : M) : 𝓝 a * 𝓝 1 = 𝓝 a :=
  ((le_nhds_mul _ _).trans_eq <| congr_arg _ (mul_one a)).antisymm <| le_mul_of_one_le_right' <| pure_le_nhds 1

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