English
If a filter l has the Icc convergence property, then it also has the uIcc convergence property; the uIcc construction preserves tendsto behavior from Icc.
Русский
Если фильтр l обладает свойством схождения Icc, то он сохраняет свойство схождения uIcc; конструкция uIcc сохраняет поведение Tendsto для Icc.
LaTeX
$$$$ \operatorname{TendstoIxxClass}(\mathrm{uIcc}, l, l) $$$$
Lean4
instance tendsto_uIcc_of_Icc {l : Filter α} [TendstoIxxClass Icc l l] : TendstoIxxClass uIcc l l :=
by
refine ⟨fun s hs => mem_map.2 <| mem_prod_self_iff.2 ?_⟩
obtain ⟨t, htl, hts⟩ : ∃ t ∈ l, ∀ p ∈ (t : Set α) ×ˢ t, Icc (p : α × α).1 p.2 ∈ s :=
mem_prod_self_iff.1 (mem_map.1 (tendsto_fst.Icc tendsto_snd hs))
refine ⟨t, htl, fun p hp => ?_⟩
rcases le_total p.1 p.2 with h | h
· rw [mem_preimage, uIcc_of_le h]
exact hts p hp
· rw [mem_preimage, uIcc_of_ge h]
exact hts ⟨p.2, p.1⟩ ⟨hp.2, hp.1⟩
