inv_mem_nhds_one — Mathlib

English

If a set S is a neighborhood of 1, then its inverse S⁻¹ is also a neighborhood of 1.

Русский

Если множество S является окрестностью единицы, то множество S⁻¹ тоже является окрестностью единицы.

LaTeX

$$$\forall S:\; S \in \mathcal{N}(1) \Rightarrow S^{-1} \in \mathcal{N}(1)$$$

Lean4

@[to_additive]
theorem inv_mem_nhds_one {S : Set G} (hS : S ∈ (𝓝 1 : Filter G)) : S⁻¹ ∈ 𝓝 (1 : G) := by rwa [← nhds_one_symm'] at hS

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