English
If hx expresses non-equality in the quotient, then toIcoMod hp a and toIocMod hp a are eventually equal along nhds x.
Русский
Если hx выражает неравенство в классе по отношению к zmultiples, то toIcoMod hp a и toIocMod hp a совпадают впоследствии в nhds x.
LaTeX
$$toIcoMod_eventuallyEq_toIocMod hp a (hx) : toIcoMod hp a =ᶠ[nhds x] toIocMod hp a$$
Lean4
theorem continuous_right_toIcoMod : ContinuousWithinAt (toIcoMod hp a) (Ici x) x :=
by
intro s h
rw [Filter.mem_map, mem_nhdsWithin_iff_exists_mem_nhds_inter]
haveI : Nontrivial 𝕜 := ⟨⟨0, p, hp.ne⟩⟩
simp_rw [mem_nhds_iff_exists_Ioo_subset] at h ⊢
obtain ⟨l, u, hxI, hIs⟩ := h
let d := toIcoDiv hp a x • p
have hd := toIcoMod_mem_Ico hp a x
simp_rw [subset_def, mem_inter_iff]
refine ⟨_, ⟨l + d, min (a + p) u + d, ?_, fun x => id⟩, fun y => ?_⟩ <;>
simp_rw [← sub_mem_Ioo_iff_left, mem_Ioo, lt_min_iff]
· exact ⟨hxI.1, hd.2, hxI.2⟩
· rintro ⟨h, h'⟩
apply hIs
rw [← toIcoMod_sub_zsmul, (toIcoMod_eq_self _).2]
exacts [⟨h.1, h.2.2⟩, ⟨hd.1.trans (sub_le_sub_right h' _), h.2.1⟩]
