`BookProof.CoreBounds.tendsto_trunc_inc` [DecidableEq ι] (c : ι → ℝ) (x : maxDom c) : Tendsto (fun S : Finset ι => ((trunc c x S : lpFiniteModes ι) : L2I ι)) atTop (𝓝 ((x : L2I ι)))

Initializing...

`BookProof.CoreBounds.tendsto_trunc_inc` [DecidableEq ι] (c : ι → ℝ) (x : maxDom c) : Tendsto (fun S : Finset ι => ((trunc c x S : lpFiniteModes ι) : L2I ι)) atTop (𝓝 ((x : L2I ι))) · Prove2Me