闭区间套定理推导证明聚点定理

1from manim import *2import numpy as np3import random4 5# 配置中文环境6config.tex_template = TexTemplateLibrary.ctex  # 使用ctex模板7 8class NestedIntervalClusterPoint(Scene):9    def construct(self):10        # 使用黑色背景11        self.camera.background_color = BLACK12        13        # 创建标题并快速显示/消失14        title = MathTex(r"\text{闭区间套定理} \Rightarrow \text{聚点定理}").scale(1.2)15        self.play(Write(title))16        self.wait(1)17        self.play(FadeOut(title))18        19        # 创建数轴20        number_line = NumberLine(21            x_range=[-2, 8, 1],22            length=12,23            include_numbers=False,24            include_tip=True25        )26        self.play(Create(number_line))27        self.wait(0.5)28        29        # 定义有界无限集E的边界30        a, b = 0, 631        32        # 添加边界标记33        a_dot = Dot(number_line.n2p(a), color=YELLOW)34        b_dot = Dot(number_line.n2p(b), color=YELLOW)35        a_label = MathTex("a").next_to(a_dot, DOWN)36        b_label = MathTex("b").next_to(b_dot, DOWN)37        38        self.play(39            Create(a_dot), Create(b_dot),40            Write(a_label), Write(b_label)41        )42        43        # 显示区间E44        interval_E = Line(45            start=number_line.n2p(a),46            end=number_line.n2p(b),47            color=BLUE_A,48            stroke_width=849        )50        interval_E_label = MathTex("E").next_to(interval_E, DOWN, buff=0.5)51        52        self.play(Create(interval_E), Write(interval_E_label))53        54        # 在E上方添加集合的定义 - 修改E的无穷表达方式55        set_definition = MathTex(r"E \subset [a,b], E \text{ 是无限点集}").to_edge(UP, buff=0.8)56        self.play(Write(set_definition))57        58        # 创建随机点集(有界无限集的可视化)59        points_coords = [random.uniform(a, b) for _ in range(30)]60        points_coords.sort()61        62        points = VGroup()63        for coord in points_coords:64            dot = Dot(number_line.n2p(coord), radius=0.05, color=GREEN, z_index=2)  # 设置z_index=2，确保绿色点在上层显示65            points.add(dot)66        67        self.play(Create(points), run_time=1.5)68        69        # 构造闭区间套70        left, right = a, b71        interval_width = right - left72        intervals = []73        interval_labels = []74        75        # 创建初始区间I176        interval = Line(77            start=number_line.n2p(left),78            end=number_line.n2p(right),79            color=YELLOW,80            stroke_width=6,81            z_index=1  # 设置z_index=1，确保区间在点的下层82        )83        interval_label = MathTex("I_1").next_to(interval, UP, buff=0.5)84        85        intervals.append(interval)86        interval_labels.append(interval_label)87        88        self.play(89            Create(interval),90            Write(interval_label)91        )92        93        # 显示I1区间的端点94        left_dot = Dot(number_line.n2p(left), color=RED)95        right_dot = Dot(number_line.n2p(right), color=RED)96        left_label = MathTex("a_1").next_to(left_dot, DOWN+LEFT, buff=0.2)97        right_label = MathTex("b_1").next_to(right_dot, DOWN+RIGHT, buff=0.2)98        99        self.play(100            Create(left_dot), Create(right_dot),101            Write(left_label), Write(right_label)102        )103        104        # 闭区间套公理105        axiom = MathTex(r"\text{闭区间套定理: } I_1 \supset I_2 \supset \cdots, |I_n| \to 0 \Rightarrow \bigcap_{n=1}^{\infty} I_n = \{c\}")106        axiom.scale(0.8).to_edge(UP, buff=0.2)107        108        # 先淡出集合定义，再显示公理109        self.play(FadeOut(set_definition))110        self.play(Write(axiom))111        112        # 存储所有端点标签以便处理重叠113        endpoint_labels = [left_label, right_label]114        endpoint_dots = [left_dot, right_dot]115        116        # 存储所有区间端点的值，用于后续演示117        a_n_values = [left]118        b_n_values = [right]119        120        # 构造后续区间121        for i in range(1, 5):122            # 将当前区间二分123            mid = (left + right) / 2124            125            # 计算左右子区间中点的数量126            left_points = sum(1 for coord in points_coords if left <= coord <= mid)127            right_points = sum(1 for coord in points_coords if mid < coord <= right)128            129            # 选择包含更多点的子区间130            if left_points >= right_points:131                new_left, new_right = left, mid132            else:133                new_left, new_right = mid, right134            135            # 存储端点值136            a_n_values.append(new_left)137            b_n_values.append(new_right)138            139            # 创建新区间140            new_interval = Line(141                start=number_line.n2p(new_left),142                end=number_line.n2p(new_right),143                color=YELLOW,144                stroke_width=6-i145            )146            new_interval_label = MathTex(f"I_{i+1}").next_to(new_interval, UP, buff=0.5)147            148            intervals.append(new_interval)149            interval_labels.append(new_interval_label)150            151            # 突出显示被选中的子区间152            highlight_rect = SurroundingRectangle(153                new_interval, 154                color=GREEN, 155                buff=0.1,156                stroke_width=2157            )158            159            # 每次选择一个子区间的数学描述 - 更改表达方式160            selection_formula = MathTex(r"I_{" + str(i+1) + r"} \text{ 包含E中无穷多点}")161            selection_formula.next_to(highlight_rect, UP, buff=1.0)162            163            # 寻找需要淡出的重叠标签164            labels_to_fade = []165            166            # 创建新的端点和标签167            new_left_dot = Dot(number_line.n2p(new_left), color=RED)168            new_right_dot = Dot(number_line.n2p(new_right), color=RED)169            new_left_label = MathTex(f"a_{i+1}").next_to(new_left_dot, DOWN+LEFT, buff=0.2)170            new_right_label = MathTex(f"b_{i+1}").next_to(new_right_dot, DOWN+RIGHT, buff=0.2)171            172            # 检查并收集需要淡出的重叠标签173            for old_label, old_dot in zip(endpoint_labels, endpoint_dots):174                # 如果新旧点太接近，将旧标签添加到淡出列表175                for new_dot in [new_left_dot, new_right_dot]:176                    if np.linalg.norm(new_dot.get_center() - old_dot.get_center()) < 0.3:177                        labels_to_fade.append(old_label)178            179            self.play(180                Create(highlight_rect),181                Write(selection_formula),182                run_time=0.8183            )184            185            # 先淡出重叠的标签186            if labels_to_fade:187                self.play(*[FadeOut(label) for label in labels_to_fade], run_time=0.5)188            189            self.play(190                Create(new_interval),191                Write(new_interval_label),192                Create(new_left_dot), Create(new_right_dot),193                Write(new_left_label), Write(new_right_label),194                run_time=1195            )196            self.play(197                FadeOut(highlight_rect),198                FadeOut(selection_formula)199            )200            201            # 更新端点标签和点集合202            endpoint_labels.extend([new_left_label, new_right_label])203            endpoint_dots.extend([new_left_dot, new_right_dot])204            205            # 更新区间边界206            left, right = new_left, new_right207        208        # 标记交点c209        c_point = (left + right) / 2210        cluster_point = Dot(number_line.n2p(c_point), color=WHITE, radius=0.1, z_index=3)  # 设置更高的z_index211        cluster_label = MathTex("c").next_to(cluster_point, UP, buff=0.3)212        213        # 交点c的出现动画214        self.play(215            FocusOn(number_line.n2p(c_point)),216            run_time=1217        )218        219        # 标记c为交点220        intersection_formula = MathTex(r"c \in \bigcap_{n=1}^{\infty} I_n")221        intersection_formula.next_to(cluster_point, UP, buff=1.0)222        223        # 找出需要淡出的元素，但保留点不淡出224        dots_to_remove = [mob for mob in self.mobjects if isinstance(mob, Dot) and mob != cluster_point]225        labels_to_remove = [mob for mob in self.mobjects if isinstance(mob, MathTex) and (mob in interval_labels or any(s in mob.tex_string for s in ["a_", "b_"]))]226        elements_to_clear = dots_to_remove + labels_to_remove227        228        # 确保最后一个区间(I5)也淡出229        last_interval = intervals[-1]230        231        # 清除一些元素，同时创建C点，但不降低点的不透明度232        self.play(233            *[FadeOut(elem) for elem in elements_to_clear],234            FadeOut(last_interval),  # 淡出I5235            Create(cluster_point),236            Write(cluster_label),237            run_time=1.5238        )239        240        self.play(Write(intersection_formula), run_time=1)241        self.wait(1)242        243        # 移除"FadeOut(axiom)"，保持闭区间套定理不淡出244        self.play(FadeOut(intersection_formula))245        246        # 演示c是聚点 - 创建ε邻域，但不显示括号247        epsilon = 0.8248        epsilon_interval = Line(249            start=number_line.n2p(c_point - epsilon),250            end=number_line.n2p(c_point + epsilon),251            color=ORANGE,252            stroke_width=4253        )254        epsilon_label = MathTex("(c-\\varepsilon, c+\\varepsilon)").next_to(epsilon_interval, UP, buff=0.5)255        256        self.play(257            Create(epsilon_interval),258            Write(epsilon_label)259        )260        261        # 创建在ε邻域内的点 - 修改为红色262        epsilon_points = []263        epsilon_old_dots = []264        # 复用已有的点，只改变颜色265        for coord in points_coords:266            if c_point - epsilon < coord < c_point + epsilon:267                # 找到对应的已有点并增加亮度268                for dot in points:269                    if np.allclose(dot.get_center(), number_line.n2p(coord), atol=0.01):270                        epsilon_point = Dot(number_line.n2p(coord), color=RED, radius=0.06, z_index=4)  # 改为红色271                        epsilon_points.append(epsilon_point)272                        epsilon_old_dots.append(dot)273                        break274        275        # 分批次显示ε邻域内的点276        for i in range(0, len(epsilon_points), 3):277            end_idx = min(i+3, len(epsilon_points))278            batch = epsilon_points[i:end_idx]279            self.play(*[Create(dot) for dot in batch], run_time=0.3)280        281        # 在显示完红色点之后，显示"必有区间[an, bn]在c的邻域内"282        # 选择一个足够大的n，使得[an, bn]完全包含在c的ε邻域内283        n = 4  # 使用区间I5284        285        # 创建显示[an, bn]的区间286        an_bn_interval = Line(287            start=number_line.n2p(a_n_values[n]),288            end=number_line.n2p(b_n_values[n]),289            color=YELLOW,290            stroke_width=3,291            z_index=2292        )293        294        # 创建[an, bn]的端点295        an_dot = Dot(number_line.n2p(a_n_values[n]), color=RED, radius=0.08)296        bn_dot = Dot(number_line.n2p(b_n_values[n]), color=RED, radius=0.08)297        # 使用通用的an和bn标签，而不是a5和b5298        an_label = MathTex("a_n").next_to(an_dot, DOWN+LEFT, buff=0.2)299        bn_label = MathTex("b_n").next_to(bn_dot, DOWN+RIGHT, buff=0.2)300        301        # 创建说明文本302        interval_in_neighborhood = MathTex(r"\exists n, [a_n, b_n] \subset (c-\varepsilon, c+\varepsilon)")303        interval_in_neighborhood.next_to(epsilon_label, UP, buff=0.5)304        305        # 显示区间和端点306        self.play(307            Create(an_bn_interval),308            Create(an_dot), Create(bn_dot),309            Write(an_label), Write(bn_label)310        )311        312        # 突出显示区间包含在ε邻域内313        highlight_inclusion = SurroundingRectangle(314            an_bn_interval, 315            color=GREEN_A, 316            buff=0.1,317            stroke_width=2318        )319        320        self.play(321            Create(highlight_inclusion),322            Write(interval_in_neighborhood)323        )324        self.wait(1)325        326        self.play(327            FadeOut(highlight_inclusion),328            FadeOut(interval_in_neighborhood),329            FadeOut(an_bn_interval),330            FadeOut(an_dot), FadeOut(bn_dot),331            FadeOut(an_label), FadeOut(bn_label)332        )333        334        # 最终结论335        conclusion = MathTex(r"\text{聚点定理: 任何有界无限点集} E \subset \mathbb{R} \text{ 至少有一个聚点}")336        conclusion.scale(0.8).to_edge(DOWN, buff=0.5)337        self.play(Write(conclusion))338        339        # 突出显示聚点340        self.play(341            cluster_point.animate.scale(1.5).set_color(YELLOW),342            run_time=1343        )344        self.play(345            cluster_point.animate.scale(1/1.5).set_color(WHITE),346            run_time=1347        )348        349        self.wait(2)350 351if __name__ == "__main__":352    import os353    os.system("manim -pqh nested_interval_cluster_point.py NestedIntervalClusterPoint")