English
Let α be a type. The map sending each finite subset of α to its powerset (the set of all finite subsets) is a cofinal map from the directed set of finite subsets to itself, i.e., tends to the top when the input tends to the top.
Русский
Пусть α — множество. отображение каждого конечного подмножества α в множество его степеней (множество всех конечных подмножеств) является когерентным отображением по отношению к включению и достигает верха, когда вход стремится к верху.
LaTeX
$$$\\text{Tendsto}\\big(\\mathrm{powerset}_{\\alpha}\\big)\\;\\mathrm{atTop} \\;\\mathrm{atTop}$$$
Lean4
theorem tendsto_finset_powerset_atTop_atTop : Tendsto (Finset.powerset (α := α)) atTop atTop := by
classical
refine tendsto_atTop_atTop.mpr fun t ↦ ⟨t.sup id, fun _ hu _ hv ↦ ?_⟩
exact Finset.mem_powerset.mpr <| (Finset.le_sup_of_le hv fun _ h ↦ h).trans hu
