English
There exists a BoundedMul structure on NonUnitalSeminormedRing.
Русский
Существует структура BoundedMul на NonUnitalSeminormedRing.
LaTeX
$$$\exists\text{BoundedMul}(R)$$$
Lean4
instance : BoundedMul R where
isBounded_mul {s t} hs
ht := by
obtain ⟨Af, hAf⟩ := (Metric.isBounded_iff_subset_closedBall 0).mp hs
obtain ⟨Ag, hAg⟩ := (Metric.isBounded_iff_subset_closedBall 0).mp ht
rw [Metric.isBounded_iff] at hs ht ⊢
use 2 * Af * Ag
intro z hz w hw
obtain ⟨x₁, hx₁, y₁, hy₁, z_eq⟩ := Set.mem_mul.mp hz
obtain ⟨x₂, hx₂, y₂, hy₂, w_eq⟩ := Set.mem_mul.mp hw
rw [← w_eq, ← z_eq, dist_eq_norm]
have hAf' : 0 ≤ Af := Metric.nonempty_closedBall.mp ⟨_, hAf hx₁⟩
have aux : ∀ {x y}, x ∈ s → y ∈ t → ‖x * y‖ ≤ Af * Ag :=
by
intro x y x_in_s y_in_t
apply (norm_mul_le _ _).trans (mul_le_mul _ _ (norm_nonneg _) hAf')
· exact mem_closedBall_zero_iff.mp (hAf x_in_s)
· exact mem_closedBall_zero_iff.mp (hAg y_in_t)
calc
‖x₁ * y₁ - x₂ * y₂‖
_ ≤ ‖x₁ * y₁‖ + ‖x₂ * y₂‖ := (norm_sub_le _ _)
_ ≤ Af * Ag + Af * Ag := (add_le_add (aux hx₁ hy₁) (aux hx₂ hy₂))
_ = 2 * Af * Ag := by simp [← two_mul, mul_assoc]
