From aaf3ae27fdaee9346d2f7807ea1519399ede033a Mon Sep 17 00:00:00 2001 From: Ken Monks Date: Fri, 13 Dec 2024 12:12:31 -0700 Subject: [PATCH] Improving the topology example. --- math/examples/D. Topo-logical.lurch | 29 ++++++++++++---------- math/examples/Topo-logical - soln.lurch | 33 ++++++++++++++----------- 2 files changed, 34 insertions(+), 28 deletions(-) diff --git a/math/examples/D. Topo-logical.lurch b/math/examples/D. Topo-logical.lurch index d06945ef..98bc6f91 100644 --- a/math/examples/D. Topo-logical.lurch +++ b/math/examples/D. Topo-logical.lurch @@ -4,7 +4,7 @@ @@ -140,7 +140,7 @@

Given

-

 Assume W
V

+

Assume W
V

Assume V
W

@@ -507,7 +507,7 @@

Prime 

-

n is prime    ≡   1<n  ,  not (∃k.(1<k and k<n) and k∣n)

+

n is prime    ≡   1<n  ,  not (∃k.(1<k and k<n) and k∣n)

We can also write rules using the 'If-then' style as an alternative to the 'Given-Conclude' style used in this document's context.  We will use this form from now on for any rule that does not contain a subproof premise, or the ≡ rule shorthand.

@@ -527,8 +527,7 @@
-

Odd

-

n is odd    ≡    not n is even

+

Odd:  n is odd    ≡    n is not even

@@ -544,7 +543,12 @@

EquationsRule

-

 

+

We can also add some convenient rules to avoid the need for explicitly citing 'by substitution' in common situations.

+
+

Substitution for is: If x=y and x is P then y is P.

+
+

 

+

 

Imported dependency document
Description:none
Source:math/Equations-Rules.lurch (web)
Auto-refresh:yes

Number Theory Theorems

Once we have proven theorems it is convenient to add the most useful ones as new rules rather than reproving them from scratch each time we need to use one.  This library contains some of the most useful theorems about the natural numbers that can be proven using the Peano Axioms.  All of the rules from the Number Theory library are also available.

@@ -1120,11 +1124,11 @@
  • if A∈τ and B∈τ then A∩B∈τ 
  • if I⊆τ then A∈I⋃​A∈τ.
    • -

    We say that the set τ is a topology on the set X. In what follows we will restrict to a single topological space for simplicity. So let's assume ⟨X,τ⟩ is a topological space in what follows.  Then we have the following simplified definitions.

    +

    We say that the set τ is a topology on the set X. In this situation we have the following simplified definitions.

    Definition: A⊆X is open if and only if A∈τ.

    Definition: A⊆X is closed if and only if A′ is open.

    Definition:  The function f:X→X is continuous if and only if the inverse image of every open set is open.

    -

    We can derive some rules from these definitions. First, declare open, closed, topological space, and τ to be constants. 

    +

    Let's declare open, closed, topological space, and τ to be constants. We can then write down some rules from these definitions.

    Following Gentzen, we can define plus and minus rules for topological spaces.

    Topological space (plus):  Let X and τ be sets. If we know that

    @@ -1171,15 +1175,14 @@

    then f is continuous.

    -

    Continuous: If ⟨X,τ⟩ is a topological space, f:X→X, f is continuous, and U∈τ then finv(U)∈τ.

    +

    Definition of Continuous: If ⟨X,τ⟩ is a topological space, f:X→X, f is continuous, and U∈τ then finv(U)∈τ.

    -

    Using these rules (and those from the Show/hide context menu) prove the following theorem.

    +

    Using these definitions we can prove the following theorem.

    -

    Theorem (composition of continuous is continuous): 

    -

    If f:X→X, g:X→X, f is continuous, and g is continuous then g∘f is continuous.

    +

    Theorem (composition of continuous is continuous): Suppose ⟨X,τ⟩ is a topological space, f:X→X, g:X→X, f is continuous, and g is continuous then g∘f is continuous.

    -
    +

    Proof:

     

    □

    diff --git a/math/examples/Topo-logical - soln.lurch b/math/examples/Topo-logical - soln.lurch index 00add4e1..80a3d02c 100644 --- a/math/examples/Topo-logical - soln.lurch +++ b/math/examples/Topo-logical - soln.lurch @@ -4,7 +4,7 @@
    @@ -140,7 +140,7 @@

    Given

    -

     Assume W
    V

    +

    Assume W
    V

    Assume V
    W

    @@ -507,7 +507,7 @@

    Prime 

    -

    n is prime    ≡   1<n  ,  not (∃k.(1<k and k<n) and k∣n)

    +

    n is prime    ≡   1<n  ,  not (∃k.(1<k and k<n) and k∣n)

    We can also write rules using the 'If-then' style as an alternative to the 'Given-Conclude' style used in this document's context.  We will use this form from now on for any rule that does not contain a subproof premise, or the ≡ rule shorthand.

    @@ -527,8 +527,7 @@
    -

    Odd

    -

    n is odd    ≡    not n is even

    +

    Odd:  n is odd    ≡    n is not even

    @@ -544,7 +543,12 @@

    EquationsRule

    -

     

    +

    We can also add some convenient rules to avoid the need for explicitly citing 'by substitution' in common situations.

    +
    +

    Substitution for is: If x=y and x is P then y is P.

    +
    +

     

    +

     

    Imported dependency document
    Description:none
    Source:math/Equations-Rules.lurch (web)
    Auto-refresh:yes

    Number Theory Theorems

    Once we have proven theorems it is convenient to add the most useful ones as new rules rather than reproving them from scratch each time we need to use one.  This library contains some of the most useful theorems about the natural numbers that can be proven using the Peano Axioms.  All of the rules from the Number Theory library are also available.

    @@ -1120,11 +1124,11 @@
  • if A∈τ and B∈τ then A∩B∈τ 
  • if I⊆τ then A∈I⋃​A∈τ.
    • -

    We say that the set τ is a topology on the set X. In what follows we will restrict to a single topological space for simplicity. So let's assume ⟨X,τ⟩ is a topological space in what follows.  Then we have the following simplified definitions.

    +

    We say that the set τ is a topology on the set X. In this situation we have the following simplified definitions.

    Definition: A⊆X is open if and only if A∈τ.

    Definition: A⊆X is closed if and only if A′ is open.

    Definition:  The function f:X→X is continuous if and only if the inverse image of every open set is open.

    -

    We can derive some rules from these definitions. First, declare open, closed, topological space, and τ to be constants. 

    +

    Let's declare open, closed, topological space, and τ to be constants. We can then write down some rules from these definitions.

    Following Gentzen, we can define plus and minus rules for topological spaces.

    Topological space (plus):  Let X and τ be sets. If we know that

    @@ -1176,23 +1180,22 @@

    Using these definitions we can prove the following theorem.

    -

    Theorem (composition of continuous is continuous): 

    -

    If f:X→X, g:X→X, f is continuous, and g is continuous then g∘f is continuous.

    +

    Theorem (composition of continuous is continuous): Suppose ⟨X,τ⟩ is a topological space, f:X→X, g:X→X, f is continuous, and g is continuous then g∘f is continuous.

    -

    Proof:

    -

    Suppose f:X→X, g:X→X, f is continuous, and g is continuous. Then g∘f:X→X by the definition of composition.  To prove g∘f is continuous, we must now show that the inverse image of any open set is open.

    +

    Proof:

    +

    Suppose ⟨X,τ⟩ is a topological space, f:X→X, g:X→X, f is continuous, and g is continuous. Then g∘f:X→X by the definition of composition.  To prove g∘f is continuous, we must now show that the inverse image of any open set is open.

    So let U∈τ be an arbitrary open set.  Then ginv(U)∈τ by the continuity of g, andfinv(ginv(U))∈τ by the continuity of f. Thus, it suffices to show that

    finv(ginv(U))=(g∘f)inv(U).

    -

    To prove that, first let x∈finv(ginv(U)).  Then by the definition of inverse image we have f(x)∈ginv(U) and g(f(x))∈U. But g(f(x))=(g∘f)(x), so (g∘f)(x)∈U by substitution. Thus, x∈(g∘f)inv(U) as desired.

    +

    To prove that, first let x∈finv(ginv(U)).  Then by the definition of inverse image we have f(x)∈ginv(U) and g(f(x))∈U. But g(f(x))=(g∘f)(x), so (g∘f)(x)∈U by substitution. Thus, x∈(g∘f)inv(U) as desired.

    -

    Conversely, let y∈(g∘f)inv(U). Then (g∘f)(y)∈U. But once again we have(g∘f)(y)=g(f(y)) and so g(f(y))∈U by substitution.  Then f(y)∈ginv(U) and

    +

    Conversely, let y∈(g∘f)inv(U). Then (g∘f)(y)∈U. But once again we have(g∘f)(y)=g(f(y)) and so g(f(y))∈U by substitution.  Then f(y)∈ginv(U) and

    y∈finv(ginv(U)).

    -

    Thus we have shown that finv(ginv(U))=(g∘f)inv(U), and so (g∘f)inv(U)∈τ by substitution.

    +

    Thus we have shown that finv(ginv(U))=(g∘f)inv(U), and so (g∘f)inv(U)∈τ by substitution.

    Therefore g∘f is continuous.

    □