instOrderTop — Mathlib

English

If β is a partially ordered set with a top element, then the germ construction over β with respect to a filter l on α carries a top element. This top element is the germ of the constant function at the top of β.

Русский

Пусть β имеет частичную порядочность и верхнюю границу top. Тогда Germ l β имеет верхний элемент, представляющий собой герм константной функции, принимающей значение top.

LaTeX

$$$\\text{OrderTop}(\\mathrm{Germ}_l \\beta)$$$

Lean4

instance instOrderTop [LE β] [OrderTop β] : OrderTop (Germ l β) where
  le_top f := inductionOn f fun _ => Eventually.of_forall fun _ => le_top

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