nhdsSet_Iio

Mathlib.Topology.Order.NhdsSet

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

English

In the same setting, the neighborhood filter of the open ray (-∞, a) equals the principal filter on (-∞, a).

Русский

В той же постановке фильтр окрестностей луча (-∞, a) равен принудительному (principal) на (-∞, a).

LaTeX

$$$𝓝^{s}(Iio(a)) = 𝓟(Iio(a))$$$

Lean4

@[simp]
theorem nhdsSet_Iio : 𝓝ˢ (Iio a) = 𝓟 (Iio a) :=
  isOpen_Iio.nhdsSet_eq

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

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

Разделы

Аффилиация

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