English
A lower linear growth expressed as an InfTopHom from sequences to EReal, given by toFun = linearGrowthInf, map_inf' = linearGrowthInf_inf, map_top' = linearGrowthInf_top.
Русский
Нижний линейный рост в виде InfTopHom от последовательностей к EReal, задающийся toFun = linearGrowthInf, map_inf' = linearGrowthInf_inf, map_top' = linearGrowthInf_top.
LaTeX
$$$\text{linearGrowthInfTopHom} : \operatorname{InfTopHom}(\mathbb{N} \to \mathbb{E}, \mathbb{E}),\; \text{toFun}=\operatorname{linearGrowthInf},\; \text{map\_inf'}=\operatorname{linearGrowthInf\_inf},\; \text{map\_top'}=\operatorname{linearGrowthInf\_top}$$$
Lean4
/-- Lower linear growth as an `InfTopHom`. -/
noncomputable def linearGrowthInfTopHom : InfTopHom (ℕ → EReal) EReal
where
toFun := linearGrowthInf
map_inf' _ _ := linearGrowthInf_inf
map_top' := linearGrowthInf_top
