nhdsLT

Mathlib.Topology.Order.OrderClosed

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

English

Same content as exists_ge' under a dense set, producing y ∈ s with x ≤ y.

Русский

То же самое, что и exists_ge' для плотного множества, существование y ∈ s с x ≤ y.

LaTeX

$$$(\text{Dense } s) \rightarrow (\forall x,\; \exists y \in s,\; x \le y)$$$

Lean4

protected theorem nhdsLT (h : a ⋖ b) : 𝓝[<] b = ⊥ :=
  empty_mem_iff_bot.mp <| h.Ioo_eq ▸ Ioo_mem_nhdsLT h.1

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

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

Разделы

Аффилиация

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