Code

Minor shortenings, moving, cleaning#4603

Code

Merged

benjub merged 2 commits intometamath:developmetamath/set.mm:developfrom benjub:miscbenjub/set.mm:miscCopy head branch name to clipboardJan 25, 2025

+67-46

Commits

Commits on Jan 25, 2025

• Shorten snexg and bj-abex. Typos.

  benjub

  committed
  9673326

  Copy full SHA for 9673326

• Move two theorems out of Section 'Theorems requiring empty set existence' when they do not require it. Add cross-links and clarify comments.

  benjub

  committed
  2e5b088

  Copy full SHA for 2e5b088