α : Type u_2
β : Type u_1
ι : Sort ?u.3977
l l' la : Filter α
lb : Filter β
s t : α → Set β
ht : ∀ (t_1 : Set β), t_1 ∈ lb → ∀ᶠ (x : α) in la, t x ⊆ t_1
hst : ∀ᶠ (x : α) in la, s x ⊆ t x
⊢ ∀ (t : Set β), t ∈ lb → ∀ᶠ (x : α) in la, s x ⊆ t
α : Type u_2
β : Type u_1
ι : Sort ?u.3977
l l' la : Filter α
lb : Filter β
s t : α → Set β
ht : Tendsto t la (smallSets lb)
hst : ∀ᶠ (x : α) in la, s x ⊆ t x
⊢ Tendsto s la (smallSets lb)
rw [tendsto_smallSets_iff] at ht ⊢
no goals
α : Type u_2
β : Type u_1
ι : Sort ?u.3977
l l' la : Filter α
lb : Filter β
s t : α → Set β
ht : ∀ (t_1 : Set β), t_1 ∈ lb → ∀ᶠ (x : α) in la, t x ⊆ t_1
hst : ∀ᶠ (x : α) in la, s x ⊆ t x
⊢ ∀ (t : Set β), t ∈ lb → ∀ᶠ (x : α) in la, s x ⊆ t
exact fun u hu => (ht u hu).mp (hst.mono fun _ hst ht => hst.trans ht)