% (find-angg "LATEX/2016-2-LA-zhas.tex")
% (find-angg "LATEX/2016-2-LA-zhas.lua")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2016-2-LA-zhas.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2016-2-LA-zhas.pdf"))
% (defun e () (interactive) (find-LATEX "2016-2-LA-zhas.tex"))
% (defun u () (interactive) (find-latex-upload-links "2016-2-LA-zhas"))
% (find-xpdfpage "~/LATEX/2016-2-LA-zhas.pdf")
% (find-sh0 "cp -v  ~/LATEX/2016-2-LA-zhas.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2016-2-LA-zhas.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2016-2-LA-zhas.pdf
%               file:///tmp/2016-2-LA-zhas.pdf
%           file:///tmp/pen/2016-2-LA-zhas.pdf
% http://angg.twu.net/LATEX/2016-2-LA-zhas.pdf

% «.comprehension»		(to "comprehension")
% «.comprehension-2»		(to "comprehension-2")
% «.comprehension-3»		(to "comprehension-3")

\documentclass[oneside]{book}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage{color}                % (find-LATEX "edrx15.sty" "colors")
\usepackage{colorweb}             % (find-es "tex" "colorweb")
\usepackage{tikz}
%
\usepackage{edrx15}               % (find-angg "LATEX/edrx15.sty")
\input edrxaccents.tex            % (find-angg "LATEX/edrxaccents.tex")
\input edrxchars.tex              % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex           % (find-dn4ex "edrxheadfoot.tex")
\input edrxgac2.tex               % (find-LATEX "edrxgac2.tex")
%
\begin{document}

\catcode`\^^J=10
\directlua{dednat6dir = "dednat6/"}
\directlua{dofile(dednat6dir.."dednat6.lua")}
\directlua{texfile(tex.jobname)}
\directlua{verbose()}
\directlua{output(preamble1)}
\def\expr#1{\directlua{output(tostring(#1))}}
\def\eval#1{\directlua{#1}}
\def\pu{\directlua{pu()}}

\directlua{dofile "edrxtikz.lua"} % (find-LATEX "edrxtikz.lua")
\directlua{dofile "edrxpict.lua"} % (find-LATEX "edrxpict.lua")
%L V.__tostring = function (v) return format("(%.3f,%.3f)", v[1], v[2]) end
\pu

\unitlength=9pt
\def\closeddot{\circle*{0.3}}
\def\opendot  {\circle*{0.3}\color{white}\circle*{0.2}}




%   ____                               _                    _             
%  / ___|___  _ __ ___  _ __  _ __ ___| |__   ___ _ __  ___(_) ___  _ __  
% | |   / _ \| '_ ` _ \| '_ \| '__/ _ \ '_ \ / _ \ '_ \/ __| |/ _ \| '_ \ 
% | |__| (_) | | | | | | |_) | | |  __/ | | |  __/ | | \__ \ | (_) | | | |
%  \____\___/|_| |_| |_| .__/|_|  \___|_| |_|\___|_| |_|___/_|\___/|_| |_|
%                      |_|                                                
%
% «comprehension» (to ".comprehension")
% (find-LATEX "2016-2-GA-algebra.tex" "comprehension")
% (laz162p 1 "comprehension")
% (lalp 8)

\def\und#1#2{\underbrace{#1}_{#2}}
\def\und#1#2{\underbrace{#1}_{\text{#2}}}
\def\ug#1{\und{#1}{gen}}
\def\uf#1{\und{#1}{filt}}
\def\ue#1{\und{#1}{expr}}
\def\uv#1{\und{#1}{var}}

{\bf Set comprehensions}

\ssk

In the (non-standard) explicit notation for set comprehensions

we have generators and filters separated by commas,

then a ``;'', then the output expression:

\ssk

$\begin{array}{lll}
\{\ug{a∈\{1,2,3,4\}}; \ue{10a}\}     &=& \{10,20,30,40\} \\
\{\ug{a∈\{1,2,3,4\}}; \ue{a}\}       &=& \{1,2,3,4\} \\
\{\ug{a∈\{1,2,3,4\}}, \uf{a≥3}; \ue{a}\} &=& \{3,4\} \\
\{\ug{a∈\{1,2,3,4\}}, \uf{a≥3}; \ue{10a}\} &=& \{30,40\} \\
\{\ug{a∈\{10,20\}}, \ug{b∈\{3,4\}}; \ue{a+b}\} &=& \{13,14,23,24\} \\
\{\ug{a∈\{1,2\}}, \ug{b∈\{3,4\}}; \ue{(a,b)}\} &=& \{(1,3),(1,4),(2,3),(2,4)\} \\
\end{array}
$

\bsk

We can calculate set comprehensions using tables.

Here are two examples.

\def\tbl#1#2{\fbox{$\begin{array}{#1}#2\end{array}$}}
\def\tbl#1#2{\fbox{$\sm{#2}$}}
\def\V{\mathbf{T}}
\def\F{\mathbf{F}}
% "Stop":
\def\S{\omit$|$\hss}
\def\S{\omit\vrule\hss}
\def\S{\omit\vrule$($\hss}
\def\S{\omit\vrule$\scriptstyle($\hss}
\def\S{\omit\vrule\phantom{$\scriptstyle($}\hss}   % stop
% strut:
\def\s{\mathstrut}
\def\s{\phantom{$|$}}
\def\s{\phantom{|}}
\def\s{}

\msk

$\{\ug{x∈\{1,2,3\}}, \ug{y∈\{3,4\}}, \uf{x+y<6}; \ue{(x,y)}\}
 = \{(1,3),(1,4),(2,3)\}
$

\tbl{ccc}{
 \s x & y & x+y<6 & (x,y) \\\hline
 \s 1 & 3 & \V & (1,3) \\
 \s 1 & 4 & \V & (1,4) \\
 \s 2 & 3 & \V & (2,3) \\
 \s 2 & 4 & \F & \S \\
 \s 3 & 3 & \F & \S \\
 \s 3 & 4 & \F & \S \\
}

\bsk
$\{\ug{(x,y)∈\{1,2,3\}^2}, \uf{x>y}; \ue{(x,y)}\}
 = \{(2,1), (3,1), (3,2)\}
$

\tbl{ccc}{
 \s (x,y) & x & y & x>y & (x,y) \\\hline
 \s (1,1) & 1 & 1 & \F & \S \\
 \s (1,2) & 1 & 2 & \F & \S    \\
 \s (1,3) & 1 & 3 & \F & \S    \\
 \s (2,1) & 2 & 1 & \V & (2,1) \\
 \s (2,2) & 2 & 2 & \F & \S    \\
 \s (2,3) & 2 & 3 & \F & \S    \\
 \s (3,1) & 3 & 1 & \V & (3,1) \\
 \s (3,2) & 3 & 2 & \V & (3,2) \\
 \s (3,3) & 3 & 3 & \F & \S    \\
}

\newpage

% «comprehension-2» (to ".comprehension-2")
% (laz162p 2 "comprehension-2")
% (lazp 2)

{\bf Set comprehensions (2)}

There are {\sl two} standard notations for set comprehensions --

they both use ``$|$'', but one is ``$\setofst{\text{generator}}{\text{filters}}$'' (``g$|$f'')

the other ``$\setofst{\text{expr}}{\text{generators and filters}}$'' (``e$|$gf'')...

Here are some examples of translations standard$↔$explicit:

\msk

$\begin{array}{llll}
   & \text{(standard)} & & \text{(explicit)} \\[5pt]
   & \setofst{\ue{10a}}{\ug{a∈\{1,2,3,4\}}} &=&
       \{\ug{a∈\{1,2,3,4\}}; \ue{10a}\} \\
   & \setofst{\ue{a}}{\ug{a∈\{1,2,3,4\}}} &=&
       \{\ug{a∈\{1,2,3,4\}}; \ue{a}\} \\
   & \setofst{\ug{a∈\{1,2,3,4\}}}{\uf{a≥3}} &=&
       \{\ug{a∈\{1,2,3,4\}}, \uf{a≥3}; \ue{a}\} \\
   & \setofst{\ue{a}}{\ug{a∈\{1,2,3,4\}}, \uf{a≥3}} &=&
       \{\ug{a∈\{1,2,3,4\}}, \uf{a≥3}; \ue{a}\} \\
   & \setofst{\ue{10a}}{\ug{a∈\{1,2,3,4\}}, \uf{a≥3}} &=&
       \{\ug{a∈\{1,2,3,4\}}, \uf{a≥3}; \ue{10a}\} \\
   % & \{\ug{a∈\{10,20\}}, \ug{b∈\{3,4\}}; \ue{a+b}\} \\
   % & \{\ug{a∈\{1,2\}}, \ug{b∈\{3,4\}}; \ue{(a,b)}\} \\
\end{array}
$

\msk
\msk

In the ``g$|$f'' case the trick is that the ``expr''

is the variable of the generator... examples:

\msk

$\begin{array}{llll}
   & \text{(standard)} & & \text{(explicit)} \\[5pt]
   & \setofst{\ug{\uv{a}∈\{1,2,3,4\}}}{\uf{a≥3}} &=&
       \{\ug{a∈\{1,2,3,4\}}, \uf{a≥3}; \ue{a}\} \\
   & \setofst {\ug{\uv{(x,y)}∈\{1,2,3\}^2}} {\uf{x>y}} &=&
       \{\ug{(x,y)∈\{1,2,3\}^2}, \uf{x>y}; \ue{(x,y)}\} \\
 \end{array}
$

\bsk

{\bf Exercises}

\msk

$\begin{array}{rcl}
 A &:=& \{x∈\{0,1,2,3\}; (x,3-x)\}                  \\ % 2C
 B &:=& \{x∈\{1,2,3\}, y∈\{3,4\}; (x,y)\}          \\ % 2E
 C &:=& \{x∈\{3,4\}, y∈\{1,2,3\}; (y,x)\}          \\ % 2G
 D &:=& \{x∈\{3,4\}, y∈\{1,2,3\}; (x,2)\}          \\ % 2H
 E &:=& \{x∈\{1,2,3\}, y∈\{3,4\}, x+y>4; (x,y)\}   \\ % 2J
 F &:=& \{x,y∈\{0,1,2,3,4\}; (x,y)\}                \\ % 2L
 G &:=& \{x,y∈\{0,1,2,3,4\}, y=3; (x,y)\}           \\ % 2M
 H &:=& \{x,y∈\{0,1,2,3,4\}, x=2; (x,y)\}           \\ % 2N
 I &:=& \{x,y∈\{0,1,2,3,4\}, x+y=3; (x,y)\}         \\ % 2O
 J &:=& \{x,y∈\{0,1,2,3\};(x,y)\}                   \\ % 5A
 K &:=& \{x,y∈\{0,1,2,3\}, y=2; (x,y)\}             \\ % 5B
 L &:=& \{x,y∈\{0,1,2,3,4\}, y=2x; (x,y)\}          \\ % 5E
 M &:=& \{(x,y)∈\{0,1,2,3,4\}^2, y=2x; (x,y)\}      \\ % 5F
 \end{array}
$

\newpage

% «comprehension-3» (to ".comprehension-3")
% (laz162p 3 "comprehension-3")



$\begin{array}{rcl}
 N &:=& \setofst{(x,x)}{x∈\{0,1,2,3\}}              \\ % 3C
 O &:=& \setofst{(x,2)}{x∈\{0,1,2,3\}}              \\ % 3M
 P &:=& \setofst {(x,y)∈\{0,1,2,3,4\}^2} {y=2x}     \\ % 5J
 Q &:=& \setofst {(x,y)∈\{1,2,3\}^2} {0x+0y=0}      \\ % 5N
 R &:=& \setofst {(x,y)∈\{1,2,3\}^2} {0x+0y=2}      \\ % 5O
 S &:=& \setofst {(x,y)∈\{1,2,3\}^2} {x≥y}         \\ % 5P
 \end{array}
$




%$\picturepiecewise(-1,-2)(5,2){
%    (-2,1)--(2,1)c (2,-1)o--(3,-1)o (3,0)c--(6,0)
%  }
%$


% (find-angg ".emacs" "find-planarhas")
% (find-LATEX "2015planar-has.tex" "connectives")


\bsk
\bsk

\def∧{\mathbin{\&}}

$$\def\o#1{\mathop{\mathsf{#1}}}
  \def\o#1{\mathbin{\mathsf{#1}}}
  \def\a#1#2{\ang{#1,#2}}
  \def\ab{\a ab}
  \def\cd{\a cd}
  \begin{array}{rcl}
  %
  \ab ≤ \cd &:=& a≤c∧b≤d \\
  \ab ≥ \cd &:=& a≥c∧b≥d \\[5pt]
  %
  \ab \o{above} \cd &:=& a≥c∧b≥d \\
  \ab \o{below} \cd &:=& a≥c∧b≥d \\
  \ab \o{leftof} \cd &:=& a≥c∧b≤d \\
  \ab \o{rightof} \cd &:=& a≤c∧b≥d \\[5pt]
  %
  \o{ne}(\ab) &:=& \o{if}   \o{valid}(\a a{b+1})
                   \o{then} \o{ne}(\a a{b+1})
                   \o{else} \ab
                   \o{end} \\
  \o{nw}(\ab) &:=& \o{if}   \o{valid}(\a {a+1}b)
                   \o{then} \o{nw}(\a {a+1}b)
                   \o{else} \ab
                   \o{end} \\\\
  %
  \ab ∧ \cd &:=& \a{\o{min}(a,c)}{\o{min}(b,d)} \\
  \ab ∨ \cd &:=& \a{\o{max}(a,c)}{\o{max}(b,d)} \\[5pt]
  %
  \ab \to \cd &:=& \begin{array}[t]{llll}
               \o{if}     & \ab \o{below} \cd   & \o{then} & ⊤           \\
               \o{elseif} & \ab \o{leftof} \cd  & \o{then} & \o{ne}(\ab∧\cd) \\
               \o{elseif} & \ab \o{rightof} \cd & \o{then} & \o{nw}(\ab∧\cd) \\
               \o{elseif} & \ab \o{above} \cd   & \o{then} & \cd            \\
               \o{end}
               \end{array} \\\\
  %
  ⊥   &:=& \a00 \\
  ¬\ab &:=& \ab→⊥ \\
  \end{array}
$$



\end{document}

% Local Variables:
% coding: utf-8-unix
% ee-anchor-format: "«%s»"
% End:
