instBoundedMulOfLipschitzMul — Mathlib

English

There is a bounded multiplication structure on R when Lipschitz multiplication is available.

Русский

Если существует липшицова умножение, то на R задаётся ограниченная операция умножения.

LaTeX

$$$\text{LipschitzMul}(R) \Rightarrow \text{BoundedMul}(R)$$$

Lean4

@[to_additive]
instance [PseudoMetricSpace R] [Monoid R] [LipschitzMul R] : BoundedMul R where
  isBounded_mul {s t} s_bdd
    t_bdd := by
    have bdd : Bornology.IsBounded (s ×ˢ t) := Bornology.IsBounded.prod s_bdd t_bdd
    obtain ⟨C, mul_lip⟩ := ‹LipschitzMul R›.lipschitz_mul
    convert mul_lip.isBounded_image bdd
    ext p
    simp only [Set.mem_image, Set.mem_prod, Prod.exists]
    constructor
    · intro ⟨a, a_in_s, b, b_in_t, eq_p⟩
      exact ⟨a, b, ⟨a_in_s, b_in_t⟩, eq_p⟩
    · intro ⟨a, b, ⟨a_in_s, b_in_t⟩, eq_p⟩
      simpa [← eq_p] using Set.mul_mem_mul a_in_s b_in_t

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