Lindelöf and paracompact spaces

Inspired by PR #7160. Here are some possible steps, non-exhaustive :-)

Lindelöf spaces

• definition (every open cover has a countable subcover)
• #9168
• $\sigma$-compact spaces are Lindelöf
• basic properties: countable unions, images of Lindelöf sets and spaces are Lindelöf
• follow-up: adapt e.g. CompactExhaustion.choice to ask for Lindelöf instead; audit comments mentioning "Lindelöf"

extension: hereditarily Lindelöf spaces

• definition: every subspace is Lindelöf (see pi-base)
• Lindelöf implies hereditarily Lindelöf
• a Lindelöf $G_\delta$ space is hereditarily Lindelöf
• secound countable implies hereditarily Lindelöf

Paracompact spaces

• definition
• locally compact and sigma-compact spaces are paracompact,
  in particular compact spaces are paracompact
• every metric space is paracompact

Corollary of both: a locally compact second countable Hausdorff space is paracompact.

Lots of potential for extensions, e.g.

• locally compact + second countable implies $\sigma$-compact
• show these notions coincide over metric spaces

Start by reading the existing topology material referenced in Mathlib/Topology/Paracompact.html and Mathlib/Topology/SubsetProperties.html, then inspect CompactExhaustion.choice for the Lindelöf follow-up. Choose one unchecked item, such as the Lindelöf Gδ result or the metric-space equivalence, and confirm its assumptions and nearby theorem style. Done means the selected result is formalized with appropriate supporting updates.