𝓕 : Type ?u.1099733
𝕜 : Type ?u.1099736
α : Type ?u.1099739
ι : Type ?u.1099742
κ : Type ?u.1099745
E : Type u_1
F : Type ?u.1099751
G : Type ?u.1099754
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁✝ a₂✝ b b₁✝ b₂✝ : E
r r₁ r₂ : ℝ
a₁ a₂ b₁ b₂ : E
⊢ ↑(nndist (a₁ * a₂) (b₁ * b₂)) ≤ ↑(nndist a₁ b₁) + ↑(nndist a₂ b₂)
𝓕 : Type ?u.1099733
𝕜 : Type ?u.1099736
α : Type ?u.1099739
ι : Type ?u.1099742
κ : Type ?u.1099745
E : Type u_1
F : Type ?u.1099751
G : Type ?u.1099754
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁✝ a₂✝ b b₁✝ b₂✝ : E
r r₁ r₂ : ℝ
a₁ a₂ b₁ b₂ : E
⊢ edist (a₁ * a₂) (b₁ * b₂) ≤ edist a₁ b₁ + edist a₂ b₂
simp only [edist_nndist]
𝓕 : Type ?u.1099733
𝕜 : Type ?u.1099736
α : Type ?u.1099739
ι : Type ?u.1099742
κ : Type ?u.1099745
E : Type u_1
F : Type ?u.1099751
G : Type ?u.1099754
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁✝ a₂✝ b b₁✝ b₂✝ : E
r r₁ r₂ : ℝ
a₁ a₂ b₁ b₂ : E
⊢ nndist (a₁ * a₂) (b₁ * b₂) ≤ nndist a₁ b₁ + nndist a₂ b₂
𝓕 : Type ?u.1099733
𝕜 : Type ?u.1099736
α : Type ?u.1099739
ι : Type ?u.1099742
κ : Type ?u.1099745
E : Type u_1
F : Type ?u.1099751
G : Type ?u.1099754
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁✝ a₂✝ b b₁✝ b₂✝ : E
r r₁ r₂ : ℝ
a₁ a₂ b₁ b₂ : E
⊢ ↑(nndist (a₁ * a₂) (b₁ * b₂)) ≤ ↑(nndist a₁ b₁) + ↑(nndist a₂ b₂)
norm_cast
no goals
𝓕 : Type ?u.1099733
𝕜 : Type ?u.1099736
α : Type ?u.1099739
ι : Type ?u.1099742
κ : Type ?u.1099745
E : Type u_1
F : Type ?u.1099751
G : Type ?u.1099754
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁✝ a₂✝ b b₁✝ b₂✝ : E
r r₁ r₂ : ℝ
a₁ a₂ b₁ b₂ : E
⊢ nndist (a₁ * a₂) (b₁ * b₂) ≤ nndist a₁ b₁ + nndist a₂ b₂
apply nndist_mul_mul_le