𝕜 : Type u_1
𝕝 : Type ?u.43430
E : Type u_2
ι : Sort ?u.43436
κ : ι → Sort ?u.43441
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s s₁ s₂ t t₁ t₂ : Set E
hs : Balanced 𝕜 s
ht : Balanced 𝕜 t
⊢ Balanced 𝕜 (s + -t)
𝕜 : Type u_1
𝕝 : Type ?u.43430
E : Type u_2
ι : Sort ?u.43436
κ : ι → Sort ?u.43441
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s s₁ s₂ t t₁ t₂ : Set E
hs : Balanced 𝕜 s
ht : Balanced 𝕜 t
⊢ Balanced 𝕜 (s - t)
simp_rw [sub_eq_add_neg]
no goals
𝕜 : Type u_1
𝕝 : Type ?u.43430
E : Type u_2
ι : Sort ?u.43436
κ : ι → Sort ?u.43441
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s s₁ s₂ t t₁ t₂ : Set E
hs : Balanced 𝕜 s
ht : Balanced 𝕜 t
⊢ Balanced 𝕜 (s + -t)
exact hs.add ht.neg