atTop_neBot_iff — Mathlib

English

The NeBot status of atTop is equivalent to the existence of a nonempty α with IsDirected α (≤).

Русский

Состояние NeBot для atTop эквивалентно существованию непустого α с направленностью по ≤.

LaTeX

$$$ (\\operatorname{atTop}.\\mathrm{NeBot}) \\iff (\\text{Nonempty } \\alpha \\land \\operatorname{IsDirected} \\alpha (\\le)) $$$

Lean4

theorem atTop_neBot_iff {α : Type*} [Preorder α] : (atTop : Filter α).NeBot ↔ Nonempty α ∧ IsDirected α (· ≤ ·) :=
  by
  refine ⟨fun h ↦ ⟨nonempty_of_neBot atTop, ⟨fun x y ↦ ?_⟩⟩, fun ⟨h₁, h₂⟩ ↦ atTop_neBot⟩
  exact ((eventually_ge_atTop x).and (eventually_ge_atTop y)).exists

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