Ioi_mem_atTop — Mathlib

English

For any x in α with Preorder and NoTopOrder, the open interval Ioi(x) lies in atTop.

Русский

Для любого x в α, если задано NoTopOrder, то открытый интервал Ioi(x) принадлежит atTop.

LaTeX

$$$\\mathrm{Ioi}(x) \\in \\mathrm{atTop}.$$$

Lean4

theorem Ioi_mem_atTop [Preorder α] [NoTopOrder α] (x : α) : Ioi x ∈ (atTop : Filter α) :=
  let ⟨z, hz⟩ := exists_not_le x
  mem_of_superset (inter_mem (mem_atTop x) (mem_atTop z)) fun _ ⟨hxy, hzy⟩ =>
    lt_of_le_not_ge hxy fun hyx => hz (hzy.trans hyx)

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