English
Let α be a preorder with a bottom element and locally finite order. The map a ↦ Finset.Iic(a) (the set of elements ≤ a) tends to the top as a tends to the top. In other words, the family of all initial segments grows to cover the whole set.
Русский
Пусть α — предпорядок с нижним пределом и локально конечным порядком. Отображение a ↦ Finset.Iic(a) (множество элементов ≤ a) стремится кверху, когда a стремится к вершине. Иными словами, семейство начальных отрезков заполняет всю множествa.
LaTeX
$$$\\operatorname{Tendsto}(\\mathrm{Iic}_{\\alpha},\\mathrm{atTop},\\mathrm{atTop})$$$
Lean4
theorem tendsto_finset_Iic_atTop_atTop [Preorder α] [LocallyFiniteOrderBot α] :
Tendsto (Finset.Iic (α := α)) atTop atTop :=
by
rcases isEmpty_or_nonempty α with _ | _
· exact tendsto_of_isEmpty
by_cases h : IsDirected α (· ≤ ·)
· refine tendsto_atTop_atTop.mpr fun s ↦ ?_
obtain ⟨a, ha⟩ := Finset.exists_le s
exact ⟨a, fun b hb c hc ↦ by simpa using (ha c hc).trans hb⟩
· obtain h := Filter.atTop_neBot_iff.not.mpr (fun h' ↦ h h'.2)
simp [not_ne_iff.mp <| Filter.neBot_iff.not.mp h]
