Deploying to gh-pages from @ 7fbbc1d 🚀

jjdishere · Sep 28, 2023 · 15ce041 · 15ce041
1 parent 8e18ca5
commit 15ce041
Show file tree

Hide file tree

Showing 174 changed files with 860 additions and 842 deletions.
diff --git a/EuclideanGeometry.html b/EuclideanGeometry.html
@@ -1,4 +1,4 @@
 <html lang="en"><head><meta charset="UTF-8"></meta><meta name="viewport" content="width=device-width, initial-scale=1"></meta><link rel="stylesheet" href="./style.css"></link><link rel="stylesheet" href="./src/pygments.css"></link><link rel="shortcut icon" href="./favicon.ico"></link><link rel="prefetch" href=".//declarations/declaration-data.bmp" as="image"></link><title>EuclideanGeometry</title><script defer="true" src="./mathjax-config.js"></script><script defer="true" src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script><script defer="true" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script><script>const SITE_ROOT="./";</script><script>const MODULE_NAME="EuclideanGeometry";</script><script type="module" src="./jump-src.js"></script><script type="module" src="./search.js"></script><script type="module" src="./expand-nav.js"></script><script type="module" src="./how-about.js"></script><script type="module" src="./instances.js"></script><script type="module" src="./importedBy.js"></script></head><body><input id="nav_toggle" type="checkbox"></input><header><h1><label for="nav_toggle"></label>Documentation</h1><p class="header_filename break_within"><span class="name">EuclideanGeometry</span></p><form action="https://google.com/search" method="get" id="search_form"><input type="hidden" name="sitesearch" value="https://leanprover-community.github.io/mathlib4_docs"></input><input type="text" name="q" autocomplete="off"></input>&#32;
-            <button id="search_button" onclick="javascript: form.action='./search.html';">Search</button><button>Google site search</button></form></header><nav class="internal_nav"><h3><a class="break_within" href="#top"><span class="name">EuclideanGeometry</span></a></h3><p class="gh_nav_link"><a href="https://github.com/jjdishere/EG/blob/c40c263cb0c12c73c247f0329375450f553a5e81//EuclideanGeometry.lean">source</a></p><div class="imports"><details><summary>Imports</summary><ul><li><a href="./Init.html">Init</a></li><li><a href="./EuclideanGeometry/Example/Index.html">EuclideanGeometry.Example.Index</a></li><li><a href="./EuclideanGeometry/Foundation/Index.html">EuclideanGeometry.Foundation.Index</a></li></ul></details><details><summary>Imported by</summary><ul id="imported-by-EuclideanGeometry" class="imported-by-list"></ul></details></div></nav><main>
+            <button id="search_button" onclick="javascript: form.action='./search.html';">Search</button><button>Google site search</button></form></header><nav class="internal_nav"><h3><a class="break_within" href="#top"><span class="name">EuclideanGeometry</span></a></h3><p class="gh_nav_link"><a href="https://github.com/jjdishere/EG/blob/7fbbc1dd47e786ef24e0cc9e139d52f7eab71410//EuclideanGeometry.lean">source</a></p><div class="imports"><details><summary>Imports</summary><ul><li><a href="./Init.html">Init</a></li><li><a href="./EuclideanGeometry/Example/Index.html">EuclideanGeometry.Example.Index</a></li><li><a href="./EuclideanGeometry/Foundation/Index.html">EuclideanGeometry.Foundation.Index</a></li></ul></details><details><summary>Imported by</summary><ul id="imported-by-EuclideanGeometry" class="imported-by-list"></ul></details></div></nav><main>
 <div class="mod_doc"><h1 class="markdown-heading" id="Euclidean-Geometry">Euclidean Geometry <a class="hover-link" href="#Euclidean-Geometry">#</a></h1><p>Welcome! This project aims to formalize the Euclidean Geometry in Lean. Please enjoy youeself in exploring with theorems and examples.</p></div></main>
 <nav class="nav"><iframe src="./navbar.html" class="navframe" frameBorder="0"></iframe></nav></body></html>
diff --git a/EuclideanGeometry.html.hash b/EuclideanGeometry.html.hash
@@ -1 +1 @@
-10636906688814281902
+960252097865868161
diff --git a/EuclideanGeometry.html.trace b/EuclideanGeometry.html.trace
@@ -1 +1 @@
-6868770566734400818
+3058136448700533037
diff --git a/EuclideanGeometry/Example/AOPS/Chap2.html b/EuclideanGeometry/Example/AOPS/Chap2.html
@@ -1,4 +1,4 @@
 <html lang="en"><head><meta charset="UTF-8"></meta><meta name="viewport" content="width=device-width, initial-scale=1"></meta><link rel="stylesheet" href="../../.././style.css"></link><link rel="stylesheet" href="../../.././src/pygments.css"></link><link rel="shortcut icon" href="../../.././favicon.ico"></link><link rel="prefetch" href="../../.././/declarations/declaration-data.bmp" as="image"></link><title>EuclideanGeometry.Example.AOPS.Chap2</title><script defer="true" src="../../.././mathjax-config.js"></script><script defer="true" src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script><script defer="true" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script><script>const SITE_ROOT="../../.././";</script><script>const MODULE_NAME="EuclideanGeometry.Example.AOPS.Chap2";</script><script type="module" src="../../.././jump-src.js"></script><script type="module" src="../../.././search.js"></script><script type="module" src="../../.././expand-nav.js"></script><script type="module" src="../../.././how-about.js"></script><script type="module" src="../../.././instances.js"></script><script type="module" src="../../.././importedBy.js"></script></head><body><input id="nav_toggle" type="checkbox"></input><header><h1><label for="nav_toggle"></label>Documentation</h1><p class="header_filename break_within"><span class="name">EuclideanGeometry</span>.<span class="name">Example</span>.<span class="name">AOPS</span>.<span class="name">Chap2</span></p><form action="https://google.com/search" method="get" id="search_form"><input type="hidden" name="sitesearch" value="https://leanprover-community.github.io/mathlib4_docs"></input><input type="text" name="q" autocomplete="off"></input>&#32;
-            <button id="search_button" onclick="javascript: form.action='../../.././search.html';">Search</button><button>Google site search</button></form></header><nav class="internal_nav"><h3><a class="break_within" href="#top"><span class="name">EuclideanGeometry</span>.<span class="name">Example</span>.<span class="name">AOPS</span>.<span class="name">Chap2</span></a></h3><p class="gh_nav_link"><a href="https://github.com/jjdishere/EG/blob/c40c263cb0c12c73c247f0329375450f553a5e81//EuclideanGeometry/Example/AOPS/Chap2.lean">source</a></p><div class="imports"><details><summary>Imports</summary><ul><li><a href="../../.././Init.html">Init</a></li><li><a href="../../.././EuclideanGeometry/Foundation/Index.html">EuclideanGeometry.Foundation.Index</a></li></ul></details><details><summary>Imported by</summary><ul id="imported-by-EuclideanGeometry.Example.AOPS.Chap2" class="imported-by-list"></ul></details></div></nav><main>
+            <button id="search_button" onclick="javascript: form.action='../../.././search.html';">Search</button><button>Google site search</button></form></header><nav class="internal_nav"><h3><a class="break_within" href="#top"><span class="name">EuclideanGeometry</span>.<span class="name">Example</span>.<span class="name">AOPS</span>.<span class="name">Chap2</span></a></h3><p class="gh_nav_link"><a href="https://github.com/jjdishere/EG/blob/7fbbc1dd47e786ef24e0cc9e139d52f7eab71410//EuclideanGeometry/Example/AOPS/Chap2.lean">source</a></p><div class="imports"><details><summary>Imports</summary><ul><li><a href="../../.././Init.html">Init</a></li><li><a href="../../.././EuclideanGeometry/Foundation/Index.html">EuclideanGeometry.Foundation.Index</a></li></ul></details><details><summary>Imported by</summary><ul id="imported-by-EuclideanGeometry.Example.AOPS.Chap2" class="imported-by-list"></ul></details></div></nav><main>
 </main>
 <nav class="nav"><iframe src="../../.././navbar.html" class="navframe" frameBorder="0"></iframe></nav></body></html>
diff --git a/EuclideanGeometry/Example/AOPS/Chap2.html.hash b/EuclideanGeometry/Example/AOPS/Chap2.html.hash
@@ -1 +1 @@
-8383406021900553125
+4179101947466671194
diff --git a/EuclideanGeometry/Example/AOPS/Chap2.html.trace b/EuclideanGeometry/Example/AOPS/Chap2.html.trace
@@ -1 +1 @@
-5741431696483615539
+18219815569272085332
diff --git a/EuclideanGeometry/Example/AOPS/Chap3.html b/EuclideanGeometry/Example/AOPS/Chap3.html
@@ -1,6 +1,6 @@
 <html lang="en"><head><meta charset="UTF-8"></meta><meta name="viewport" content="width=device-width, initial-scale=1"></meta><link rel="stylesheet" href="../../.././style.css"></link><link rel="stylesheet" href="../../.././src/pygments.css"></link><link rel="shortcut icon" href="../../.././favicon.ico"></link><link rel="prefetch" href="../../.././/declarations/declaration-data.bmp" as="image"></link><title>EuclideanGeometry.Example.AOPS.Chap3</title><script defer="true" src="../../.././mathjax-config.js"></script><script defer="true" src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script><script defer="true" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script><script>const SITE_ROOT="../../.././";</script><script>const MODULE_NAME="EuclideanGeometry.Example.AOPS.Chap3";</script><script type="module" src="../../.././jump-src.js"></script><script type="module" src="../../.././search.js"></script><script type="module" src="../../.././expand-nav.js"></script><script type="module" src="../../.././how-about.js"></script><script type="module" src="../../.././instances.js"></script><script type="module" src="../../.././importedBy.js"></script></head><body><input id="nav_toggle" type="checkbox"></input><header><h1><label for="nav_toggle"></label>Documentation</h1><p class="header_filename break_within"><span class="name">EuclideanGeometry</span>.<span class="name">Example</span>.<span class="name">AOPS</span>.<span class="name">Chap3</span></p><form action="https://google.com/search" method="get" id="search_form"><input type="hidden" name="sitesearch" value="https://leanprover-community.github.io/mathlib4_docs"></input><input type="text" name="q" autocomplete="off"></input>&#32;
-            <button id="search_button" onclick="javascript: form.action='../../.././search.html';">Search</button><button>Google site search</button></form></header><nav class="internal_nav"><h3><a class="break_within" href="#top"><span class="name">EuclideanGeometry</span>.<span class="name">Example</span>.<span class="name">AOPS</span>.<span class="name">Chap3</span></a></h3><p class="gh_nav_link"><a href="https://github.com/jjdishere/EG/blob/c40c263cb0c12c73c247f0329375450f553a5e81//EuclideanGeometry/Example/AOPS/Chap3.lean">source</a></p><div class="imports"><details><summary>Imports</summary><ul><li><a href="../../.././Init.html">Init</a></li><li><a href="../../.././EuclideanGeometry/Foundation/Index.html">EuclideanGeometry.Foundation.Index</a></li></ul></details><details><summary>Imported by</summary><ul id="imported-by-EuclideanGeometry.Example.AOPS.Chap3" class="imported-by-list"></ul></details></div><div class="nav_link"><a class="break_within" href="#EuclidGeom.Exercise_3_4_4.a_ne_b"><span class="name">EuclidGeom</span>.<span class="name">Exercise_3_4_4</span>.<span class="name">a_ne_b</span></a></div><div class="nav_link"><a class="break_within" href="#EuclidGeom.Exercise_3_4_4.a_ne_c"><span class="name">EuclidGeom</span>.<span class="name">Exercise_3_4_4</span>.<span class="name">a_ne_c</span></a></div><div class="nav_link"><a class="break_within" href="#EuclidGeom.Exercise_3_4_4.x_ne_b"><span class="name">EuclidGeom</span>.<span class="name">Exercise_3_4_4</span>.<span class="name">x_ne_b</span></a></div><div class="nav_link"><a class="break_within" href="#EuclidGeom.Exercise_3_4_4.y_ne_c"><span class="name">EuclidGeom</span>.<span class="name">Exercise_3_4_4</span>.<span class="name">y_ne_c</span></a></div></nav><main>
-<div class="decl" id="EuclidGeom.Exercise_3_4_4.a_ne_b"><div class="theorem"><div class="gh_link"><a href="https://github.com/jjdishere/EG/blob/c40c263cb0c12c73c247f0329375450f553a5e81//EuclideanGeometry/Example/AOPS/Chap3.lean#L20-L20">source</a></div><div class="decl_header"><span class="decl_kind">theorem</span>
+            <button id="search_button" onclick="javascript: form.action='../../.././search.html';">Search</button><button>Google site search</button></form></header><nav class="internal_nav"><h3><a class="break_within" href="#top"><span class="name">EuclideanGeometry</span>.<span class="name">Example</span>.<span class="name">AOPS</span>.<span class="name">Chap3</span></a></h3><p class="gh_nav_link"><a href="https://github.com/jjdishere/EG/blob/7fbbc1dd47e786ef24e0cc9e139d52f7eab71410//EuclideanGeometry/Example/AOPS/Chap3.lean">source</a></p><div class="imports"><details><summary>Imports</summary><ul><li><a href="../../.././Init.html">Init</a></li><li><a href="../../.././EuclideanGeometry/Foundation/Index.html">EuclideanGeometry.Foundation.Index</a></li></ul></details><details><summary>Imported by</summary><ul id="imported-by-EuclideanGeometry.Example.AOPS.Chap3" class="imported-by-list"></ul></details></div><div class="nav_link"><a class="break_within" href="#EuclidGeom.Exercise_3_4_4.a_ne_b"><span class="name">EuclidGeom</span>.<span class="name">Exercise_3_4_4</span>.<span class="name">a_ne_b</span></a></div><div class="nav_link"><a class="break_within" href="#EuclidGeom.Exercise_3_4_4.a_ne_c"><span class="name">EuclidGeom</span>.<span class="name">Exercise_3_4_4</span>.<span class="name">a_ne_c</span></a></div><div class="nav_link"><a class="break_within" href="#EuclidGeom.Exercise_3_4_4.x_ne_b"><span class="name">EuclidGeom</span>.<span class="name">Exercise_3_4_4</span>.<span class="name">x_ne_b</span></a></div><div class="nav_link"><a class="break_within" href="#EuclidGeom.Exercise_3_4_4.y_ne_c"><span class="name">EuclidGeom</span>.<span class="name">Exercise_3_4_4</span>.<span class="name">y_ne_c</span></a></div></nav><main>
+<div class="decl" id="EuclidGeom.Exercise_3_4_4.a_ne_b"><div class="theorem"><div class="gh_link"><a href="https://github.com/jjdishere/EG/blob/7fbbc1dd47e786ef24e0cc9e139d52f7eab71410//EuclideanGeometry/Example/AOPS/Chap3.lean#L20-L20">source</a></div><div class="decl_header"><span class="decl_kind">theorem</span>
 <span class="decl_name"><a class="break_within" href="../../.././EuclideanGeometry/Example/AOPS/Chap3.html#EuclidGeom.Exercise_3_4_4.a_ne_b"><span class="name">EuclidGeom</span>.<span class="name">Exercise_3_4_4</span>.<span class="name">a_ne_b</span></a></span><span class="impl_arg"><span class="decl_args">
 <span class="fn">{P : <a href="../../.././foundational_types.html">Type</a> u_1}</span></span>
 </span><span class="impl_arg"><span class="decl_args">
@@ -13,7 +13,7 @@
 <span class="fn">{C : <span class="fn">P</span>}</span></span>
 </span><span class="impl_arg"><span class="decl_args">
 <span class="fn">{hnd : <span class="fn"><a href="../../.././Init/Prelude.html#Not">¬</a><span class="fn"><a href="../../.././EuclideanGeometry/Foundation/Axiom/Linear/Colinear.html#EuclidGeom.colinear">EuclidGeom.colinear</a> <span class="fn">A</span> <span class="fn">B</span> <span class="fn">C</span></span></span>}</span></span>
-</span><span class="decl_args"> :</span><div class="decl_type"><span class="fn"><span class="fn">A</span> <a href="../../.././Init/Core.html#Ne">≠</a> <span class="fn">B</span></span></div></div></div></div><div class="decl" id="EuclidGeom.Exercise_3_4_4.a_ne_c"><div class="theorem"><div class="gh_link"><a href="https://github.com/jjdishere/EG/blob/c40c263cb0c12c73c247f0329375450f553a5e81//EuclideanGeometry/Example/AOPS/Chap3.lean#L21-L21">source</a></div><div class="decl_header"><span class="decl_kind">theorem</span>
+</span><span class="decl_args"> :</span><div class="decl_type"><span class="fn"><span class="fn">A</span> <a href="../../.././Init/Core.html#Ne">≠</a> <span class="fn">B</span></span></div></div></div></div><div class="decl" id="EuclidGeom.Exercise_3_4_4.a_ne_c"><div class="theorem"><div class="gh_link"><a href="https://github.com/jjdishere/EG/blob/7fbbc1dd47e786ef24e0cc9e139d52f7eab71410//EuclideanGeometry/Example/AOPS/Chap3.lean#L21-L21">source</a></div><div class="decl_header"><span class="decl_kind">theorem</span>
 <span class="decl_name"><a class="break_within" href="../../.././EuclideanGeometry/Example/AOPS/Chap3.html#EuclidGeom.Exercise_3_4_4.a_ne_c"><span class="name">EuclidGeom</span>.<span class="name">Exercise_3_4_4</span>.<span class="name">a_ne_c</span></a></span><span class="impl_arg"><span class="decl_args">
 <span class="fn">{P : <a href="../../.././foundational_types.html">Type</a> u_1}</span></span>
 </span><span class="impl_arg"><span class="decl_args">
@@ -26,7 +26,7 @@
 <span class="fn">{C : <span class="fn">P</span>}</span></span>
 </span><span class="impl_arg"><span class="decl_args">
 <span class="fn">{hnd : <span class="fn"><a href="../../.././Init/Prelude.html#Not">¬</a><span class="fn"><a href="../../.././EuclideanGeometry/Foundation/Axiom/Linear/Colinear.html#EuclidGeom.colinear">EuclidGeom.colinear</a> <span class="fn">A</span> <span class="fn">B</span> <span class="fn">C</span></span></span>}</span></span>
-</span><span class="decl_args"> :</span><div class="decl_type"><span class="fn"><span class="fn">A</span> <a href="../../.././Init/Core.html#Ne">≠</a> <span class="fn">C</span></span></div></div></div></div><div class="decl" id="EuclidGeom.Exercise_3_4_4.x_ne_b"><div class="theorem"><div class="gh_link"><a href="https://github.com/jjdishere/EG/blob/c40c263cb0c12c73c247f0329375450f553a5e81//EuclideanGeometry/Example/AOPS/Chap3.lean#L25-L25">source</a></div><div class="decl_header"><span class="decl_kind">theorem</span>
+</span><span class="decl_args"> :</span><div class="decl_type"><span class="fn"><span class="fn">A</span> <a href="../../.././Init/Core.html#Ne">≠</a> <span class="fn">C</span></span></div></div></div></div><div class="decl" id="EuclidGeom.Exercise_3_4_4.x_ne_b"><div class="theorem"><div class="gh_link"><a href="https://github.com/jjdishere/EG/blob/7fbbc1dd47e786ef24e0cc9e139d52f7eab71410//EuclideanGeometry/Example/AOPS/Chap3.lean#L25-L25">source</a></div><div class="decl_header"><span class="decl_kind">theorem</span>
 <span class="decl_name"><a class="break_within" href="../../.././EuclideanGeometry/Example/AOPS/Chap3.html#EuclidGeom.Exercise_3_4_4.x_ne_b"><span class="name">EuclidGeom</span>.<span class="name">Exercise_3_4_4</span>.<span class="name">x_ne_b</span></a></span><span class="impl_arg"><span class="decl_args">
 <span class="fn">{P : <a href="../../.././foundational_types.html">Type</a> u_1}</span></span>
 </span><span class="impl_arg"><span class="decl_args">
@@ -41,7 +41,7 @@
 <span class="fn">{X : <span class="fn">P</span>}</span></span>
 </span><span class="impl_arg"><span class="decl_args">
 <span class="fn">{hx : <span class="fn"><a href="../../.././EuclideanGeometry/Foundation/Axiom/Basic/Class.html#EuclidGeom.lies_int">EuclidGeom.lies_int</a> <span class="fn">X</span> <span class="fn">{ <span class="fn">source</span> := <span class="fn">A</span>, <span class="fn">target</span> := <span class="fn">C</span> }</span></span>}</span></span>
-</span><span class="decl_args"> :</span><div class="decl_type"><span class="fn"><span class="fn">X</span> <a href="../../.././Init/Core.html#Ne">≠</a> <span class="fn">B</span></span></div></div></div></div><div class="decl" id="EuclidGeom.Exercise_3_4_4.y_ne_c"><div class="theorem"><div class="gh_link"><a href="https://github.com/jjdishere/EG/blob/c40c263cb0c12c73c247f0329375450f553a5e81//EuclideanGeometry/Example/AOPS/Chap3.lean#L26-L26">source</a></div><div class="decl_header"><span class="decl_kind">theorem</span>
+</span><span class="decl_args"> :</span><div class="decl_type"><span class="fn"><span class="fn">X</span> <a href="../../.././Init/Core.html#Ne">≠</a> <span class="fn">B</span></span></div></div></div></div><div class="decl" id="EuclidGeom.Exercise_3_4_4.y_ne_c"><div class="theorem"><div class="gh_link"><a href="https://github.com/jjdishere/EG/blob/7fbbc1dd47e786ef24e0cc9e139d52f7eab71410//EuclideanGeometry/Example/AOPS/Chap3.lean#L26-L26">source</a></div><div class="decl_header"><span class="decl_kind">theorem</span>
 <span class="decl_name"><a class="break_within" href="../../.././EuclideanGeometry/Example/AOPS/Chap3.html#EuclidGeom.Exercise_3_4_4.y_ne_c"><span class="name">EuclidGeom</span>.<span class="name">Exercise_3_4_4</span>.<span class="name">y_ne_c</span></a></span><span class="impl_arg"><span class="decl_args">
 <span class="fn">{P : <a href="../../.././foundational_types.html">Type</a> u_1}</span></span>
 </span><span class="impl_arg"><span class="decl_args">

diff --git a/EuclideanGeometry/Example/AOPS/Chap3.html.hash b/EuclideanGeometry/Example/AOPS/Chap3.html.hash
@@ -1 +1 @@
-4965983880921030744
+9412719551386672736