case intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.125647
E : Type u_2
ι : Sort ?u.125653
κ : ι → Sort ?u.125658
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
ht : Absorbs 𝕜 t u
a : ℝ
ha : 0 < a
hs : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
⊢ Absorbs 𝕜 (s ∩ t) u
𝕜 : Type u_1
𝕝 : Type ?u.125647
E : Type u_2
ι : Sort ?u.125653
κ : ι → Sort ?u.125658
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Absorbs 𝕜 s u
ht : Absorbs 𝕜 t u
⊢ Absorbs 𝕜 (s ∩ t) u
obtain ⟨a, ha, hs⟩ := hs
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.125647
E : Type u_2
ι : Sort ?u.125653
κ : ι → Sort ?u.125658
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b✝ : 𝕜
a : ℝ
ha : 0 < a
hs : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
b : ℝ
_hb : 0 < b
ht : ∀ (a : 𝕜), b ≤ ‖a‖ → u ⊆ a • t
⊢ Absorbs 𝕜 (s ∩ t) u
case intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.125647
E : Type u_2
ι : Sort ?u.125653
κ : ι → Sort ?u.125658
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
ht : Absorbs 𝕜 t u
a : ℝ
ha : 0 < a
hs : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
⊢ Absorbs 𝕜 (s ∩ t) u
obtain ⟨b, _hb, ht⟩ := ht
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.125647
E : Type u_2
ι : Sort ?u.125653
κ : ι → Sort ?u.125658
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b✝ : 𝕜
a : ℝ
ha : 0 < a
hs : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
b : ℝ
_hb : 0 < b
ht : ∀ (a : 𝕜), b ≤ ‖a‖ → u ⊆ a • t
h : 0 < max a b
⊢ Absorbs 𝕜 (s ∩ t) u
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.125647
E : Type u_2
ι : Sort ?u.125653
κ : ι → Sort ?u.125658
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b✝ : 𝕜
a : ℝ
ha : 0 < a
hs : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
b : ℝ
_hb : 0 < b
ht : ∀ (a : 𝕜), b ≤ ‖a‖ → u ⊆ a • t
⊢ Absorbs 𝕜 (s ∩ t) u
have h : 0 < max a b := lt_max_of_lt_left ha
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.125647
E : Type u_2
ι : Sort ?u.125653
κ : ι → Sort ?u.125658
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b✝ : 𝕜
a : ℝ
ha : 0 < a
hs : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
b : ℝ
_hb : 0 < b
ht : ∀ (a : 𝕜), b ≤ ‖a‖ → u ⊆ a • t
h : 0 < max a b
c : 𝕜
hc : max a b ≤ ‖c‖
⊢ u ⊆ c • (s ∩ t)
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.125647
E : Type u_2
ι : Sort ?u.125653
κ : ι → Sort ?u.125658
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b✝ : 𝕜
a : ℝ
ha : 0 < a
hs : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
b : ℝ
_hb : 0 < b
ht : ∀ (a : 𝕜), b ≤ ‖a‖ → u ⊆ a • t
h : 0 < max a b
⊢ Absorbs 𝕜 (s ∩ t) u
refine' ⟨max a b, lt_max_of_lt_left ha, fun c hc => _⟩
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.125647
E : Type u_2
ι : Sort ?u.125653
κ : ι → Sort ?u.125658
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b✝ : 𝕜
a : ℝ
ha : 0 < a
hs : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
b : ℝ
_hb : 0 < b
ht : ∀ (a : 𝕜), b ≤ ‖a‖ → u ⊆ a • t
h : 0 < max a b
c : 𝕜
hc : max a b ≤ ‖c‖
⊢ u ⊆ c • s ∩ c • t
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.125647
E : Type u_2
ι : Sort ?u.125653
κ : ι → Sort ?u.125658
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b✝ : 𝕜
a : ℝ
ha : 0 < a
hs : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
b : ℝ
_hb : 0 < b
ht : ∀ (a : 𝕜), b ≤ ‖a‖ → u ⊆ a • t
h : 0 < max a b
c : 𝕜
hc : max a b ≤ ‖c‖
⊢ u ⊆ c • (s ∩ t)
rw [smul_set_inter₀ (norm_pos_iff.1 <| h.trans_le hc)]
no goals
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.125647
E : Type u_2
ι : Sort ?u.125653
κ : ι → Sort ?u.125658
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b✝ : 𝕜
a : ℝ
ha : 0 < a
hs : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
b : ℝ
_hb : 0 < b
ht : ∀ (a : 𝕜), b ≤ ‖a‖ → u ⊆ a • t
h : 0 < max a b
c : 𝕜
hc : max a b ≤ ‖c‖
⊢ u ⊆ c • s ∩ c • t
exact subset_inter (hs _ <| le_of_max_le_left hc) (ht _ <| le_of_max_le_right hc)