avewright/proofwiki-math huggingface dataset:
Theorem: Mapping at Element is Supremum of Compact Elements implies Mapping is Increasing

Let $\struct {S, \vee_1, \wedge_1, \preceq_1}$ be a lattice.
Let $\struct {T, \vee_2, \wedge_2, \preceq_2}$ be a complete lattice.
Let $f: S \to T$ be a mapping such that
:$\forall x \in S: \map f x = \sup \leftset {\map f w : w \in S \land w \preceq_1 x \land w}$ is compact$\rightset{}$
Then $f$ is increasing.

Proof:
Let $x, y \in S$ such that
:$x \preceq_1 y$
By Compact Closure is Increasing:
:$x^{\mathrm {compact} } \subseteq y^{\mathrm {compact} }$
By Image of Subset under Mapping is Subset of Image:
:$f \sqbrk {x^{\mathrm {compact} } } \subseteq f \sqbrk {y^{\mathrm {compact} } }$
By assumption:
:$\map f x = \sup \leftset {\map f w: w \in S \land w \preceq_1 x \land w}$ is compact$\rightset{}$
and
:$\map f y = \sup \leftset {\map f w: w \in S \land w \preceq_1 y \land w}$ is compact$\rightset{}$
By definitions of image of set and compact closure:
:$\map f x = \map \sup {f \sqbrk {x^{\mathrm {compact} } } }$
and
:$\map f y = \map \sup {f \sqbrk {y^{\mathrm {compact} } } }$
Thus by Supremum of Subset and definition of complete lattice:
:$\map f x \preceq_2 \map f y$
{{qed}}
Theorem: Equivalence of Definitions of Compatible Atlases

Let $M$ be a topological space.
Let $\mathscr F, \mathscr G$ be $d$-dimensional atlases of class $C^k$ on $M$.
{{TFAE|def = Compatible Atlases}}

Proof:
=== Definition $1$ implies Definition $2$ ===
Follows immediately from the definition of $C^k$-atlas.
{{qed|lemma}}
Theorem: Atlas is Contained in Unique Maximal Atlas

Let $M$ be a topological space.
Let $A$ be a $d$-dimensional atlas of class $C^k$.
Then $A$ is contained in a unique maximal atlas of class $C^k$.

Proof:
=== Existence ===
Theorem: Locally Euclidean iff has C0-Atlas

Let $M$ be a topological space.
{{TFAE}}
:$(1): \quad$ $M$ is locally euclidean.
:$(2): \quad$ There exists a $C^0$-atlas on $M$.

Proof:
{{ProofWanted|use Transition Mapping between Charts is Homeomorphism}}
Category:Atlases
Category:Topological Spaces
Category:Locally Euclidean Spaces
m4xz9zlgb5n2ga8wq14uqorb3lyv3n4
Theorem: Differentiable Structure Contains Unique Maximal Atlas

Let $M$ be a topological space.
Let $k$ and $d$ be natural numbers.
Let $S$ be a $d$-dimensional differentiable structure of class $C^k$ on $M$.
Then $S$ contains a unique maximal $C^k$-atlas.

Proof:
{{ProofWanted}}
Category:Topological Manifolds
Category:Maximal Atlases
alrzbmnkm9a5a5mei0vpkxszoneg71r
Theorem: Consecutive Integers whose Product is Primorial

The following primorials can be expressed as the product of consecutive integers:
:$2, 6, 30, 210, 510 \, 510$
{{OEIS|A161620}}
No others are known.
The corresponding indices of those primorials are:
:$2, 3, 5, 7, 17$
{{OEIS|A215658}}
The corresponding values of $n$ such that $p\# = \paren {n - 1} n$ are:
:$2, 3, 6, 15, 715$
{{OEIS|A215659}}

Proof:
{{begin-eqn}}
{{eqn | l = 2 \#
      | r = 1 \times 2
}}
{{eqn | r = 2
}}
{{eqn | l = 3 \#
      | r = 2 \times 3
}}
{{eqn | r = 6
}}
{{eqn | l = 5 \#
      | r = 2 \times 3 \times 5
}}
{{eqn | r = 5 \times \paren {2 \times 3}
}}
{{eqn | r = 5 \times 6
}}
{{eqn | r = 30
}}
{{eqn | l = 7 \#
      | r = 2 \times 3 \times 5 \times 7
}}
{{eqn | r = \paren {2 \times 7}  \times \paren {3 \times 5}
}}
{{eqn | r = 14 \times 15
}}
{{eqn | r = 210
}}
{{eqn | l = 17 \#
      | r = 2 \times 3 \times 5 \times 7 \times 11 \times 13 \times 17
}}
{{eqn | r = \paren {2 \times 3 \times 7 \times 17}  \times \paren {5 \times 11 \times 13}
}}
{{eqn | r = 714 \times 715
}}
{{eqn | r = 510 \, 510
}}
{{end-eqn}}
{{qed}}
Theorem: Implicit Function Theorem

{{:Implicit Function Theorem/Real Functions}}

Proof:
==== Reduction to $\tuple {a, b} = \tuple {0, 0}$ ====
We may assume $\tuple {a, b} = \tuple {0, 0}$.
{{explain|why}}
Define:
:$F: \Omega \to \R^k: \map F {x, y} = y - \map {D_2 \map f {a, b}^{-1} } {\map f {x, y} }$
By Linear Function is Continuous, $D_2 \map f {a, b}^{-1}$ is continuous on $\R^k$.
Thus $F$ is continuous on $\Omega$.
==== $F$ is locally a uniform contraction ====
Let $r_1 > 0$ such that the open ball $\map B {0, r_1} \subseteq \Omega$.
We have, for $\tuple {x, y_1}, \tuple {x, y_2} \in \map B {0, r_1}$, by the Mean Value Inequality:
:$\ds \norm {\map F {x, y_2} - \map F {x, y_1} } \le \sup_{y \mathop \in \closedint {y_1} {y_2} } \norm {D_2 \map F {x, y} } \cdot \norm {y_2 - y_1}$
We have, for $\tuple {x, y} \in \Omega$:
:$D_2 \map F {x, y} = I - \paren {D_2 \map F {0, 0} }^{-1} \circ D_2 \map F {x, y}$
where $I$ is the identity mapping.
Thus $D_2 F$ is continuous in $\Omega$.
By definition, $D_2 \map F {0, 0} = 0$.
By continuity, there exists $r_2 > 0$ such that:
:$\norm {D_2 \map F {x, y} } \le \dfrac 1 2$ for $\norm {\tuple {x, y} } \le r_2$
From the above inequality, $F$ is a uniform contraction mapping on the open ball $\map B {0, r_2}$ for the Lipschitz Constant $\dfrac 1 2$.
==== Constructing a stable neighborhood ====
We have, for $x, y \in \map {\overline B} {0, r_2}$:
{{begin-eqn}}
{{eqn | l = \norm {\map F {x, y} }
      | o = \le
      | r = \norm {\map F {x, y} - \map F {x, 0} } + \norm {\map F {x, 0} }
      | c = {{NormAxiomVector|3}}
}}
{{eqn | o = \le
      | r = \frac 1 2 \norm y + \norm {\map F {x, 0} }
      | c = Definition of $r_2$
}}
{{end-eqn}}
Because $\map F {0, 0} = 0$ and $F$ is continuous, there exists $r_3>0$ such that $\norm {\map F {x, 0} } \le \dfrac {r_2} 2$.
Then:
:$\norm {\map F {x, y} } \le r_2$ for $\norm y \le r_2$
and:
:$\norm x \le r_3$
Thus the restriction of $F$ to $\map B {0, r_3} \times \map {\overline B} {0, r_2}$ is a uniform contraction:
:$F: \map B {0, r_3} \times \map {\overline B} {0, r_2} \to \map {\overline B} {0, r_2}$
==== Applying the Uniform Contraction Theorem ====
By Subspace of Complete Metric Space is Closed iff Complete, $\map {\overline B} {0, r_2}$ is complete.
By the Uniform Contraction Mapping Theorem, there exists a unique mapping $g: \map B {0, r_3} \to \map {\overline B} {0, r_2}$ such that $\map F {x, \map g x} = \map g x$.
Moreover, $g$ is continuous.
A mapping $h: \map B {0, r_3} \to \map {\overline B} {0, r_2}$ satisfies $\map F {x, \map h x} = \map h x$ {{iff}} it satisfies $\map {D_2 \map f {a, b}^{-1} } {\map f {x, \map h x} } = 0$ {{iff}} it satisfies $\map f {x, \map h x} = 0$, because $D_2 \map f {a, b}^{-1}$ is invertible.
Thus $g$ is the unique mapping $g: \map B {0, r_3} \to \map {\overline B} {0, r_2}$ such that $\map f {x, \map g x} = 0$.
{{qed}}
Theorem: Uniform Contraction Mapping Theorem

Let $M$ and $N$ be metric spaces.
Let $M$ be complete.
Let $f : M \times N \to M$ be a continuous uniform contraction.
Then for all $t \in N$ there exists a unique $\map g t \in M$ such that $\map f {\map g t, t} = \map g t$, and the mapping $g: N \to M$ is continuous.

Proof:
For every $t\in N$, the mapping:
:$f_t: M \to M : x \mapsto \map f {x, t}$ is a contraction.
By the Banach Fixed-Point Theorem, there exists a unique $\map g t \in M$ such that $\map {f_t} {\map g t} = \map g t$.
We show that $g$ is continuous.
Let $K < 1$ be a uniform Lipschitz constant for $f$.
Let $s, t \in N$.
Then
{{begin-eqn}}
{{eqn | l = \map d {\map g s, \map g t}
      | r = \map d {\map f {\map g s, s}, \map f {\map g t, t} }
      | c = Definition of $g$
}}
{{eqn | o = \le
      | r = \map d {\map f {\map g s, s}, \map f {\map g t, s} } + \map d {\map f {\map g t, s}, \map f {\map g t, t} }
      | c = {{Defof|Metric}}
}}
{{eqn | o = \le
      | r = K \cdot \map d {\map g s, \map g t} + \map d {\map f {\map g t, s}, \map f {\map g t, t} }
      | c = $f$ is a uniform contraction
}}
{{end-eqn}}
and thus:
:$\map d {\map g s, \map g t} \le \dfrac 1 {1 - K} \map d {\map f {\map g t, s}, \map f {\map g t, t} }$
The continuity of $g$ now follows from that of $f$ using the definition of product metric
{{qed}}
Theorem: Mapping at Element is Supremum of Compact Elements implies Mapping at Element is Supremum that Way Below

Let $\struct{S, \vee_1, \wedge_1, \preceq_1}$ and $\struct{T, \vee_2, \wedge_2, \preceq_2}$ be complete lattices.
Let $f: S \to T$ be a mapping such that
:$\forall x \in S: \map f x = \sup \leftset {\map f w: w \in S \land w \preceq_1 x \land w}$ is compact$\rightset{}$
Then
:$\forall x \in S: \map f x = \sup \set{ \map f w: w \in S \land w \ll x}$

Proof:
Let $x \in S$.
Define $X = \leftset {\map f w: w \in S \land w \preceq_1 x \land w}$ is compact$\rightset{}$
Define $Y = \set { \map f w: w \in S \land w \ll x}$
We will prove that
:$X \subseteq Y$
Let $b \in X$.
By definition of $X$:
:$\exists w \in S: b = \map f w \land w \preceq_1 x \land w$ is compact.
By definition of compact element:
:$w \ll w$
By Preceding and Way Below implies Way Below:
:$w \ll x$
Thus by definition of $Y$:
:$b \in Y$
{{qed|lemma}}
We will prove that
:$\map f x$ is upper bound for $Y$.
Let $b \in Y$.
By definition of $Y$:
:$\exists w \in S: b = \map f w \land w \ll x$
By Way Below implies Preceding:
:$w \preceq_1 x$
By Mapping at Element is Supremum implies Mapping is Increasing:
:$f$ is an increasing mapping.
Thus by definition of increasing mapping:
:$b \preceq_2 \map f x$
{{qed|lemma}}
We will prove that
:$\forall b \in T: b$ is upper bound for $Y \implies \map f x \preceq_2 b$
Let $b \in T$ such that
:$b$ is upper bound for $Y$.
By Upper Bound for Subset:
:$b$ is upper bound for $X$.
By assumption:
:$\map f x = \sup X$
Thus by definition of supremum:
:$\map f x \preceq_2 b$
{{qed|lemma}}
Thus by definition of supremum:
:$\map f x = \sup Y$
{{qed}}
Theorem: Inverse Function Theorem for Real Functions

Let $n \ge 1$ and $k \ge 1$ be natural numbers.
Let $\Omega \subset \R^n$ be open.
Let $f: \Omega \to \R^n$ be a vector-valued function of class $C^k$.
Let $a \in \Omega$.
Let the differential $D \map f a$ of $f$ at $a$ be invertible.
Then there exist open sets $U \subset \Omega$ and $V \subset \R^n$ such that:
:$a \in U$
:the restriction of $f$ to $U$ is a $C^k$-diffeomorphism $f: U \to V$.

Proof:
{{ProofWanted}}
Category:Implicit Functions
sg5dapv9eegzltg41sxmzl005tuvoft
Theorem: Sum of 714 and 715

The sum of $714$ and $715$ is a $4$-digit integer which has $6$ anagrams which are prime.

Proof:
We have that:
:$714 + 715 = 1429$
Hence we investigate its anagrams.
We bother only to check those which do not end in either $2$ or $4$, as those are even.
{{begin-eqn}}
{{eqn | l = 1429
      | o = 
      | c = is prime
}}
{{eqn | l = 1249
      | o = 
      | c = is prime
}}
{{eqn | l = 4129
      | o = 
      | c = is prime
}}
{{eqn | l = 4219
      | o = 
      | c = is prime
}}
{{eqn | l = 2149
      | r = 7 \times 307
      | c = and so is not prime
}}
{{eqn | l = 2419
      | r = 41 \times 59
      | c = and so is not prime
}}
{{eqn | l = 9241
      | o = 
      | c = is prime
}}
{{eqn | l = 9421
      | o = 
      | c = is prime
}}
{{eqn | l = 2941
      | r = 17 \times 173
      | c = and so is not prime
}}
{{eqn | l = 2491
      | r = 47 \times 53
      | c = and so is not prime
}}
{{eqn | l = 4291
      | r = 7 \times 613
      | c = and so is not prime
}}
{{eqn | l = 4921
      | r = 7 \times 19 \times 37
      | c = and so is not prime
}}
{{end-eqn}}
Of the above, $6$ are seen to be prime.
{{qed}}
Theorem: 720 is Product of Consecutive Numbers in Two Ways

:$720 = 6 \times 5 \times 4 \times 3 \times 2 = 10 \times 9 \times 8$

Proof:
Follows from Factorial as Product of Two Factorials:
:$10! = 6! \times 7!$
and so:
:$\dfrac {10!} {7!} = 10 \times 9 \times 8 = 6 \times 5 \times 4 \times 3 \times 2 \times 1$
Hence the result.
{{qed}}
Theorem: Factorial which is Sum of Two Squares

The only factorial which can be expressed as the sum of two squares is:
{{begin-eqn}}
{{eqn | l = 6!
      | r = 12^2 + 24^2
      | c = 
}}
{{end-eqn}}

Proof:
We show that for $n \ge 7$, $n!$ cannot be expressed as the sum of two squares.
By refining the result in Interval containing Prime Number of forms 4n - 1, 4n + 1, 6n - 1, 6n + 1, one can show that:
:There exists a prime of the form $4 k + 3$ strictly between $m$ and $2 m$ whenever $m \ge 4$.
Let $n \ge 7$. Then $\ceiling {\dfrac n 2} \ge 4$.
Using the result above, there is a prime $p$ of the form $4 k + 3$ such that:
:$\ceiling {\dfrac n 2} < p < 2 \ceiling {\dfrac n 2}$
We then have, by multiplying the inequality by $2$:
:$2 \ceiling {\dfrac n 2} < 2 p < 4 \ceiling {\dfrac n 2}$
This gives:
:$p < 2 \ceiling {\dfrac n 2} < 2 p$
Which implies:
:$p \le n < 2 p$
From Integer as Sum of Two Squares:
:$n!$ can be expressed as the sum of two squares {{iff}} each of its prime divisors of the form $4 k + 3$ (if any) occur to an even power.
The inequality above shows that there are no multiples of $p$ which are not greater than $n$ except $p$ itself.
Hence $p$ occurs to an odd power, $1$, in $n!$.
This shows that for $n \ge 7$, $n!$ cannot be expressed as the sum of two squares.
Checking the rest of the factorials we see that the only ones satisfying the criteria are:
{{begin-eqn}}
{{eqn | l = 0! = 1!
      | r = 0^2 + 1^2
}}
{{eqn | l = 2!
      | r = 1^2 + 1^2
}}
{{eqn | l = 6!
      | r = 12^2 + 24^2
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Multiplicity of 720 in 720 Factorial

The multiplicity of $720$ in $720!$ is $178$.
That is:
:$720^{178} \divides 720!$
but:
:$720^{179} \nmid 720!$
where:
:$720!$ denotes $720$ factorial
:$\divides$ denotes divisibility
:$\nmid$ denotes non-divisibility.

Proof:
We have that:
:$720 = 2^4 \times 3^2 \times 5$
It remains to inspect the divisibility of $2$, $3$ and $5$ in $720!$
Thus:
Theorem: Continuous iff Mapping at Element is Supremum

Let $\left({S, \preceq_1, \tau_1}\right)$ and $\left({T, \preceq_2, \tau_2}\right)$ be complete continuous topological lattices with Scott topologies.
Let $f: S \to T$ be a mapping.
Then $f$ is continuous {{iff}}
:$\forall x \in S: f\left({x}\right) = \sup \left\{ {f\left({w}\right): w \in S \land w \ll x}\right\}$

Proof:
=== Sufficient Condition ===
Assume that
:$f$ is continuous.
By Continuous iff Directed Suprema Preserving:
:$f$ is preserves directed suprema.
Thus by Directed Suprema Preserving Mapping at Element is Supremum:
:$\forall x \in S: f\left({x}\right) = \sup \left\{ {f\left({w}\right): w \in S \land w \ll x}\right\}$
{{qed|lemma}}
Theorem: Equivalence of Definitions of Synthetic Basis

Let $S$ be a set.
{{TFAE|def = Synthetic Basis}}

Proof:
We note that $\paren {\text B 1}$ and $\paren {\text B 1'}$ are the same for both definition $1$ and definition $2$.
It remains to demonstrate the equivalence of $\paren {\text B 2}$ and $\paren {\text B 2'}$.
Theorem: Equivalence of Definitions of Generated Submodule over Ring with Unity

Let $R$ be a ring with unity..
Let $\struct {M, +, \circ}_R$ be a unitary $R$-module.
Let $S\subset M$ be a subset.
{{TFAE|def = Generated Submodule}}

Proof:
Let:
:$\ds H_1 := \bigcap \set { M' \subseteq M : S \subseteq M', \textrm {$M'$ is a submodule of $M$} }$
be the intersection defined in first definition.
From Intersection of Submodules is Submodule:General Result, it follows that $H_1$ is a submodule of $M$.
Let:
:$\ds H_2 := \set { \sum_{i \mathop = 1}^n \lambda_i \circ x_i: n \in \N_{\ge 1}, \lambda_i \in R, x_i \in S}$
be the set defined in second definition.
To show equivalence of the definitions, we prove that $H_1 = H_2$.
Theorem: Equivalence of Definitions of Basis of Vector Space

Let $K$ be a division ring.
Let $\struct {G, +_G, \circ}_K$ be an vector space over $K$.
{{TFAE| def = Basis of Vector Space}}

Proof:
=== Definition 1 implies Definition 2 ===
Let $\BB$ be a linearly independent subset of $G$ which is a generator for $G$.
Suppose $\BB \subseteq \BB'$ is a linearly independent subset of $G$.
We aim to show that $\BB = \BB'$, proving maximality. 
Suppose that $\BB \ne \BB'$. 
Let $x \in \BB' \setminus \BB$. 
Since $G$ is a generator for $G$, there exists $x_1, \ldots, x_n \in \BB \subseteq \BB'$ and $\alpha_1, \ldots, \alpha_n \in K$ such that: 
:$\ds x = \sum_{i \mathop = 1}^n \alpha_i x_i$ 
so that: 
:$\ds \sum_{i \mathop = 1}^n \alpha_i x_i - x = 0$ 
Since $K$ is a field, we have that $-1 \ne 0$. 
This shows that $\set {x_1, \ldots, x_n, x}$ and hence $\BB'$ is linearly dependent. 
This is a contradiction, so we must have $\BB = \BB'$. 
{{qed|lemma}}
Theorem: Equivalence of Definitions of Differentiable Real Function at Point

Let $\openint a b \subset \R$ be an open interval.
Let $\xi$ be a point in $\openint a b$.
{{TFAE|def = Differentiable Real Function at Point|view = differentiable real function at a point}}

Proof:
{{ProofWanted|compare Equivalence of Definitions of Derivative}}
Category:Differentiable Real Functions
34ueqe29g1aqkgizzbncuvs99ypu7tq
Theorem: Continuous iff Mapping at Element is Supremum of Compact Elements

Let $L = \struct {S, \preceq_1, \tau_1}$ and $R = \struct {T, \preceq_2, \tau_2}$ be complete algebraic topological lattices with Scott topologies.
Let $f: S \to T$ be a mapping.
Then $f$ is continuous {{iff}}:
:$\forall x \in S: \map f x = \sup \leftset {\map f w: w \in S \land w \preceq_1 x \land w}$ is compact$\rightset {}$

Proof:
By Algebraic iff Continuous and For Every Way Below Exists Compact Between:
:$L$ and $R$ are continuous.
Theorem: Solutions to Approximate Fermat Equation x^3 = y^3 + z^3 Plus or Minus 1

The approximate Fermat equation:
:$x^3 = y^3 + z^3 \pm 1$
has the solutions:
{{begin-eqn}}
{{eqn | l = 9^3
      | r = 6^3 + 8^3 + 1
}}
{{eqn | l = 103^3
      | r = 64^3 + 94^3 - 1
      | c = 
}}
{{end-eqn}}

Proof:
Performing the arithmetic:
{{begin-eqn}}
{{eqn | l = 6^3 + 8^3 + 1
      | r = 216 + 512 + 1
}}
{{eqn | r = 729
      | c = 
}}
{{eqn | r = 9^3
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 64^3 + 94^3 - 1
      | r = 262 \, 144 + 830 \, 584 - 1
}}
{{eqn | r = 1 \, 092 \, 727
      | c = 
}}
{{eqn | r = 103^3
      | c = 
}}
{{end-eqn}}
{{qed}}
{{ExtractTheorem}}
Theorem: Cubes which are Sum of Five Cubes

The following cube numbers can be expressed as the sum of $5$ positive cube numbers:
:$9^3, \ldots$
{{expand|More terms needed. It seems that: </br> $4$ and all numbers $> 8$ can be so expressed </br> only $4, 8, 10, 11, 13$ require repeated cubes}}

Proof:
{{begin-eqn}}
{{eqn | l = 9^3
      | r = 729
      | c = 
}}
{{eqn | r = 1 + 27 + 64 + 125 + 512
      | c = 
}}
{{eqn | r = 1^3 + 3^3 + 4^3 + 5^3 + 8^3
      | c = 
}}
{{end-eqn}}
{{expand|Add the proof based on $9^3 {{=}} 1^3 + 6^3 + 8^3$ and $6^3 {{=}} 3^3 + 4^3 + 5^3$ from Cubes which are Sum of Three Cubes}}
Theorem: Implicit Function Theorem for Differentiable Real Functions

Let $\Omega \subset \R^{n+k}$ be open.
Let $f : \Omega \to \R^k$ be differentiable.
Let the $i$th partial derivatives of $f$ be continuous in $\Omega$ for $n+1 \leq i \leq n+k$.
Let $(a,b) \in \Omega$, with $a\in \R^n$ and $b\in \R^k$.
Let $f(a,b) = 0$.
For $(x_0,y_0)\in\Omega$, let $D_2 f(x_0,y_0)$ denote the differential of the function $y\mapsto f(x_0, y)$ at $y_0$.
Let the linear map $D_2 f(a,b)$ be invertible.
Then there exist neighborhoods $U\subset\Omega$ of $a$ and $V\subset\R^k$ of $b$ such that there exists a unique function $g : U \to V$ such that $f(x, g(x)) = 0$ for all $x\in U$.
Moreover, $g$ is differentiable, and its differential satisfies:
:$dg (x) = - \left( (D_2f)(x, g(x)) \right)^{-1} \circ (D_1 f)(x, g(x))$ for all $x\in U$.

Proof:
{{ProofWanted}}
Category:Implicit Functions
4t3eiy6pzrf811n7rr0487hxp0tgrea
Theorem: Implicit Function Theorem for Smooth Real Functions

Let $\Omega \subset \R^{n+k}$ be open.
Let $f : \Omega \to \R^k$ be smooth.
Let $(a,b) \in \Omega$, with $a\in \R^n$ and $b\in \R^k$.
Let $f(a,b) = 0$.
For $(x_0,y_0)\in\Omega$, let $D_2 f(x_0,y_0)$ denote the differential of the function $y\mapsto f(x_0, y)$ at $y_0$.
Let the linear map $D_2 f(a,b)$ be invertible.
Then there exist neighborhoods $U\subset\Omega$ of $a$ and $V\subset\R^k$ of $b$ such that there exists a unique function $g : U \to V$ such that $f(x, g(x)) = 0$ for all $x\in U$.
Moreover, $g$ is smooth, and its differential satisfies:
:$dg (x) = - \left( (D_2f)(x, g(x)) \right)^{-1} \circ (D_1 f)(x, g(x))$ for all $x\in U$.

Proof:
{{ProofWanted}}
Category:Implicit Functions
op8r7n6voyto8kaqajoonhlny7b7fra
Theorem: Implicit Function Theorem for Lipschitz Contractions

Let $M$ and $N$ be metric spaces.
Let $M$ be complete.
Let $f : M \times N \to M$ be a Lipschitz continuous uniform contraction.
Then for all $t\in N$ there exists a unique $\map g t \in M$ such that $\map f {\map g t, t} = \map g t$, and the mapping $g : N \to M$ is Lipschitz continuous.

Proof:
For every $t\in N$, the mapping:
:$f_t : M \to M : x \mapsto \map f {x, t}$ is a contraction mapping.
By the Banach Fixed-Point Theorem, there exists a unique $\map g t \in M$ such that $\map {f_t} {\map g t} = \map g t$.
We show that $g$ is Lipschitz continuous.
Let $K<1$ be a uniform Lipschitz constant for $f$.
Let $L$ be a Lipschitz constant for $f$.
Let $s,t\in N$.
Then
{{begin-eqn}}
{{eqn | l = \map d {\map g s, \map g t}
      | r = \map d {\map f {\map g s, s}, \map f {\map g t, t} }
      | c = Definition of $g$
}}
{{eqn | o = \le
      | r = \map d {\map f {\map g s, s}, \map f {\map g t, s} } + \map d {\map f {\map g t, s}, \map f {\map g t, t} }
      | c = {{Defof|Metric}}
}}
{{eqn | o = \le
      | r = K \cdot \map d {\map g s, \map g t} + \map d {\map f {\map g t, s}, \map f {\map g t, t} }
      | c = $f$ is a uniform contraction
}}
{{end-eqn}}
and thus:
{{begin-eqn}}
{{eqn | l = \map d {\map g s, \map g t}
      | o = \le
      | r = \dfrac 1 {1 - K} \map d {\map f {\map g t, s}, \map f {\map g t, t} }
}}
{{eqn | o = \le
      | r = \dfrac L {1 - K} \map d {s, t}
      | c = $f$ is Lipschitz continuous
}}
{{end-eqn}}
Thus $g$ is Lipschitz continuous.
{{qed}}
Category:Implicit Functions
kvrlxni05wpp3jsn9733cfatmu41440
Theorem: Implicit Function Theorem for Lipschitz Contraction at Point

Let $M$ and $N$ be metric spaces.
Let $M$ be complete.
Let $f: M \times N \to M$ be a uniform contraction.
Then for all $t \in N$ there exists a unique $\map g t \in M$ such that $\map f {\map g t, t} = \map g t$, and if $f$ is Lipschitz continuous at a point $\tuple {\map g t, t}$, then $g$ is Lipschitz continuous at $t$.

Proof:
For every $t \in N$, the mapping:
:$f_t : M \to M : x \mapsto \map f {x, t}$ is a contraction mapping.
{{explain|Source for above statement? What exactly does $f_t$ mean here?}}
By the Banach Fixed-Point Theorem, there exists a unique $\map g t \in M$ such that $\map {f_t} {\map g t} = \map g t$.
Let $f$ be Lipschitz continuous at $\tuple {\map g t, t}$.
We show that $g$ is Lipschitz continuous at $t$.
Let $K < 1$ be a uniform Lipschitz constant for $f$.
Let $L$ be a Lipschitz constant for $f$ at $a$.
Let $s\in N$.
Then
{{begin-eqn}}
{{eqn | l = \map d {\map g s, \map g t}
      | r = \map d {\map f {\map g s, s}, \map f {\map g t, t} }
      | c = Definition of $g$
}}
{{eqn | o = \le
      | r = \map d {\map f {\map g s, s}, \map f {\map g t, s} } + \map d {\map f {\map g t, s}, \map f {\map g t, t} }
      | c = {{Defof|Metric}}
}}
{{eqn | o = \le
      | r = K \cdot \map d {\map g s, \map g t} + \map d {\map f {\map g t, s}, \map f {\map g t, t} }
      | c = $f$ is a uniform contraction
}}
{{end-eqn}}
and thus:
{{begin-eqn}}
{{eqn | l = \map d {\map g s, \map g t}
      | o = \le
      | r = \dfrac 1 {1 - K} \map d {\map f {\map g t, s}, \map f {\map g t, t} }
}}
{{eqn | o = \le
      | r = \dfrac L {1 - K} \map d {s, t}
      | c = $f$ is Lipschitz continuous at $\tuple {\map g t, t}$
}}
{{end-eqn}}
Thus $g$ is Lipschitz continuous at $t$.
{{qed}}