atTop_eq_pure_of_isTop — Mathlib

English

If x is a top element in a partial order, then the atTop filter equals the principal filter at x.

Русский

Если x является верхним элементом частичного порядка, то фильтр atTop равен чистому фильтру по x.

LaTeX

$$$\text{IsTop}(x) \Rightarrow \text{atTop} = \text{pure}(x)$$

Lean4

theorem atTop_eq_pure_of_isTop [PartialOrder α] {x : α} (hx : IsTop x) : (atTop : Filter α) = pure x :=
  { top := x, le_top := hx : OrderTop α }.atTop_eq

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