mem_nhds_one — Mathlib

English

If U ∈ B then U is a neighborhood of the identity; i.e., U ∈ nhds(1).

Русский

Если U ∈ B, то U является окрестностью единицы; то есть U ∈ nhds(1).

LaTeX

$$$\forall U\,(U\in B)\Rightarrow U\in \nhds(1)$.$$

Lean4

@[to_additive]
theorem mem_nhds_one (B : GroupFilterBasis G) {U : Set G} (hU : U ∈ B) : U ∈ @nhds G B.topology 1 :=
  by
  rw [B.nhds_one_hasBasis.mem_iff]
  exact
    ⟨U, hU, rfl.subset⟩
      -- See note [lower instance priority]

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