Symbols¶

Every symbol used in these notes that is not on a standard keyboard, with the abbreviation that types it and what it means in Lean. In either editor a backslash starts an abbreviation, and most symbols have several spellings; the one given is the shortest.

Logic¶

These symbols build statements.

Symbol	Type	Meaning	First used
`∀`	`\all`	for all	4
`∃`	`\ex`	there exists	how-to
`→`	`\to`	function type, and implication between statements	2
`↔`	`\iff`	if and only if	explanation
`∧`	`\and`	and	5
`∨`	`\or`	or	5
`¬`	`\not`	not; `¬ P` means `P → False`	5

Order and equality¶

These compare two values of the same type.

Symbol	Type	Meaning	First used
`≤`	`\le`	less than or equal to	5
`≠`	`\ne`	not equal; `a ≠ b` means `¬ (a = b)`	5

The symbols <, > and = are on the keyboard.

Types¶

These name types of numbers.

Symbol	Type	Meaning	First used
`ℝ`	`\R`	the real numbers, from Mathlib	1
`ℕ`	`\N`	the natural numbers, from Lean	explanation

The symbol ∑, typed \sum, is a finite sum, as in ∑ first, f first, the sum of f over every value of first. It is first used in Define expected payoffs for mixed strategies.

Proof structure¶

These appear in proofs and in the infoview.

Symbol	Type	Meaning	First used
`⊢`	`\vdash`	separates the context from the goal; appears in the infoview	3
`·`	`\.`	focuses on the first remaining goal	4
`⟨` `⟩`	`\<` `\>`	builds or takes apart a pair, such as the parts of an `∧`	6
`✝`	not typed	marks a hypothesis that has no usable name	6

Unknown abbreviations¶

When a symbol is on the screen but its abbreviation is unknown, Neovim's :LeanAbbreviationsReverseLookup, or \\ with the cursor on the symbol, lists the abbreviations that produce it. In VS Code, ⌘⌥\ on macOS or Ctrl+Alt+\ elsewhere opens a searchable list of symbols to insert.