tendsto_finset_range — Mathlib

English

The range map for Finset tends to atTop, i.e., the sequence of finite initial segments grows unboundedly.

Русский

Переход по диапазону Finset стремится к atTop, последовательность конечных начальных отрезков неограничена.

LaTeX

$$$\operatorname{Tendsto}(\operatorname{Finset.range}, \operatorname{atTop}, \operatorname{atTop})$$$

Lean4

theorem tendsto_finset_range : Tendsto Finset.range atTop atTop :=
  Finset.range_mono.tendsto_atTop_atTop Finset.exists_nat_subset_range

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