nhds_bot'

Mathlib.Topology.Instances.EReal.Lemmas

URI: https://scilib.ai/kg/mathlib#EReal.nhds_bot'

English

The primed form of nhds_bot expresses the same bottom basis via Iio a in Real via toEReal.

Русский

Преобразование nhds_bot в форму через toEReal даёт эквивалентный базис снизу.

LaTeX

$$$\\mathcal{N}(\\bot) = \\bigwedge_{a\\in\\mathbb{R}} \\mathcal{P}(Iio(a)^{\\mathrm{toEReal}})$$$

Lean4

theorem nhds_bot' : 𝓝 (⊥ : EReal) = ⨅ a : ℝ, 𝓟 (Iio ↑a) :=
  nhds_bot_basis.eq_iInf

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

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

Разделы

Аффилиация

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