Welcome to Math 299. Below you will find some of the rules, definitions, theorems, and declarations that we use in the course. For more detail about these rules see the Course Lecture Notes on the Math 299 Home Page accessible via the Lurch Help menu at the top of the page. (Note that some of the definitions below differ from what is in the lecture notes as they are still in the process of being updated to be consistent with the rules below.)
There are many ways to write the same definition, theorem, or rule in Lurch. For consistency most of the rules below use the same style that imitates the Given-Conclude format used in many high school geometry textbooks.
+
| Imported dependency document | |
| Description: | none |
| Filename: | math/Intro.lurch |
| Source: | the web |
| Auto-refresh: | yes |
This is a basic library of the rules that define a natural deduction style formal system for Propositional Logic. Premises are denoted by 'From' and conclusions by 'Conclude'.
+This is a basic library of the rules that define a natural deduction style formal system for Propositional Logic. Rule premises are denoted as 'Given' and conclusions by 'Conclude'.
Declare ⇔, and, ⇒, or, ¬, and →← to be constants.
+Declare ⇔, and, ⇒, or, ¬, and →← to be constants.
and+
-From W
From V
Conclude W and V
Given
+W
+V
+Conclude W and V
and-
-From W and V
Conclude W
Conclude V
Given
+W and V
+Conclude W
Conclude V
implies+
-From the subproof
Assume W
V
Given
+Assume W
+V
+Conclude W⇒V
+Conclude W⇒V
implies- (modus ponens)
-From W⇒V
From W
Conclude V
Given
+W⇒V
+W
+Conclude V
iff+
-From the two subproofs:
Assume W
V
Given
+ Assume W
V
Assume V
W
Conclude W⇔V
+Conclude W⇔V
iff- (1 of 2)
-From W⇔V
-From W
Conclude V
Given
+W⇔V
+W
+Conclude V
iff- (2 of 2)
-From W⇔V
-From V
+Given
+W⇔V
+V
+Conclude W
or+
-From W
Conclude W or V
Conclude V or W
Given
+W
+Conclude W or V
+Conclude V or W
or- (proof by cases)
-From W or V
From W⇒U
From V⇒U
Conclude U
Given
+W or V
+W⇒U
+V⇒U
+Conclude U
not+ (proof by contradiction)
-From the subproof:
Assume W
→←
Given
+Assume W
+→←
Conclude ¬W
+Conclude not W
not- (proof by contradiction)
-From the subproof:
Assume ¬W
→←
Given
+Assume not W
+→←
+Conclude W
+Conclude W
contradiction+
-From W
From ¬W
Conclude →←
Given
+W
+not W
+Conclude →←
| Imported dependency document | |
| Description: | none |
| Source: | math/Prop-Rules.lurch (web) |
| Auto-refresh: | yes |
| Imported dependency document | |
| Description: | none |
| Filename: | math/Prop-Rules.lurch |
| Source: | the web |
| Auto-refresh: | yes |
This is a basic library of the rules that define a natural deduction style formal system for Predicate Logic with equality. All of the rules from the Propositional Logic library are also available.
forall+
-From the subproof:
Let z (a variable declaration)
+Given
+Let z (a variable declaration)
P(z)
Conclude ∀x.P(x)
+Conclude ∀x.P(x)
forall-
-From ∀x.P(x)
-Conclude P(t)
+Given
+∀x.P(x)
+Conclude P(t)
exists+
-From P(t)
-Conclude ∃x.P(x)
+Given
+P(t)
+Conclude ∃x.P(x)
exists-
-From ∃x.P(x)
-Conclude P(c) for some c (constant declaration)
+Given
+∃x.P(x)
Conclude P(c) for some c (constant declaration)
Substitution Rule:
+Substitution Rule
+Note: For efficiency, most documents will not use this rule unless you explicitly say 'by substitution' in a meaningful expression after the statement you are trying to justify.
From w=v
-From P(w)
-Conclude P(v)
+Substitution
+Given
+w=v
+P(w)
+Conclude P(v)
unique existence-
-From ∃!x.P(x)
-Conclude P(c) and (∀y.(P(y)⇒y=c)) for some c
+Given
+∃!x.P(x)
+Conclude P(c) and (∀y.(P(y)⇒y=c)) for some c
unique existence+
-From P(t)
-From the subproof:
Given
+P(t)
+Let y be such that P(y)
y=t
Conclude ∃!x.P(x)
+Conclude ∃!x.P(x)
| Imported dependency document | |
| Description: | none |
| Source: | math/Pred-Rules.lurch (web) |
| Auto-refresh: | yes |
| Imported dependency document | |
| Description: | none |
| Filename: | math/Pred-Rules.lurch |
| Source: | the web |
| Auto-refresh: | yes |
This is a basic library of the rules that are theorems provable in the system defined by the rules in the Predicate Logic with Equality library.
No additional constants are required.
+No additional constants are required.
The first rule uses '≡' to indicate that it functions effectively as two rules, one where not(not(W)) is given and W is the conclusion and a second rule where W is given and not(not(W)) is the conclusion. The analogous interpretation applies even when there are multiple expressions on the left hand or right hand side of the ≡ symbol.
excluded middle
-W or ¬W
+Theorem (double negative)
+not (not W) ≡ W
double negative
-¬(¬W) ≡ W
+Theorem (excluded middle)
+W or not W
commutativity of 'or'
-From W or V
-Conclude V or W
+Theorem (commutativity of 'or')
+Given
+W or V
+Conclude V or W
associativity of 'or'
-(W or V) or U≡W or (V or U)
+Theorem (associativity of 'or')
+(W or V) or U ≡ W or (V or U)
alternate definition of 'implies'
-W⇒V ≡ ¬W or V
+Theorem (alternate definition of 'implies')
+W⇒V ≡ not W or V
alternate or-
-From W or V
-From ¬W
-Conclude V
+Theorem (alternate or-)
+Given
+W or V
+not W
+Conclude V
alternate or-
-From W or V
-From ¬V
+Theorem (alternate or-)
+Given
+W or V
+not V
+Conclude W
negated implication
-¬(W⇒V) ≡ W and ¬V
+Theorem (negated implication)
+not (W⇒V) ≡ W, not V
contrapositive
-W⇒V ≡ ¬V⇒¬W
+Theorem (contrapositive)
+W⇒V ≡ not V⇒not W
DeMorgan's Law
-¬(W and V) ≡ ¬W or ¬V
+Theorem (DeMorgan's Law)
+not (W and V) ≡ not W or not V
DeMorgan's Law
-¬(W or V) ≡ ¬W and ¬V
+Theorem (DeMorgan's Law)
+not (W or V) ≡ not W and not V
Anything follows from a contradiction
-From →←
-Conclude W
+Theorem (anything follows from a contradiction)
+Given
+→←
+Conclude W
| Imported dependency document | |
| Description: | none |
| Source: | math/Logic-theorems-Rules.lurch (web) |
| Auto-refresh: | yes |
Declare 0, σ, +, ⋅, and ≤ to be constants.
+Declare 0, σ, +, ⋅, and ≤ to be constants.
(We don't need axioms N0 or N1.)
-N0: 0 is a natural number.
-N1: For all natural numbers n, the successor of n is a natural number.
+(We don't need axioms N0 or N1 because in this context the domain of discourse is the set of natural numbers.)
+Axiom N0: 0 is a natural number.
+Axiom N1: For all natural numbers n, the successor of n is a natural number.
N2 (successor is injective): If σ(m)=σ(n) then m=n
+Axiom N2 (successor is injective)
+Given
+σ(m)=σ(n)
+Conclude m=n
N3 (zero is first): 0=σ(n)
+Axiom N3 (zero is first)
+0=σ(n)
N4 (induction):
-If P(0) (the Base Case)
-and we have the subproof (the Inductive step)
+Axiom N4 (induction)
Let k be such that P(k)
+Given
+P(0) (base case)
+Let k be such that P(k) (inductive hypothesis)
P(σ(k))
then we can conclude ∀n.P(n)
+Conclude ∀n.P(n)
A0: n+0=n
+Axiom A0 (base case for addition)
+n+0=n
A1: m+σ(n)=σ(m+n)
+Axiom A1 (recursion for addition)
+m+σ(n)=σ(m+n)
M0: n⋅0=0
+Axiom M0 (base case for multiplication)
+n⋅0=0
M1: m⋅σ(n)=m+m⋅n
+Axiom M1 (recursion for multiplication)
+m⋅σ(n)=m+m⋅n
I: m≤n≡∃k.m+k=n
+Axiom I (inequality)
+m≤n ≡ ∃k.m+k=n
| Imported dependency document | |
| Description: | none |
| Source: | math/Peano-Rules.lurch (web) |
| Auto-refresh: | yes |
This library contains some definitions from Number Theory. It includes all of the rules in the Peano Axioms library.
Declare 1, 2, 3, 4, 5, <, is, ∣, prime, even, and odd
+Declare 1, 2, 3, 4, 5, <, is, ∣, prime, even, and odd
Base ten digits
1=σ(0)
5=σ(4)
Less than: m<n ≡ m≤n & m=n
+Less than
+m<n ≡ m≤n , m=n
Divides: If m∣n then n=k⋅m for some k.
+Prime
+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.
Divides: If n=k⋅m then m∣n.
+Divides: If m∣n then n=k⋅m for some k.
Prime: n is prime ≡ 1<n & ¬(∃k.(1<k and k<n) and k∣n)
+Divides: If n=k⋅m then m∣n.
Odd: n is odd ≡ ¬n is even
+Odd
+n is odd ≡ not n is even
a=b=c=d
-
(entered as a=b=c=d). It automates the application of the substitution and reflexive rules of equality, its derived properties of symmetry and transitivity, and checks each pair in the chain for both direct equality, and equality via a single substitution. This topic includes everything from the Number Theory topic.
(entered as a=b=c=d). It automates the application of the substitution and reflexive rules of equality, the derived properties of symmetry and transitivity, and checks each pair in the chain for both direct equality, and equality via a single substitution. This topic includes everything from the Number Theory topic.
Equations Rule: EquationsRule
+Equations Rule
+EquationsRule
Theorem (alternate definition of 𝜎): σ(n)=n+1
+Theorem (alternate definition of 𝜎)
+σ(n)=n+1
Theorem (commutativity of addition): m+n=n+m
+Theorem (commutativity of addition)
+m+n=n+m
Theorem (associativity of addition): (m+n)+p=m+(n+p)
+Theorem (associativity of addition)
+(m+n)+p=m+(n+p)
Theorem (addition of zero on the left): 0+n=n
+Theorem (addition of zero on the left)
+0+n=n
Theorem (multiplication by zero on the left): 0⋅n=0
+Theorem (multiplication by zero on the left)
+0⋅n=0
Theorem (identity of multiplication): n⋅1=n
+Theorem (identity of multiplication)
+n⋅1=n
Theorem (identity of multiplication): 1⋅n=n
+Theorem (identity of multiplication)
+1⋅n=n
Theorem (commutativity of multiplication): m⋅n=n⋅m
+Theorem (commutativity of multiplication)
+m⋅n=n⋅m
Theorem(associativity of multiplication): (m⋅n)⋅p=m⋅(n⋅p)
+Theorem(associativity of multiplication)
+(m⋅n)⋅p=m⋅(n⋅p)
Theorem (distributive property of ⋅ over +): m⋅(n+p)=m⋅n+m⋅p
+Theorem (distributive property of ⋅ over +)
+m⋅(n+p)=m⋅n+m⋅p
Theorem (distributive property of ⋅ over +): (n+p)⋅m=n⋅m+p⋅m
+Theorem (distributive property of ⋅ over +)
+(n+p)⋅m=n⋅m+p⋅m
Once we have defined the natural numbers we can use them to define sequences, both finite and infinite. They can be defined explicitly or recursively. In this topic we define a few well known recursive sequences. All of the rules, definitions, and theorems in the Number Theory Theorems topic are also available here.
Declare Sum, F, factorial, multinomial, choose, and ∧ to be constants.
+Declare Sum, F, factorial, multinomial, choose, and ∧ to be constants.
Summation:
k=0∑0P(k)=P(0)
+Summation (base case)
+k=0∑0P(k)=P(0)
k=0∑σ(n)P(k)=P(σ(n))+k=0∑nP(k)
+Summation (recursion)
+k=0∑σ(n)P(k)=P(σ(n))+k=0∑nP(k)
Natural Number Exponentiation:
z0=1
+Natural Number Exponentiation (base case)
+z0=1
zσ(n)=z⋅zn
+Natural Number Exponentiation (recursion)
+zσ(n)=z⋅zn
Factorial:
+
0!=1
+Factorial (base case)
+0!=1
σ(n)!=σ(n)⋅n!
+Factorial (recursion)
+σ(n)!=σ(n)⋅n!
Fibonacci Numbers:
+
Fibonacci Numbers (base cases)
F0=1
F1=1
Fn+2=Fn+1+Fn
+Fibonacci Numbers (recursion)
+Fn+2=Fn+1+Fn
Multinomial coefficients:
+
(m,0)=1
+Multinomial coefficients (base case)
+(m,0)=1
(0,n)=1
+Multinomial coefficients (base case)
+(0,n)=1
Multinomial coefficients (recursion)
(σ(m),σ(n))=(σ(m),n)+(m,σ(n))
Binomial Coefficients:
+
(n+mm)=(n,m)
+Binomial Coefficients
+(n+mm)=(n,m)
| Imported dependency document | |
| Description: | none |
| Source: | math/Sequences-Rules.lurch (web) |
| Auto-refresh: | yes |
We can now define a formal system for the Real Numbers. This library includes all of the rules, definitions, and axioms from the Sequences library.
Declare < and − (the negative sign) to be constants.
+Declare − (the negative sign) to be constants.
We include here all of the rules of inference for the real numbers except for the completeness axiom, which is beyond the scope of this course.
x+(−x)=0
−x+x=0
The next two axioms (and several more below) are already available as theorems about the natural numbers, so we don't repeat them here. The only difference is now we have changed our domain of discourse from the natural numbers to the real numbers.
Commutativity of addition: x+y=y+x
+Commutativity of addition
+x+y=y+x
Associativity of addition: (x+y)+z=x+(y+z)
+Associativity of addition
+(x+y)+z=x+(y+z)
Multiplicative identity 1=0
+Multiplicative identity
+1=0
Multiplicative identity
@@ -589,17 +717,17 @@Multiplicative inverse
-if x=0 then
-x⋅x−=1
-(x−)⋅x=1
+if x=0 then x⋅x−=1 and (x−)⋅x=1
Commutativity of multiplication: x⋅y=y⋅x
+Commutativity of multiplication
+x⋅y=y⋅x
Associativity of multiplication: (x⋅y)⋅z=x⋅(y⋅z)
+Associativity of multiplication
+(x⋅y)⋅z=x⋅(y⋅z)
< is irreflexive: ¬(x<x)
+< is irreflexive
+not (x<x)
< is transitive: If x<y and y<z then x<z.
+< is transitive
+If x<y and y<z then x<z.
Trichotomy: x=y or (x<y or y<x)
+Trichotomy
+x=y or (x<y or y<x)
Distributivity: x⋅(y+z)=x⋅y+x⋅z
+Distributivity
+x⋅(y+z)=x⋅y+x⋅z
Translation: If x<y then x+z<y+z
+Translation
+If x<y then x+z<y+z
Product of positives: if 0<x and 0<y then 0<x⋅y
+Product of positives
+If 0<x and 0<y then 0<x⋅y
| Imported dependency document | |
| Description: | none |
| Source: | math/Reals-Rules.lurch (web) |
| Auto-refresh: | yes |
Declare ∈, ⊆, ∩, ∪, ′, ∖, P, ×, set, tuple, Union, Intersect, and setbuilder to be constants.
Empty set: x∉{}
+Empty set
+x∉{}
Nonempty: A={} iff ∃x.x∈A
+Nonempty
+A={} ≡ ∃x.x∈A
Finite set notation:
x∈{a} iff x=a
+x∈{a} ≡ x=a
x∈{a,b} iff x=a or x=b
+x∈{a,b} ≡ x=a or x=b
x∈{a,b,c} iff x=a or (x=b or x=c)
+x∈{a,b,c} ≡ x=a or (x=b or x=c)
x∈{a,b,c,d} iff x=a or (x=b or (x=c or x=d))
+x∈{a,b,c,d} ≡ x=a or (x=b or (x=c or x=d))
Set builder: x∈{z:P(z)} iff P(x)
+Set builder
+x∈{z:P(z)} ≡ P(x)
Subset-:
From A⊆B
From x∈A
-x∈B
+Subset-:
+Given
+A⊆B
+x∈A
+Conclude x∈B
Subset+:
Given
+Let x∈A
x∈B
A⊆B
+Conclude A⊆B
Set equality:
Let a∈A
+Given
+Let a∈A
a∈B
Let b∈B
+Let b∈B
b∈A
A=B
Set equality: A=B iff A⊆B and B⊆A
+Set equality
+A=B ≡ A⊆B , B⊆A
Powerset: A∈P(B) iff A⊆B
+Powerset
+A∈P(B) ≡ A⊆B
Intersection: x∈A∩B iff x∈A and x∈B
+Intersection
+x∈A∩B ≡ x∈A , x∈B
Union: a∈A∪B iff x∈A or x∈B
+Union
+a∈A∪B ≡ x∈A or x∈B
Relative Complement: x∈A∖B iff x∈A and x∉B
+Relative Complement
+x∈A∖B ≡ x∈A , x∉B
Complement: x∈B′ iff x∉B
+Complement
+x∈B′ ≡ x∉B
Ordered tuple:
(pair): ⟨a,b⟩=⟨c,d⟩ iff a=c and b=d
+(pair)
+⟨a,b⟩=⟨c,d⟩ ≡ a=c , b=d
(triple): ⟨a,b,c⟩=⟨d,e,f⟩ iff a=d, b=e, and c=f
+(triple)
+⟨a,b,c⟩=⟨d,e,f⟩ ≡ a=d, b=e, c=f
Cartesian product
(pair): If z∈A×B then z=⟨a,b⟩ and (a∈A and b∈B) for some a and b.
+(pair): If z∈A×B then z=⟨a,b⟩ and (a∈A and b∈B) for some a and b.
(pair): If ⟨a,b⟩∈A×B then a∈A and b∈B.
@@ -758,29 +915,29 @@(triple): If ⟨a,b,c⟩∈A×B×C then a∈A and b∈B and c∈C.
If x∈i∈I⋃A(i) then x∈A(j) for some j∈I.
+Indexed Union: If x∈i∈I⋃A(i) then x∈A(j) for some j∈I.
If j∈I and x∈A(j) then x∈i∈I⋃A(i)
+Indexed Union: If j∈I and x∈A(j) then x∈i∈I⋃A(i)
If x∈i∈I⋂A(i) and j∈I then x∈A(j).
+Indexed Intersection: If x∈i∈I⋂A(i) and j∈I then x∈A(j).
From the subproof:
+Indexed Intersection
Given
+Let j∈I
x∈A(j)
we can conclude x∈i∈I⋂A(i).
+Conclude x∈i∈I⋂A(i).
| Imported dependency document | |
| Description: | none |
| Source: | math/Sets-Rules.lurch (web) |
| Auto-refresh: | yes |
| Imported dependency document | |
| Description: | none |
| Source: | math/Sets-Rules.lurch (web) |
| Auto-refresh: | yes |
We now define a formal system for defining elementary concepts related to functions. This library includes all of the rules, definitions, and axioms from the Sets library.
@@ -800,18 +957,22 @@Function Equality: If f:A→B and g:A→B
-and we have the subproof:
+Function Equality
+Given
+f:A→B
+g:A→B
Let x∈A
f(x)=g(x)
then f=g.
+Conclude f=g.
Image of a Set: If x∈S then f(x)∈f(S).
+Image of a Set: If x∈S then f(x)∈f(S)
Image of a Set: if y∈f(S) then y=f(x) for some x∈S.
@@ -819,83 +980,137 @@Identity map: idA:A→A.
+Identity map
+idA:A→A
Identity map: idA(x)=x.
+Identity map
+idA(x)=x.
Composition: If f:A→B and g:B→C then g∘f:A→C
+Composition
+Given
+f:A→B
+g:B→C
+Conclude g∘f:A→C
Composition: (g∘f)(x)=g(f(x))
+Composition
+(g∘f)(x)=g(f(x))
Injective: If f is injective and f(x)=f(y) then x=y.
+Injective
+Given
+f is injective
+f(x)=f(y)
+Conclude x=y
Injective: From the subproof
+Injective:
Given
+Let x and y be such that f(x)=f(y)
x=y
we can conclude that f is injective.
+Conclude f is injective
Surjective: If f:A→B, f is surjective, and b∈B then b=f(a) for some a∈A.
+Surjective
+Given
+f:A→B
+f is surjective
+b∈B
+Conclude b=f(a) for some a∈A.
Surjective:
-If f:A→B and we have the subproof
Given
+If f:A→B
+Let b∈B
b=f(a)
then f is surjective.
+Conclude f is surjective
Bijective: f is bijective iff f is injective and f is surjective
+Bijective
+f is bijective ≡ f is injective , f is surjective
Inverse map: If f:A→B and f is bijective thenf−1:B→A
+Inverse map
+Given
+f:A→B
+f is bijective
+Conclude f−1:B→A
Inverse map: If f:A→B and f is bijective then f−1(f(a))=a.
+Inverse map
+Given
+f:A→B
+f is bijective
+Conclude f−1(f(a))=a
Inverse map: If f:A→B and f is bijective then f(f−1(b))=b.
+Inverse map
+Given
+f:A→B
+f is bijective
+Conclude f(f−1(b))=b
Inverse image: a∈finv(S) iff f(a)∈S
+Inverse image
+a∈finv(S) ≡ f(a)∈S
Inverse image: If f:A→B and U⊆B then finv(U)⊆A
+Inverse image
+Given
+f:A→B
+U⊆B
+Conclude finv(U)⊆A
| Imported dependency document | |
| Description: | none |
| Source: | math/Functions-Rules.lurch (web) |
| Auto-refresh: | yes |
| Imported dependency document | |
| Description: | none |
| Source: | math/Functions-Rules.lurch (web) |
| Auto-refresh: | yes |
Topology is a branch of mathematics that studies properties of continuous functions and geometric properties that they preserve. We begin by defining a topological space.
Definition: The pair ⟨X,τ⟩ is a topological space if and only if it has the following properties.
@@ -921,30 +1136,39 @@Let A and B be such that A∈τ and B∈τ
A∩B∈τ
+5. and this subproof
Let I be such that I⊆τ
A∈I⋃A∈τ
+we can conclude that ⟨X,τ⟩ is a topologial space.
+Topological Space (minus) Rules:
1. If ⟨X,τ⟩ is a topologial space and U∈τ then U⊆X.
+2. If ⟨X,τ⟩ is a topologial space then {}∈τ.
+3. If ⟨X,τ⟩ is a topologial space then X∈τ.
+4. If ⟨X,τ⟩ is a topologial space, A∈τ, and B∈τ then A∩B∈τ
+5. If ⟨X,τ⟩ is a topologial space and I⊆τ then A∈I⋃A∈τ.
+We can also derive 'plus' and 'minus' rules for the concept of continuity.
Let U∈τ
finv(U)∈τ
+then f is continuous.
+Continuous: If ⟨X,τ⟩ is a topologial space, f:X→X, f is continuous, and U∈τ then finv(U)∈τ.
+Using these rules (and those from the Show/hide rules menu) 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.
+Proof:
Suppose f:X→X, g:X→X, f is continuous, and g is continuous.
-g∘f:X→X
+Then g∘f:X→X by the definition of composition. To prove g∘f is continuous, we must show that the inverse image of any open set is open.
Let U∈τ
-ginv(U)∈τ
-finv(ginv(U))∈τ
-+
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).
Let x∈finv(ginv(U))
-f(x)∈ginv(U)
-g(f(x))∈U
-g(f(x))=(g∘f)(x)
-(g∘f)(x)∈U by substitution
-x∈(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.
+
Let y∈(g∘f)inv(U)
-(g∘f)(y)∈U
-(g∘f)(y)=g(f(y))
-g(f(y))∈U by substitution
-f(y)∈ginv(U)
-y∈finv(ginv(U))
+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)).
+-
finv(ginv(U))=(g∘f)inv(U)
-(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.
+g∘f is continuous
+Therefore g∘f is continuous.
□
+