singleton_mem_nhds_of_units

Mathlib.Topology.Algebra.WithZeroTopology

URI: https://scilib.ai/kg/mathlib#WithZeroTopology.singleton_mem_nhds_of_units

← MathLib Explorer

English

For a unit γ, the set {γ} is a neighborhood of γ.

Русский

Для единицы γ множество {γ} является окрестностью γ.

LaTeX

$$$\\{\\gamma\\}\\in\\mathcal{N}(\\gamma)$$$

Lean4

/-- If `γ` is an invertible element of a linearly ordered group with zero element adjoined, then
`{γ}` is a neighbourhood of `γ`. -/
theorem singleton_mem_nhds_of_units (γ : Γ₀ˣ) : ({↑γ} : Set Γ₀) ∈ 𝓝 (γ : Γ₀) := by simp

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru