English
Let f: α → β. If Tendsto f l1 lb1 and lb1 and lb2 are disjoint, and Tendsto f l2 lb2, then la1 and la2 are disjoint. Concretely, convergence into two disjoint targets forces the source filters to be disjoint as well.
Русский
Пусть f: α → β. Если Tendsto f la1 lb1 и lb1 ⊥ lb2, и Tendsto f la2 lb2, то la1 ⊥ la2. Фактически: сходимость через f в две несовместные фильтры на β влечет за собой несовместность фильтров на α.
LaTeX
$$$\\forall f:\\alpha \\to \\beta, \\forall la_1 la_2:\\mathrm{Filter}(\\alpha), \\forall lb_1 lb_2:\\mathrm{Filter}(\\beta),\\; \\mathrm{Tendsto} f\\ la_1\\ lb_1 \\to \\mathrm{Disjoint}\\ lb_1 lb_2 \\to \\mathrm{Tendsto} f\\ la_2\\ lb_2 \\Rightarrow \\mathrm{Disjoint}\\ la_1 la_2$$$
Lean4
protected theorem disjoint {f : α → β} {la₁ la₂ : Filter α} {lb₁ lb₂ : Filter β} (h₁ : Tendsto f la₁ lb₁)
(hd : Disjoint lb₁ lb₂) (h₂ : Tendsto f la₂ lb₂) : Disjoint la₁ la₂ :=
(disjoint_comap hd).mono h₁.le_comap h₂.le_comap
