English
Let i ↦ if p(i) then a else b be a function into a topological space, and F,G be filters with neighborhoods around a and b as in the hypotheses. Then the limit to the conditional target (depending on q) is equivalent to eventual agreement p(i) ↔ q.
Русский
Пусть i ↦ if p(i) then a иначе b — функция в топологическом пространстве. Тогда переход к пределу к соответствующему фильтру равносилен тому, что в большинстве i выполняется p(i) ↔ q.
LaTeX
$$$\operatorname{Tendsto}\big(i \mapsto \mathbf{if}\ p(i)\ \mathbf{then}\ a\ \mathbf{else}\ b\big)\;L\;\big(\mathbf{if}\ q\ \mathbf{then}\ F\ \mathbf{else}\ G\big) \ \Longleftrightarrow\ \forall^\infty i\in L\, (p(i) \leftrightarrow q)$$
Lean4
theorem tendsto_ite {β : Type*} {p : ι → Prop} [DecidablePred p] {q : Prop} [Decidable q] {a b : β} {F G : Filter β}
(haG : { a }ᶜ ∈ G) (hbF : { b }ᶜ ∈ F) (haF : principal { a } ≤ F) (hbG : principal { b } ≤ G) :
Tendsto (fun i ↦ if p i then a else b) L (if q then F else G) ↔ ∀ᶠ i in L, p i ↔ q :=
by
constructor <;> intro h
· by_cases hq : q
· simp only [hq, ite_true] at h
filter_upwards [mem_map.mp (h hbF)] with i hi
simp only [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff, ite_eq_right_iff,
not_forall, exists_prop] at hi
tauto
· simp only [hq, ite_false] at h
filter_upwards [mem_map.mp (h haG)] with i hi
simp only [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff, ite_eq_left_iff,
not_forall, exists_prop] at hi
tauto
· have obs : (fun _ ↦ if q then a else b) =ᶠ[L] (fun i ↦ if p i then a else b) :=
by
filter_upwards [h] with i hi
simp only [hi]
apply Tendsto.congr' obs
by_cases hq : q
· simp only [hq, ite_true]
apply le_trans _ haF
simp only [principal_singleton, le_pure_iff, mem_map, Set.mem_singleton_iff, Set.preimage_const_of_mem, univ_mem]
· simp only [hq, ite_false]
apply le_trans _ hbG
simp only [principal_singleton, le_pure_iff, mem_map, Set.mem_singleton_iff, Set.preimage_const_of_mem, univ_mem]
