English
Let la and lb be filters on α and β with bases {sa(i)} and {sb(j)} respectively, and let f: α → β satisfy Tendsto(f, la, lb). Then for every j with pb(j), there exists i with pa(i) such that f[sa(i)] ⊆ sb(j).
Русский
Пусть фильтры la на α и lb на β имеют базы {sa(i)} и {sb(j)} соответственно, и пусть f: α → β удовлетворяет переходу Tendsto(f, la, lb). Тогда для каждого индекса j с PB(j) существует i, для которого PA(i) и выполняется f[sa(i)] ⊆ sb(j).
LaTeX
$$$\text{Let } \mathcal{L} \text{ } \mathcal{M} \text{ be filters with bases } \{S_i\}_{i\in I}, \{T_j\}_{j\in J} \text{ respectively, and } f: X \to Y.\text{ If } f_*(\mathcal{L}) \le \mathcal{M}, \text{ then for every } j, \; pb(j) \implies \exists i, pa(i) \land f[S_i] \subseteq T_j.$$$
Lean4
theorem basis_both (H : Tendsto f la lb) (hla : la.HasBasis pa sa) (hlb : lb.HasBasis pb sb) :
∀ ib, pb ib → ∃ ia, pa ia ∧ MapsTo f (sa ia) (sb ib) :=
(hla.tendsto_iff hlb).1 H
