instBoundedMulNNReal — Mathlib

English

There is a BoundedMul structure on NNReal.

Русский

Существует структура BoundedMul на NNReal.

LaTeX

$$$\text{BoundedMul NNReal}$$$

Lean4

instance : BoundedMul ℝ≥0 where
  isBounded_mul {s t} hs
    ht := by
    obtain ⟨Af, hAf⟩ := (isBounded_iff_subset_closedBall 0).mp hs
    obtain ⟨Ag, hAg⟩ := (isBounded_iff_subset_closedBall 0).mp ht
    have key : IsCompact (closedBall (0 : ℝ≥0) Af ×ˢ closedBall (0 : ℝ≥0) Ag) :=
      IsCompact.prod (isCompact_closedBall _ _) (isCompact_closedBall _ _)
    apply Bornology.IsBounded.subset (key.image continuous_mul).isBounded
    intro _ ⟨x, x_in_s, y, y_in_t, xy_eq⟩
    exact ⟨⟨x, y⟩, by simpa only [Set.mem_prod] using ⟨⟨hAf x_in_s, hAg y_in_t⟩, xy_eq⟩⟩

Похожие утверждения