Add concept of glossary.

finite-set-exercises
Joshua Potter 2023-05-12 19:31:44 -06:00
parent da7f00753b
commit 3fc293579d
5 changed files with 93 additions and 23 deletions

View File

@ -0,0 +1,57 @@
\documentclass{article}
\input{../../preamble}
\newcommand{\lean}[2]{\leanref{../../#1.html\##2}{#2}}
\begin{document}
\tableofcontents
\section{The Concepts of Integral Calculus}%
\label{sec:concepts-integral-calculus}
\subsection{\defined{Partition}}%
\label{sub:partition}
Let $[a, b]$ be a closed interval decomposed into $n$ subintervals by inserting
$n - 1$ points of subdivision, say $x_1$, $x_2$, $\ldots$, $x_{n-1}$, subject
only to the restriction
\begin{equation}
\label{sec:partition-eq1}
a < x_1 < x_2 < \cdots < x_{n-1} < b.
\end{equation}
It is convenient to denote the point $a$ itself by $x_0$ and the point $b$ by
$x_n$.
A collection of points satisfying \eqref{sec:partition-eq1} is called a
\textbf{partition} $P$ of $[a, b]$, and we use the symbol
$$P = \{x_0, x_1, \ldots, x_n\}$$ to designate this partition.
\begin{definition}
\lean{Common/Set/Intervals/Partition}{Set.Intervals.Partition}
\end{definition}
\subsection{\defined{Step Function}}%
\label{sub:step-function}
A function $s$, whose domain is a closed interval $[a, b]$, is called a step
function if there is a \nameref{sub:partition} $P = \{x_0, x_1, \ldots, x_n\}$
of $[a b]$ such that $s$ is constant on each open subinterval of $P$.
That is to say, for each $k = 1, 2, \ldots, n$, there is a real number $s_k$
such that $$s(x) = s_k \quad\text{if}\quad x_{k-1} < x < x_k.$$
Step functions are sometimes called piecewise constant functions.
\vspace{8pt}
\noindent
\textit{Note:} At each of the endpoints $x_{k-1}$ and $x_k$ the function must
have some well-defined value, but this need not be the same as $s_k$.
\begin{definition}
\lean{Common/Set/Intervals/StepFunction}{Set.Intervals.StepFunction}
\end{definition}
\end{document}

View File

@ -69,6 +69,12 @@ theorem right_ge_mem_self [Preorder α] [@DecidableRel α LT.lt]
(p : Partition α) : ∀ x ∈ p, x ≤ p.b := by (p : Partition α) : ∀ x ∈ p, x ≤ p.b := by
sorry sorry
/--
The closed interval determined by the endpoints of the `Partition`.
-/
abbrev toIcc [Preorder α] [@DecidableRel α LT.lt]
(p : Partition α) := Set.Icc p.a p.b
/- /-
Return the closed subintervals determined by the `Partition`. Return the closed subintervals determined by the `Partition`.
-/ -/
@ -76,6 +82,12 @@ def closedSubintervals [Preorder α] [@DecidableRel α LT.lt]
(p : Partition α) : List (Set α) := (p : Partition α) : List (Set α) :=
p.toList.pairwise (fun x₁ x₂ => Icc x₁ x₂) p.toList.pairwise (fun x₁ x₂ => Icc x₁ x₂)
/--
The open interval determined by the endpoints of the `Partition`.
-/
abbrev toIoo [Preorder α] [@DecidableRel α LT.lt]
(p : Partition α) := Set.Ioo p.a p.b
/- /-
Return the open subintervals determined by the `Partition`. Return the open subintervals determined by the `Partition`.
-/ -/

View File

@ -8,20 +8,19 @@ Characterization of step functions.
namespace Set.Intervals namespace Set.Intervals
open Partition
/-- /--
A function `f`, whose domain is a closed interval `[a, b]`, is a `StepFunction` A function `f`, whose domain is a closed interval `[a, b]`, is a `StepFunction`
if there exists a `Partition` `P = {x₀, x₁, …, xₙ}` of `[a, b]` such that `f` is if there exists a `Partition` `P = {x₀, x₁, …, xₙ}` of `[a, b]` such that `f` is
constant on each open subinterval of `P`. constant on each open subinterval of `P`.
-/ -/
structure StepFunction (α : Type _) [Preorder α] [@DecidableRel α LT.lt] where structure StepFunction (α : Type _) [Preorder α] [@DecidableRel α LT.lt] where
/- A partition of some closed interval `[a, b]`. -/ p : Partition α
partition : Partition α toFun : ∀ x ∈ p.toIcc, α
/-- A function whose domain is a closed interval `[a, b]`. -/
function : ∀ x ∈ Icc partition.a partition.b, α
/-- Ensure the function is constant on each open subinterval of `p`. -/
const_open_subintervals : const_open_subintervals :
∀ (hI : I ∈ partition.openSubintervals), ∃ c : α, ∀ (hy : y ∈ I), ∀ (hI : I ∈ p.openSubintervals), ∃ c : α, ∀ (hy : y ∈ I),
function y (Partition.mem_open_subinterval_mem_closed_interval hI hy) = c toFun y (mem_open_subinterval_mem_closed_interval hI hy) = c
namespace StepFunction namespace StepFunction

View File

@ -37,13 +37,20 @@ def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <|
status: status:
<ul> <ul>
<li> <li>
<span style="color:teal">Teal statements </span> are those that <span style="color:darkgray">Dark gray statements </span> are
have been proven or encoded in both LaTeX and Lean. reserved for definitions and axioms that have been encoded in both
LaTeX and Lean.
</li> </li>
<li> <li>
<span style="color:magenta">Magenta statements </span> are those <span style="color:teal">Teal statements </span> are reserved for
that have been proven or encoded in LaTeX but not yet verified in statements, theorems, lemmas, etc. that have been proven in both
Lean. LaTeX and Lean.
</li>
<li>
<span style="color:magenta">Magenta statements </span> are reserved
for definitions, axioms, statements, theorems, lemmas, etc. that
have been proven or encoded in LaTeX but not yet proven or encoded
in Lean.
</li> </li>
<li> <li>
<span style="color:red">Red </span> serves as a catch-all for all <span style="color:red">Red </span> serves as a catch-all for all

View File

@ -14,8 +14,8 @@
% Linking % Linking
% ======================================== % ========================================
\hypersetup{colorlinks=true, urlcolor=blue} \hypersetup{colorlinks=true, linkcolor=blue, urlcolor=blue}
\newcommand{\leanref}[2]{{\color{blue}$\pmb{\exists}\;{-}\;$}\href{#1}{#2}} \newcommand{\leanref}[2]{\textcolor{blue}{$\pmb{\exists}\;{-}\;$}\href{#1}{#2}}
% ======================================== % ========================================
% Environments % Environments
@ -24,6 +24,9 @@
\newenvironment{axiom}{% \newenvironment{axiom}{%
\paragraph{\normalfont\normalsize\textit{Axiom.}}} \paragraph{\normalfont\normalsize\textit{Axiom.}}}
{\hfill$\square$} {\hfill$\square$}
\newenvironment{definition}{%
\paragraph{\normalfont\normalsize\textit{Definition.}}}
{\hfill$\square$}
\newcommand{\divider}{% \newcommand{\divider}{%
\vspace{10pt} \vspace{10pt}
\hrule \hrule
@ -47,20 +50,12 @@
% Status % Status
% ======================================== % ========================================
% Used for statements encoded in both LaTeX and Lean.
\DeclareRobustCommand{\defined}[1]{% \DeclareRobustCommand{\defined}[1]{%
\texorpdfstring{\color{teal}\faParagraph\ #1}{#1}} \texorpdfstring{\color{darkgray}\faParagraph\ #1}{#1}}
% Used for statements proven in both LaTeX and Lean.
\DeclareRobustCommand{\verified}[1]{% \DeclareRobustCommand{\verified}[1]{%
\texorpdfstring{\color{teal}\faCheckCircle\ #1}{#1}} \texorpdfstring{\color{teal}\faCheckCircle\ #1}{#1}}
% Used for statements proven or encoded in LaTeX but not yet in Lean.
\DeclareRobustCommand{\partial}[1]{% \DeclareRobustCommand{\partial}[1]{%
\texorpdfstring{\color{magenta}\faPencil*\ #1}{#1}} \texorpdfstring{\color{magenta}\faPencil*\ #1}{#1}}
% A catch-all for anything that doesn't fit the above categories. Incomplete
% definitions, statements without proof, etc. belong here.
\DeclareRobustCommand{\unverified}[1]{% \DeclareRobustCommand{\unverified}[1]{%
\texorpdfstring{\color{red}\faExclamationCircle\ #1}{#1}} \texorpdfstring{\color{red}\faExclamationCircle\ #1}{#1}}