nhdsLE

Mathlib.Topology.Order.OrderClosed

URI: https://scilib.ai/kg/mathlib#CovBy.nhdsLE

English

If a ⋖ b (a is the immediate predecessor of b), then the left-neighborhood filter at b is the principal filter at b: 𝓝[≤] b = pure b.

Русский

Если a ⋖ b, то 𝓝[≤] b = чистая фильтр-первоночник b.

LaTeX

$$$[CovBy\ a\ b] \rightarrow 𝓝_{[\le]}(b) = \text{pure } b$$$

Lean4

protected theorem nhdsLE (H : a ⋖ b) : 𝓝[≤] b = pure b := by rw [← Iio_insert, nhdsWithin_insert, H.nhdsLT, sup_bot_eq]

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

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

Разделы

Аффилиация

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