English
Same as LebesgueNumberSUnion, expressed for a possibly different presentation of the cover.
Русский
То же самое, что и Лемма Лебега для суммы, возможно для другой записи покрытия.
LaTeX
$$$\text{IsCompact}(s) \rightarrow (\forall t \in c, \ IsOpen(t)) \rightarrow s \subseteq \bigcup c.sUnion \rightarrow \exists \delta>0, \forall x\in s, \exists t \in c, \ball(x,\delta) \subseteq t$$$
Lean4
/-- A finite product of pseudometric spaces is a pseudometric space, with the sup distance. -/
instance pseudoMetricSpacePi : PseudoMetricSpace (∀ b, X b) := by
/- we construct the instance from the pseudoemetric space instance to avoid checking again that
the uniformity is the same as the product uniformity, but we register nevertheless a nice
formula for the distance -/
let i :=
PseudoEMetricSpace.toPseudoMetricSpaceOfDist
(fun f g : ∀ b, X b => ((sup univ fun b => nndist (f b) (g b) : ℝ≥0) : ℝ))
(fun f g => ((Finset.sup_lt_iff bot_lt_top).2 fun b _ => edist_lt_top _ _).ne)
(fun f g => by simp only [edist_pi_def, edist_nndist, ← ENNReal.coe_finset_sup, ENNReal.coe_toReal])
refine i.replaceBornology fun s => ?_
simp only [isBounded_iff_eventually, ← forall_isBounded_image_eval_iff, forall_mem_image, ← Filter.eventually_all,
@dist_nndist (X _)]
refine eventually_congr ((eventually_ge_atTop 0).mono fun C hC ↦ ?_)
lift C to ℝ≥0 using hC
refine
⟨fun H x hx y hy ↦ NNReal.coe_le_coe.2 <| Finset.sup_le fun b _ ↦ H b hx hy, fun H b x hx y hy ↦
NNReal.coe_le_coe.2 ?_⟩
simpa only using Finset.sup_le_iff.1 (NNReal.coe_le_coe.1 <| H hx hy) b (Finset.mem_univ b)
