α : Type u_1
β : Type u_3
γ : Type ?u.69837
ι : Sort u_2
ι' : Sort ?u.69843
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
f : α → β
hla : HasBasis la pa sa
⊢ (∀ (t : Set β), t ∈ lb → ∃ i, pa i ∧ sa i ⊆ f ⁻¹' t) ↔ ∀ (t : Set β), t ∈ lb → ∃ i, pa i ∧ MapsTo f (sa i) t
α : Type u_1
β : Type u_3
γ : Type ?u.69837
ι : Sort u_2
ι' : Sort ?u.69843
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
f : α → β
hla : HasBasis la pa sa
⊢ Tendsto f la lb ↔ ∀ (t : Set β), t ∈ lb → ∃ i, pa i ∧ MapsTo f (sa i) t
simp only [Tendsto, (hla.map f).le_iff, image_subset_iff]
no goals
α : Type u_1
β : Type u_3
γ : Type ?u.69837
ι : Sort u_2
ι' : Sort ?u.69843
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
f : α → β
hla : HasBasis la pa sa
⊢ (∀ (t : Set β), t ∈ lb → ∃ i, pa i ∧ sa i ⊆ f ⁻¹' t) ↔ ∀ (t : Set β), t ∈ lb → ∃ i, pa i ∧ MapsTo f (sa i) t
rfl