nhdsWithin_isUnit_neBot

Mathlib.Analysis.Normed.Field.Basic

URI: https://scilib.ai/kg/mathlib#NormedField.nhdsWithin_isUnit_neBot

English

The nhdsWithin of 0 restricted to units is nonempty.

Русский

nhdsWithin вокруг 0 ограниченный единицами не пуст.

LaTeX

$$$ (\nhdsWithin 0 (\{x \mid IsUnit x\})).NeBot $$$

Lean4

@[instance]
theorem nhdsWithin_isUnit_neBot : NeBot (𝓝[{x : α | IsUnit x}] 0) := by
  simpa only [isUnit_iff_ne_zero] using nhdsNE_neBot (0 : α)

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

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

Разделы

Аффилиация

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