\( \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}} \)
UP | HOME

Schemes - Mizar

Table of Contents

1. Overview

In programming, there's this idea of DRY code ("don't repeat yourself"), where we carve out helper functions if the exact sequence of code is repeated twice or more. In mathematics, we have this idea too, where we abstract away a predicate or functor. We call them "schemes".

For example, if we have a family of subgroups satisfying "some property" \(\{H\leq G : P[H]\}\), then the intersection of all these subgroups forms another subgroup. This is a scheme (namely, MeetSbgEx found in GROUP_4).

Last Updated 2022-02-14 Mon 14:50.