inv_nhdsGT_zero

Mathlib.Topology.Algebra.Order.Field

URI: https://scilib.ai/kg/mathlib#inv_nhdsGT_zero

English

The reciprocal of the neighborhood of zero from the right equals the atTop filter; i.e., (nhds[>](0))^{-1} = atTop.

Русский

Обратная окрестность нуля справа равна atTop; то есть (nhds[>](0))^{-1} = atTop.

LaTeX

$$$(\mathcal{N}_{[>0]}(0))^{-1} = \mathrm{atTop}$$$

Lean4

@[simp]
theorem inv_nhdsGT_zero : (𝓝[>] (0 : 𝕜))⁻¹ = atTop := by rw [← inv_atTop₀, inv_inv]

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

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

Разделы

Аффилиация

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