Good idea. Many thanks! > On 6 May 2025, at 07:30, 伊藤洋介 <glacier345 at gmail.com> wrote: > > However, the dual of this lemma (on the left-hand limit) is missing. > Could you consider adding the following code to Elementary_Topology.thy? > If there is an appropriate way to suggest improvements, please let me know. >