tendsto_finset_Ici_atBot_atTop — Mathlib

English

Let α be a preorder with a top element. The map a ↦ Finset.Ici(a) (the set of elements ≥ a) tends to the top as a tends to the bottom, i.e., starting from the bottom, the upward cones expand to cover the whole type.

Русский

Пусть α — предпорядок с вершиной. Отображение a ↦ Finset.Ici(a) (множество элементов ≥ a) стремится к верху, когда a стремится к низу; от нижней границы конусы вверх заполняют множество.

LaTeX

$$$\\operatorname{Tendsto}(\\mathrm{Ici}_{\\alpha},\\mathrm{atBot},\\mathrm{atTop})$$$

Lean4

theorem tendsto_finset_Ici_atBot_atTop [Preorder α] [LocallyFiniteOrderTop α] :
    Tendsto (Finset.Ici (α := α)) atBot atTop :=
  tendsto_finset_Iic_atTop_atTop (α := αᵒᵈ)

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