From 6acc5654f1702f2466006564a415546a3def16e3 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 27 Aug 2024 17:19:02 +0200
Subject: Feature Complete Finalised the proof output and goals. The Local
 Function definition now producces a Function f with the right domain and
 range, together with the rules presented in cases. Then proof goal of this
 local definition is set to for all x we have x is element of dom(f) if and
 only if x is in exactly one of the subdomains. This suffices as
 welldefindness check on f, besides the right range.

Further checks that should be implemented are the correct range of the function.
And optional subproof such that the presented goal can be check easily.
---
 library/topology/urysohn2.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library/topology/urysohn2.tex')

diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index f2f6ef3..ea49a6c 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -46,7 +46,7 @@
 
     Define $f : X \to \reals$ such that  $f(x) = $
     \begin{cases}
-        &(x + x) &\text{if} x \in X
+        &(x + k) &\text{if} x \in X \land k \in \naturals
         & x &\text{if} x \neq \zero
         & \zero & \text{if} x = \zero
         % & x ,x \in X    <- will result in technicly ambigus parse
-- 
cgit v1.2.3

