atBot_neBot_iff — Mathlib

English

Dual statement: the atBot filter is NeBot iff α is nonempty and directed with respect to ≥.

Русский

Двунаправленная версия: atBot NeBot тогда и только тогда, когда α непусто и направлено по ≥.

LaTeX

$$$ (\\operatorname{atBot}.\\mathrm{NeBot}) \\iff (\\text{Nonempty } α \\land \\operatorname{IsDirected} α (\\ge)) $$$

Lean4

theorem atBot_neBot_iff {α : Type*} [Preorder α] : (atBot : Filter α).NeBot ↔ Nonempty α ∧ IsDirected α (· ≥ ·) :=
  atTop_neBot_iff (α := αᵒᵈ)

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