exists_nhds_split_inv — Mathlib

English

If s ∈ 𝓝(1_G), then there exists V ∈ 𝓝(1_G) such that ∀ v,w ∈ V, v/w ∈ s.

Русский

Если s является окрестностью единицы, то существует окрестность V единицы такая, что для всех v,w ∈ V выполняется v/w ∈ s.

LaTeX

$$$\exists V \in 𝓝(1_G),\; \forall v \in V, \forall w \in V,\; v / w \in s$$$

Lean4

@[to_additive exists_nhds_half_neg]
theorem exists_nhds_split_inv {s : Set G} (hs : s ∈ 𝓝 (1 : G)) : ∃ V ∈ 𝓝 (1 : G), ∀ v ∈ V, ∀ w ∈ V, v / w ∈ s :=
  by
  have : (fun p : G × G => p.1 * p.2⁻¹) ⁻¹' s ∈ 𝓝 ((1, 1) : G × G) :=
    continuousAt_fst.mul continuousAt_snd.inv (by simpa)
  simpa only [div_eq_mul_inv, nhds_prod_eq, mem_prod_self_iff, prod_subset_iff, mem_preimage] using this

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