case intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.2354
E : Type u_2
ι : Sort ?u.2360
κ : ι → Sort ?u.2365
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t u v A B : Set E
hv : Absorbs 𝕜 s v
a : ℝ
ha : 0 < a
hu : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
⊢ Absorbs 𝕜 s (u ∪ v)
𝕜 : Type u_1
𝕝 : Type ?u.2354
E : Type u_2
ι : Sort ?u.2360
κ : ι → Sort ?u.2365
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t u v A B : Set E
hu : Absorbs 𝕜 s u
hv : Absorbs 𝕜 s v
⊢ Absorbs 𝕜 s (u ∪ v)
obtain ⟨a, ha, hu⟩ := hu
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.2354
E : Type u_2
ι : Sort ?u.2360
κ : ι → Sort ?u.2365
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t u v A B : Set E
a : ℝ
ha : 0 < a
hu : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
b : ℝ
_hb : 0 < b
hv : ∀ (a : 𝕜), b ≤ ‖a‖ → v ⊆ a • s
⊢ Absorbs 𝕜 s (u ∪ v)
case intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.2354
E : Type u_2
ι : Sort ?u.2360
κ : ι → Sort ?u.2365
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t u v A B : Set E
hv : Absorbs 𝕜 s v
a : ℝ
ha : 0 < a
hu : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
⊢ Absorbs 𝕜 s (u ∪ v)
obtain ⟨b, _hb, hv⟩ := hv
no goals
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.2354
E : Type u_2
ι : Sort ?u.2360
κ : ι → Sort ?u.2365
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t u v A B : Set E
a : ℝ
ha : 0 < a
hu : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
b : ℝ
_hb : 0 < b
hv : ∀ (a : 𝕜), b ≤ ‖a‖ → v ⊆ a • s
⊢ Absorbs 𝕜 s (u ∪ v)
exact
  ⟨max a b, lt_max_of_lt_left ha, fun c hc =>
    union_subset (hu _ <| le_of_max_le_left hc) (hv _ <| le_of_max_le_right hc)⟩