mem_closure_iff_nhds_one — Mathlib

English

An element x belongs to the closure of a set s if and only if for every neighborhood U of 1, there exists y ∈ s with y/x ∈ U.

Русский

Элемент x принадлежит замыканию множества s тогда и только тогда, когда для любой окрестности U единицы существует y ∈ s such that y/x ∈ U.

LaTeX

$$$x \in \overline{s} \quad\Longleftrightarrow\quad \forall U \in 𝓝(1), \exists y \in s, \ y/x \in U$$$

Lean4

@[to_additive]
theorem mem_closure_iff_nhds_one {x : G} {s : Set G} : x ∈ closure s ↔ ∀ U ∈ (𝓝 1 : Filter G), ∃ y ∈ s, y / x ∈ U :=
  by
  rw [mem_closure_iff_nhds_basis ((𝓝 1 : Filter G).basis_sets.nhds_of_one x)]
  simp_rw [Set.mem_setOf, id]

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