Iio_mem_atBot

Mathlib.Order.Filter.AtTopBot.Defs

URI: https://scilib.ai/kg/mathlib#Filter.Iio_mem_atBot

← MathLib Explorer

English

Iio x lies in atBot whenever NoBotOrder holds.

Русский

Iio x принадлежит atBot при отсутствии нижней границы.

LaTeX

$$$Iio(x) \\in \\mathrm{atBot}.$$$

Lean4

theorem Iio_mem_atBot [Preorder α] [NoBotOrder α] (x : α) : Iio x ∈ (atBot : Filter α) :=
  let ⟨z, hz⟩ := exists_not_ge x
  mem_of_superset (inter_mem (mem_atBot x) (mem_atBot z)) fun _ ⟨hyx, hyz⟩ =>
    lt_of_le_not_ge hyx fun hxy => hz (hxy.trans hyz)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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