𝕜 : Type u_1
𝕝 : Type ?u.6565
E : Type u_2
ι : Sort ?u.6571
κ : ι → Sort ?u.6576
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t u v A B : Set E
hA : Absorbent 𝕜 A
hAB : A ⊆ B
x : E
⊢ (∃ r, 0 < r ∧ ∀ (a : 𝕜), r ≤ ‖a‖ → x ∈ a • A) → ∃ r, 0 < r ∧ ∀ (a : 𝕜), r ≤ ‖a‖ → x ∈ a • B
𝕜 : Type u_1
𝕝 : Type ?u.6565
E : Type u_2
ι : Sort ?u.6571
κ : ι → Sort ?u.6576
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t u v A B : Set E
hA : Absorbent 𝕜 A
hAB : A ⊆ B
⊢ Absorbent 𝕜 B
refine' forall_imp (fun x => _) hA
no goals
𝕜 : Type u_1
𝕝 : Type ?u.6565
E : Type u_2
ι : Sort ?u.6571
κ : ι → Sort ?u.6576
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t u v A B : Set E
hA : Absorbent 𝕜 A
hAB : A ⊆ B
x : E
⊢ (∃ r, 0 < r ∧ ∀ (a : 𝕜), r ≤ ‖a‖ → x ∈ a • A) → ∃ r, 0 < r ∧ ∀ (a : 𝕜), r ≤ ‖a‖ → x ∈ a • B
exact Exists.imp fun r => And.imp_right <| forall₂_imp fun a _ha hx => Set.smul_set_mono hAB hx