有限覆盖定理的证明

1# -*- coding: utf-8 -*-2from manim import *3import numpy as np4 5class FiniteCoveringProof(Scene):6    def construct(self):7        # 创建坐标系8        axes = Axes(9            x_range=[-1, 6, 1],10            y_range=[-0.5, 3.5, 0.5],11            x_length=10,12            y_length=6,13            axis_config={"include_tip": True}14        )15        16        self.play(Create(axes), run_time=1.5)17        18        # 创建闭区间 [0,5]19        interval = Line(20            axes.c2p(0, 0),21            axes.c2p(5, 0),22            color=WHITE,23            stroke_width=424        )25        endpoints = VGroup(26            Dot(axes.c2p(0, 0), radius=0.07),27            Dot(axes.c2p(5, 0), radius=0.07)28        )29        interval_labels = VGroup(30            MathTex("a").next_to(axes.c2p(0, 0), DOWN),31            MathTex("b").next_to(axes.c2p(5, 0), DOWN)32        )33        34        self.play(35            Create(interval),36            Create(endpoints),37            Write(interval_labels),38            run_time=1.539        )40 41        # 标题和反证法说明42        title = Text("有限覆盖定理的证明", color=BLUE).scale(0.8)43        title.to_corner(UP)44        self.play(Write(title), run_time=1.5)45        46        # 添加反证法假设47        assumption = Text("反证法：假设不存在有限子覆盖", color=RED).scale(0.6)48        assumption.next_to(title, DOWN)49        self.play(Write(assumption), run_time=1.5)50        51        # 展示开覆盖 - 修改为包含更多开集并明确是无限覆盖52        centers = [0.4, 1.2, 2.0, 2.8, 3.6, 4.4, 5.2]  # 增加更多中心点53        radii = [0.8, 0.7, 0.8, 0.7, 0.8, 0.7, 0.8]    # 对应的半径54        colors = [BLUE, RED, GREEN, YELLOW, BLUE_B, RED_B, GREEN_B]  # 更多颜色55        y_positions = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0]56        57        open_sets = VGroup()58        59        for i, (center, radius, color, y_pos) in enumerate(zip(centers, radii, colors, y_positions)):60            arc = Arc(61                radius=radius,62                angle=PI,63                color=color,64                stroke_width=3,65                fill_opacity=0.2,66                fill_color=color67            ).shift(axes.c2p(center, y_pos))68            69            # 只给前5个开集添加标签70            if i < 5:71                label = MathTex(f"U_{{{i+1}}}").set_color(color)72                label.next_to(arc, UP, buff=0.2)73                open_sets.add(VGroup(arc, label))74                75                self.play(76                    Create(arc),77                    Write(label),78                    run_time=0.8  # 放慢速度79                )80            else:81                # 最后几个开集快速创建，不添加标签82                open_sets.add(arc)83                self.play(Create(arc), run_time=0.6)  # 放慢速度84        85        # 添加省略号表示无限继续86        dots = MathTex(r"\ldots").scale(1.2).set_color(WHITE)87        dots.next_to(axes.c2p(5.5, 1.0), RIGHT, buff=0.1)88        self.play(Write(dots), run_time=1.0)89        90        # 添加无限开集的标签91        infinity_label = MathTex(r"U_n, n \in \mathbb{N}").set_color(WHITE)92        infinity_label.next_to(dots, UP, buff=0.2)93        self.play(Write(infinity_label), run_time=1.2)94 95        self.wait(1.5)96        97        # 淡化开覆盖，进入二分过程98        self.play(99            open_sets.animate.set_opacity(0.3),100            dots.animate.set_opacity(0.3),101            infinity_label.animate.set_opacity(0.3),102            run_time=1.5103        )104        105        # 初始划分106        mid_point = 2.5107        mid_dot = Dot(axes.c2p(mid_point, 0.5), color=YELLOW)108        left_interval = Line(109            axes.c2p(0, 0.5),110            axes.c2p(mid_point, 0.5),111            color=YELLOW112        )113        right_interval = Line(114            axes.c2p(mid_point, 0.5),115            axes.c2p(5, 0.5),116            color=YELLOW117        )118        119        # 添加区间端点标签120        a0_label = MathTex("a_0").scale(0.6).next_to(axes.c2p(0, 0.5), DOWN, buff=0.15)121        b0_label = MathTex("b_0").scale(0.6).next_to(axes.c2p(5, 0.5), DOWN, buff=0.15)122        123        # 添加简短说明124        split_text = Text("初始划分", color=YELLOW).scale(0.5)125        split_text.next_to(left_interval, UP, buff=0.2)126        127        self.play(128            Create(mid_dot),129            Create(left_interval),130            Create(right_interval),131            Write(split_text),132            Write(a0_label),133            Write(b0_label),134            run_time=1.8135        )136        137        # 选择左区间138        left_brace = Brace(left_interval, DOWN)139        left_text = Text("不能有限覆盖（下同）", color=YELLOW).scale(0.4)140        left_text.next_to(left_brace, DOWN, buff=0.1)141        142        self.play(143            Create(left_brace),144            Write(left_text),145            right_interval.animate.set_opacity(0.3),146            run_time=1.5147        )148        149        # 递归过程150        recursive_intervals = []151        current_left, current_right = 0, mid_point152        bisection_colors = [YELLOW_B, YELLOW_C, YELLOW_D]153        interval_endpoints = []  # 保存各区间端点154        endpoint_labels = VGroup()  # 端点标签组155        156        for i, color in enumerate(bisection_colors):157            y_level = 1.0 + (i+1) * 0.4158            new_mid = (current_left + current_right) / 2159            160            new_mid_dot = Dot(axes.c2p(new_mid, y_level), color=color)161            new_left = Line(162                axes.c2p(current_left, y_level),163                axes.c2p(new_mid, y_level),164                color=color165            )166            new_right = Line(167                axes.c2p(new_mid, y_level),168                axes.c2p(current_right, y_level),169                color=color170            )171            172            # 添加端点标签（不显示具体数值）173            a_label = MathTex(f"a_{{{i+1}}}").scale(0.5)174            a_label.next_to(axes.c2p(current_left, y_level), DOWN+LEFT, buff=0.1)175            mid_label = MathTex("").scale(0.5)  # 空标签，不显示中点值176            mid_label.next_to(axes.c2p(new_mid, y_level), DOWN, buff=0.1)177            b_label = MathTex(f"b_{{{i+1}}}").scale(0.5)178            b_label.next_to(axes.c2p(current_right, y_level), DOWN+RIGHT, buff=0.1)179            endpoint_labels.add(a_label, mid_label, b_label)180            181            recursive_intervals.append((current_left, current_right))182            183            self.play(184                Create(new_mid_dot),185                Create(new_left),186                Create(new_right),187                run_time=1.2188            )189            190            self.play(191                Write(a_label),192                Write(b_label),193                run_time=1.0194            )195            196            # 选择左区间或右区间（交替选择以展示递归过程）197            select_left = (i % 2 == 0)198            selected_line = new_left if select_left else new_right199            selected_brace = Brace(selected_line, DOWN)200            201            self.play(202                Create(selected_brace),203                (new_right if select_left else new_left).animate.set_opacity(0.3),204                run_time=1.2205            )206            207            # 保存区间端点208            if select_left:209                interval_endpoints.append((current_left, new_mid))210                current_right = new_mid211            else:212                interval_endpoints.append((new_mid, current_right))213                current_left = new_mid214        215        # 添加区间套说明216        interval_desc = Text("构造闭区间套", color=YELLOW_B).scale(0.5)217        interval_desc.to_corner(RIGHT).shift(LEFT * 2 + UP * 1)218        self.play(Write(interval_desc), run_time=1.2)219        220        # 计算最终区间位置和ξ的位置221        final_left, final_right = interval_endpoints[-1]222        # 确保ξ位于最终区间内223        xi_position = (final_left + final_right) / 2  # 选择区间中点作为ξ224        225        # 极限点226        limit_point = Dot(axes.c2p(xi_position, 0), color=WHITE, radius=0.1)227        limit_label = MathTex(r"\xi").scale(1.2).next_to(limit_point, UP, buff=0.2)228        229        # 分开处理中文和数学符号230        limit_text_ch = Text("存在唯一点", color=WHITE).scale(0.5)231        limit_math = MathTex(r"\xi \in [a_{n}, b_{n}]", color=WHITE).scale(0.7)232        limit_text_n = Text("，n=1,2,...", color=WHITE).scale(0.5)233        234        # 将这些元素组合成一组235        limit_group = VGroup(limit_text_ch, limit_math, limit_text_n)236        limit_group.arrange(RIGHT, buff=0.1)237        limit_group.next_to(interval_desc, DOWN, buff=0.3)238        239        self.play(240            FadeIn(limit_point, scale=1.5),241            Write(limit_label),242            Write(limit_group),243            run_time=1.8244        )245        246        # 强调ξ在最终区间内247        final_interval_with_brackets = VGroup(248            Line(axes.c2p(final_left, 0), axes.c2p(final_right, 0), color=YELLOW_D, stroke_width=5),249            Brace(Line(axes.c2p(final_left, 0), axes.c2p(final_right, 0)), DOWN, color=YELLOW_D)250        )251        252        final_interval_label = MathTex(r"[a_{n},b_{n}]").set_color(YELLOW_D).scale(0.8)253        final_interval_label.next_to(final_interval_with_brackets, DOWN, buff=0.2)254        255        self.play(256            Create(final_interval_with_brackets),257            Write(final_interval_label),258            run_time=1.5259        )260        261        # 创建epsilon说明文本 - 先显示这个262        epsilon_text_ch = Text("存在ε>0", color=WHITE).scale(0.5)263        epsilon_text_ch.next_to(limit_group, DOWN, buff=0.3)264        265        # 先显示文本说明266        self.play(Write(epsilon_text_ch), run_time=1.2)267        268        # 显示ξ的ε-邻域 - 更加明显，改为红色269        epsilon = (final_right - final_left) * 1.5  # 增大邻域范围，使其明显大于[a_n,b_n]270        epsilon_interval = Line(271            axes.c2p(xi_position-epsilon, 0),272            axes.c2p(xi_position+epsilon, 0),273            color=RED,  # 改为红色274            stroke_width=8275        )276        277        # 创建ε-邻域两端的点和标记 - 改为红色278        epsilon_left_dot = Dot(axes.c2p(xi_position-epsilon, 0), color=RED, radius=0.08)279        epsilon_right_dot = Dot(axes.c2p(xi_position+epsilon, 0), color=RED, radius=0.08)280        281        # 放在[a_n,b_n]标签下方 - 改为红色282        epsilon_brace = Brace(epsilon_interval, DOWN, color=RED)283        284        # 显示包含关系 - 将包含符号和标签放在同一行285        inclusion_symbol = MathTex(r"\subset", color=RED).scale(0.9)286        inclusion_symbol.next_to(final_interval_label, RIGHT, buff=0.2)287        288        epsilon_label = MathTex(r"({\xi}-\epsilon,{\xi}+\epsilon)").set_color(RED).scale(0.8)289        epsilon_label.next_to(inclusion_symbol, RIGHT, buff=0.2)  # 放在包含符号右侧290        291        # 然后再显示ε-邻域相关动画292        self.play(293            Create(epsilon_interval),294            FadeIn(epsilon_left_dot),295            FadeIn(epsilon_right_dot),296            Create(epsilon_brace),297            run_time=1.5298        )299        300        # 显示包含关系和标签在同一行301        self.play(302            Write(inclusion_symbol),303            Write(epsilon_label),304            run_time=1.5305        )306        307        # 当n足够大时的矛盾308        final_interval = Line(309            axes.c2p(final_left, 0),310            axes.c2p(final_right, 0),311            color=YELLOW_D,312            stroke_width=5313        )314        315        # 可视化包含关系 - 区间缩小的动画316        self.play(317            final_interval_with_brackets.animate.scale(0.9, about_point=axes.c2p(xi_position, 0)),318            rate_func=there_and_back_with_pause,319            run_time=2.5  # 加长这个动画320        )321        322        # 分开处理中文和数学符号，保持原来的位置323        n_large_ch = Text("当n足够大时，", color=YELLOW_D).scale(0.5)324        n_large_math = MathTex(r"[a_{n},b_{n}] \subset (\xi-\epsilon,\xi+\epsilon)", color=YELLOW_D).scale(0.7)325        n_large_group = VGroup(n_large_ch, n_large_math)326        n_large_group.arrange(RIGHT, buff=0.1)327        n_large_group.next_to(epsilon_text_ch, DOWN, buff=0.3)  # 保持相对位置引用328        329        self.play(330            Write(n_large_group),331            run_time=1.5332        )333        334        # 显示矛盾335        contradiction_ch = Text("矛盾！", color=RED).scale(0.6)336        contradiction_math = MathTex(r"[a_{n},b_{n}]", color=RED).scale(0.7)337        contradiction_ch2 = Text("可被单个开集覆盖!", color=RED).scale(0.6)338        contradiction_group = VGroup(contradiction_ch, contradiction_math, contradiction_ch2)339        contradiction_group.arrange(RIGHT, buff=0.1)340        contradiction_group.next_to(n_large_group, DOWN, buff=0.3)341        342        contradiction = Cross(scale_factor=0.5, stroke_width=6, color=RED)343        contradiction.move_to(final_interval)344        345        self.play(346            Create(contradiction),347            Write(contradiction_group),348            run_time=1.8349        )350        351        # 结论 - 向右移动一个单位并稍微下移352        conclusion = Text("结论：任意开覆盖存在有限子覆盖", color=GREEN).scale(0.6)353        conclusion.to_edge(DOWN, buff=0.3).shift(RIGHT)  # 减小buff值，使其下移一点354        self.play(Write(conclusion), run_time=1.5)355        356        self.wait(2.5)357 358def main():359    import os360    os.system("manim -pql finite_covering_theorem.py FiniteCoveringProof")361 362if __name__ == "__main__":363    main()