\(
\DeclareMathOperator{\tr}{tr}
\newcommand\D{\mathrm{d}}
\newcommand\E{\mathrm{e}}
\newcommand\I{\mathrm{i}}
\newcommand\bigOh{\mathcal{O}}
\newcommand{\cat}[1]{\mathbf{#1}}
\newcommand\curl{\vec{\nabla}\times}
\newcommand{\CC}{\mathbb{C}}
\newcommand{\NN}{\mathbb{N}}
\newcommand{\QQ}{\mathbb{Q}}
\newcommand{\RR}{\mathbb{R}}
\newcommand{\ZZ}{\mathbb{Z}}
% For +---- metric
\newcommand{\BDpos}{}
\newcommand{\BDneg}{-}
\newcommand{\BDposs}{\phantom{-}}
\newcommand{\BDnegg}{-}
\newcommand{\BDplus}{+}
\newcommand{\BDminus}{-}
% For -+++ metric
\newcommand{\BDpos}{-}
\newcommand{\BDposs}{-}
\newcommand{\BDneg}{}
\newcommand{\BDnegg}{\phantom{-}}
\newcommand{\BDplus}{-}
\newcommand{\BDminus}{+}
\)
"Element of" - Mizar
It's possible to write things like let x be Element of {} in
Mizar. This isn't a typing error, arguably, since {} is a term whose
type is set. I believe later on, in the CHECKER, it's treated as it
(logically) should.
Last Updated: Wed, 25 May 2022 12:14:58 -0700