mathlib

0a28adf1 - feat(topology/continuous_function/bounded): continuous bounded real-valued functions form a normed vector lattice (#10322)

feat(topology/continuous_function/bounded): continuous bounded real-valued functions form a normed vector lattice (#10322) feat(topology/continuous_function/bounded): continuous bounded real-valued functions form a normed vector lattice Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>