Glossary

Defined in this project

Every definition in this project that has a description, under its own name, with the first paragraph of it. The others are on their file pages. Theorems are not listed here: they are results, not words. There are too many for one page, so there is one page per first letter.

A (1025) · B (984) · C (2999) · D (834) · E (1088) · F (1426) · G (577) · H (665) · I (1087) · J (72) · K (112) · L (1029) · M (1165) · N (516) · O (702) · P (2155) · Q (191) · R (2352) · S (2596) · T (1425) · U (313) · V (289) · W (440) · X (16) · Y (12) · Z (81) · Other (4)

Implication edges

A dependency records which declarations a proof uses: the map and the “uses” lists show those, read from the code. An implication edge records what one result could establish about another, even when the released proof goes another way. It is a claim, so each one keeps its contract: the declarations it starts from and reaches, the exact hypotheses, the conclusion it derives, the commit the statements were read at, and how far it has been checked. The edges are curated beside the project, not written by its authors.

argued

Argued: the argument is written out below. Lean has not checked it.

Composes with

The sources together give the conclusion, and it needs each of them.

proposed

Proposed: someone suggested it. No argument is recorded, and nothing has checked it.

proved

Proved in Lean: the bridge declaration states the hypotheses and the conclusion, and proves them.

refuted

Refuted: the evidence below shows it does not hold as stated.

Specializes to

The target's statement is the source's general statement with particular values or in a narrower setting; the hypotheses say which.

Strengthens

From the sources and the hypotheses, the conclusion follows, and the conclusion gives the target's statement with more: an explicit constant, a weaker hypothesis, a wider range.

Supports an executable construction

The sources justify a computable definition, the target, and the conclusion says what it computes.

Terms from the explanations

Words defined in the explanations on this site (Lean4 Domain Explanation Language term lines). Where they appear, they link here.

affine copy

a translated and nonzero-rescaled set x+sA · OAI.Problem310.dyadic_affine_avoidance

affine maximal

satisfying the fourth-order equation that the cofactor-Hessian contracted with the Hessian of det(D2u)^(-(n+1)/(n+2)) vanishes · OAI.AffineBernstein.affine_bernstein

amenable group

a group admitting a positive normalized mean on bounded real functions that is unchanged by left translation · OAI.ThompsonNonamenability.thompson_F_nonamenable_composition

Artin group

a group presented by generators whose pairwise relations equate alternating words of lengths prescribed by a Coxeter matrix · OAI.ArtinCAT0.main

Catalan's constant

the special value β(2) = Σ(j ≥ 0) (-1)^j/(2j+1)^2 of the Dirichlet beta function · OAI.InternalCatalan.catalan_irrational

circle domain

a domain in the Riemann sphere whose complementary components are round closed disks or single points · OAI.Problem047.koebe_circle_domain

circulant matrix

a matrix in which every row is a cyclic shift of one common row · OAI.CirculantHadamard.exists_iff_order_one_or_four

clique minor

a family of disjoint connected vertex sets in a graph, every two of which have an edge between them · OAI.HadwigerCounterexample.not_hadwiger_conjecture

cohomological dimension

the projective dimension of the trivial integral module over the group's integral group ring · OAI.EilenbergGanea.source_main

Comparator challenge

a file that states a theorem with a sorry body so the Comparator tool can check that a separate solution module proves exactly that statement · OAI.riemannZeta_ne_zero_of_seven_eighths_lt_re

complete Crouzeix inequality

the Crouzeix norm bound required uniformly for matrix-valued, rather than only scalar-valued, polynomials · OAI.CompleteCrouzeix.main

conformally removable

a compact set outside which every orientation-preserving conformal sphere homeomorphism must already be Möbius everywhere · OAI.Problem047.removability_implies_rigidity

conformally rigid circle domain

a circle domain whose conformal equivalences to other circle domains are restrictions of Möbius transformations · OAI.Problem047.removability_implies_rigidity

coordinate polynomial

a polynomial that is the image of a coordinate variable under an automorphism of the ambient polynomial ring · OAI.AbhyankarSathaye.exists_noncoordinate_polynomial

cubic graph

a graph in which every vertex has degree three · OAI.Barnette.main

Dirichlet L-function

the analytic continuation of the Dirichlet series sum chi(n) n^(-s) attached to a Dirichlet character chi · OAI.DirichletCharacter.LFunction_ne_zero_of_seven_eighths_lt_re

dyadic piecewise-linear homeomorphism

an increasing interval homeomorphism with finitely many dyadic breakpoints and slopes that are integer powers of two · OAI.ThompsonNonamenability.thompson_F_nonamenable_composition

edge connectivity

the minimum number of graph edges crossing any nonempty proper vertex cut · OAI.AlgorithmicThinTrees.algorithmic_strong_thin_trees

Egyptian-fraction expansion

a representation of a positive rational number as a finite sum of distinct positive unit fractions · OAI.ShortEgyptian.main

Frobenius metric

Euclidean distance between matrices obtained from the square root of the sum of squared entries · OAI.BorsukNine.main_theorem

generalized amplitude-damping channel

a qubit noise channel modeling energy relaxation in contact with a thermal environment · OAI.GAD.main

geometric action

an isometric group action that is proper and cocompact · OAI.CannonRelease.cannon

geometric CAT(0) action

a proper and cocompact action by isometries on a nonempty proper CAT(0) metric space · OAI.ArtinCAT0.main

geometric dimension

the least dimension of a classifying CW space for the group · OAI.EilenbergGanea.source_main

Hadamard matrix

here, a sign-valued square matrix whose product with its transpose is its order times the identity · OAI.CirculantHadamard.exists_iff_order_one_or_four

Hadwiger-Nelson problem

the problem of finding the smallest number of colors needed so that points of the plane exactly one unit apart always have different colors · OAI.EuclideanFiveColor.no_proper_five_coloring

Hamiltonian cycle

one cycle that visits every vertex exactly once before returning to its start · OAI.Barnette.main

Holevo information

the entropy of an ensemble's average output minus the ensemble-average output entropy · OAI.GAD.main

hyperbolic-group boundary

asymptotic classes of geodesic rays in a Cayley graph, equipped with its boundary topology · OAI.CannonRelease.cannon

irrationality exponent

the supremum of exponents ν for which an irrational number has infinitely many rational approximations with error below q^(-ν) · OAI.PiExponent.main

Koopman operator

the operator on functions given here by composition with the measure-preserving transformation · OAI.ThreeTorus.simple_lebesgue_spectrum

Landau-Siegel zero

a hypothetical real zero of a Dirichlet L-function very close to 1 · OAI.SiegelZeros.WeightedTorusJets.exists_absolute_real_zero_gap

limit cycle

the image of a nonconstant periodic solution that is isolated among periodic-orbit images · OAI.QuinticLienard.main

mixing of order k

asymptotic factorization of every k-fold translated intersection when all consecutive time gaps diverge · OAI.Rokhlin.mixing_all_finite_orders

nodal set

the zero set of an eigenfunction · OAI.Yau.Target.yau_nodal_set_upper_bound_counterexample

numerical range

the set of scalar values $\langle x,Ax\rangle$ obtained from unit vectors $x$ · OAI.CompleteCrouzeix.main

oriented graph

a directed graph with no loops and no pair of oppositely directed edges · OAI.SeymourSecondNeighborhood.exists_goodVertex

polar body

the set of vectors p whose pairing with every point of K is at most 1 · OAI.SymmetricMahler.symmetric_mahler

Santaló point

the unique interior center that minimizes the volume of the translated polar body · OAI.GeneralMahler.general_mahler

second out-neighborhood

vertices at directed distance exactly two, excluding the starting vertex and its first out-neighbors · OAI.SeymourSecondNeighborhood.exists_goodVertex

simple Lebesgue spectrum

unitary equivalence to one copy of multiplication by the circle coordinate, rather than multiple spectral copies · OAI.ThreeTorus.simple_lebesgue_spectrum

strong thin tree

a spanning tree that crosses every cut using at most an $O(1/k)$ fraction of the original cut in a $k$-edge-connected graph · OAI.AlgorithmicThinTrees.algorithmic_strong_thin_trees

Unique Game

a constraint-satisfaction instance in which each edge constraint is a permutation, so either endpoint's label uniquely determines the satisfying label at the other endpoint · OAI.UniqueGamesTheorem.theorem11

unit sphere

the vectors of norm exactly one in a normed space · OAI.Tingley.tingley_sphere_isometry_full

volume product

the volume of a convex body multiplied by the volume of its polar at an optimizing interior center · OAI.GeneralMahler.general_mahler

zero fibre

the hypersurface obtained by imposing the equation F = 0, represented algebraically by quotienting by the ideal generated by F · OAI.AbhyankarSathaye.exists_noncoordinate_polynomial

Acronyms from the explanations

Explicit expansions supplied by acronym lines and repeated in each affected page's legend.

CAT

Cartan-Alexandrov-Toponogov · OAI.ArtinCAT0.main

CW

closure-finite weak topology · OAI.EilenbergGanea.source_main

GAD

generalized amplitude damping · OAI.GAD.main

Types

What kind of object something is. The Reading says these in words wherever they appear.

Bool

true or false

Equiv.Perm

Equiv.Perm α — a permutation (reordering) of α

EReal

a real number or ±∞

EuclideanSpace

EuclideanSpace ℝ (Fin n) — a point in n-dimensional space

Fin

Fin n — a number from 0 up to n − 1

Finset

Finset α — a finite set of elements of α

Ideal

Ideal R — a ideal (Ideal R)

IntermediateField

IntermediateField K L — a intermediate field (IntermediateField K L)

List

List α — a list of elements of α

Matrix

Matrix m n R — a matrix with rows m, columns n and entries in R

Measure

Measure α — a measure on α (a way to give sets a size)

Multiset

Multiset α — a finite collection of elements of α, repeats allowed

Option

Option α — either nothing or an element of α

Polynomial, R[X]

Polynomial R — a polynomial with coefficients in R

Prop

a statement (something true or false)

Set

Set α — a set of elements of α

SimpleGraph

SimpleGraph V — a graph whose vertices are the elements of V

String

a piece of text

Subfield

Subfield K — a subfield (Subfield K)

Subgroup

Subgroup G — a subgroup (Subgroup G)

Submodule

Submodule R M — a submodule (Submodule R M)

Subring

Subring R — a subring (Subring R)

Type, Type*, Type _, Type u, Type v, Sort*

a type (a collection of objects)

ZMod

ZMod n — an integer modulo n

× (pair type)

α × β — a pair (α, β)

ℂ, Complex

a complex number

ℕ+

a positive whole number

ℕ, Nat

a natural number (0, 1, 2, …)

ℚ, Rat

a rational number (a fraction)

ℝ, Real

a real number

ℝ≥0, NNReal

a real number that is at least 0

ℝ≥0∞, ENNReal

a number from 0 to ∞, ∞ included

ℤ, Int

an integer

→ (function type)

α → β — a function that takes α and gives β

Structures a type can have

Written in square brackets, such as [Field K]. Lean finds them by itself (they are type classes).

AddCommGroup

[AddCommGroup G] — G is a commutative group under addition

AddGroup

[AddGroup G] — G is a group under addition

CharZero

[CharZero α] — in α, 1 + 1 + … + 1 is never 0

CommGroup

[CommGroup G] — G is a commutative group

CommRing

[CommRing R] — R is a commutative ring: you can add, subtract and multiply, and order of multiplication does not matter

CommSemiring

[CommSemiring R] — R has addition and commutative multiplication

Countable

[Countable α] — α is countable

DecidableEq

[DecidableEq α] — equality between elements of α can be checked

DecidablePred

[DecidablePred p] — whether p holds can be checked

Fact

[Fact (Nat.Prime p)] — it is known that Nat.Prime p

Field

[Field K] — K is a field: you can add, subtract, multiply and divide (except by 0)

Finite

[Finite α] — α has finitely many elements

Fintype

[Fintype α] — α has finitely many elements

Group

[Group G] — G is a group: you can multiply and undo multiplication

Inhabited

[Inhabited α] — α has a chosen default element

InnerProductSpace

[InnerProductSpace ℝ E] — E has angles and lengths (an inner product)

LinearOrder

[LinearOrder α] — any two elements of α can be compared

MeasurableSpace

[MeasurableSpace X] — X has measurable sets

MetricSpace

[MetricSpace X] — X has a distance between any two points

Module

[Module R M] — M is a module (a vector space when the scalars form a field)

Monoid

[Monoid M] — M has a multiplication with a 1

NeZero

[NeZero n] — n is not 0

Nonempty

[Nonempty α] — α has at least one element

Nontrivial

[Nontrivial α] — α has at least two different elements

NormedAddCommGroup

[NormedAddCommGroup E] — E has a length (norm) for its elements

NormedSpace

[NormedSpace ℝ E] — E is a vector space with lengths

PartialOrder

[PartialOrder α] — α has an order (some pairs may be incomparable)

Ring

[Ring R] — R is a ring: you can add, subtract and multiply

Semiring

[Semiring R] — R has addition and multiplication

TopologicalSpace

[TopologicalSpace X] — X has a notion of nearness (open sets)

Properties

Statements about functions, numbers and sets that the Reading puts in words, each shown on a sample use.

AEMeasurable

AEMeasurable f — f is measurable, apart from a set of measure zero

AEStronglyMeasurable

AEStronglyMeasurable f — f is (strongly) measurable, apart from a set of measure zero

Antitone

Antitone f — f never increases

BddAbove

BddAbove S — S is bounded above

BddBelow

BddBelow S — S is bounded below

Bijective

Bijective f — f is a bijection: a perfect one-to-one pairing

BijOn

BijOn f s t — f pairs s one-to-one with t

Collinear

Collinear ℝ S — the points S lie on one line

Colorable

Colorable G n — the graph can be colored with n colors so that neighbors get different colors

Commute

Commute a b — a and b commute: their product is the same in either order

Computable

Computable f — f is computable

ConcaveOn

ConcaveOn ℝ s f — f is concave on s: its graph bends downward

ContDiff

ContDiff ℝ n f — f is smooth: it can be differentiated n times, continuously

ContDiffAt

ContDiffAt ℝ n f x — f is smooth at x

Continuous

Continuous f — f is continuous: no jumps or breaks

ContinuousAt

ContinuousAt f x — f is continuous at x

ContinuousOn

ContinuousOn f s — f is continuous on s

ContinuousWithinAt

ContinuousWithinAt f s x — f is continuous at x within s

Convex

Convex ℝ s — s is convex: it contains the segment between any two of its points

ConvexOn

ConvexOn ℝ s f — f is convex on s: its graph bends upward

Coprime

Coprime a b — a and b are coprime: no common factor bigger than 1

Countable

Countable S — S is countable

Dense

Dense S — S is dense: it comes arbitrarily close to every point

Differentiable

Differentiable ℝ f — f is differentiable: it has a derivative everywhere

DifferentiableAt

DifferentiableAt ℝ f x — f has a derivative at x

DifferentiableOn

DifferentiableOn ℝ f s — f has a derivative at every point of s

Disjoint

Disjoint s t — s and t have nothing in common

Even

Even n — n is even

Finite

Finite S — S is finite

HasDerivAt

HasDerivAt f f' x — f has derivative f' at x

HasSum

HasSum a s — the terms a add up to s

IdentDistrib

IdentDistrib X Y — X and Y have the same distribution

iIndepFun

iIndepFun m X μ — the random variables X are independent

IndepFun

IndepFun X Y — the random variables X and Y are independent

Infinite

Infinite S — S is infinite

Injective

Injective f — f is injective: different inputs always give different outputs

InjOn

InjOn f s — f is injective on s: different inputs there give different outputs

Integrable

Integrable f — f is integrable (its integral is finite)

IntegrableOn

IntegrableOn f s — f is integrable on s

IntervalIntegrable

IntervalIntegrable f volume a b — f can be integrated from a to b

Involutive

Involutive f — applying f twice gives back the input

Irrational

Irrational x — x is irrational: not a fraction of two integers

Irreducible

Irreducible p — p is irreducible: it cannot be factored into smaller non-units

IsAlgebraic

IsAlgebraic ℤ x — x is algebraic: a root of a nonzero polynomial

IsBigO

IsBigO l f g — f is at most a constant times g (big O)

IsClosed

IsClosed F — F is a closed set

IsCompact

IsCompact K — K is compact (closed and bounded, in ℝⁿ)

IsConnected

IsConnected S — S is connected: it is all in one piece

IsCoprime

IsCoprime a b — a and b are coprime

IsGLB

IsGLB S m — m is the greatest lower bound of S

IsGreatest

IsGreatest S m — m is the greatest element of S

IsLeast

IsLeast S m — m is the least element of S

IsLittleO

IsLittleO l f g — f is negligible compared with g (little o)

IsLUB

IsLUB S m — m is the least upper bound of S

IsOpen

IsOpen U — U is an open set

IsProbabilityMeasure

IsProbabilityMeasure μ — μ is a probability measure: the whole space has size 1

IsSquare

IsSquare n — n is a perfect square

IsUnit

IsUnit a — a has a multiplicative inverse

LeftInverse

LeftInverse g f — g undoes f: applying f then g gives back the input

LinearIndependent

LinearIndependent K v — the vectors v are linearly independent

LipschitzWith

LipschitzWith K f — f never stretches distances by more than a factor K

MapsTo

MapsTo f s t — f sends every element of s into t

Measurable

Measurable f — f is measurable

MeasurableSet

MeasurableSet S — S is a measurable set (one that has a size)

MeasurePreserving

MeasurePreserving f — f preserves the measure: sets keep their size

MemLp

MemLp f p — f is in Lᵖ for p = p (the p-th power of |f| has a finite integral)

Monotone

Monotone f — f never decreases: a bigger input gives an output at least as big

MonotoneOn

MonotoneOn f s — f never decreases on s

Nonempty

Nonempty S — S is not empty

Odd

Odd n — n is odd

Pairwise

Pairwise r — every two different elements are related by r

Periodic

Periodic f c — f repeats every c

Perm

Perm l₁ l₂ — l₁ is a rearrangement of l₂

Prime

Prime p — p is a prime number

Primrec

Primrec f — f is primitive recursive (computable by a simple kind of program)

Reachable

Reachable u v — there is a path from u to v

RightInverse

RightInverse g f — g is a right inverse of f

Sbtw

Sbtw ℝ x y z — y lies strictly between x and z

Squarefree

Squarefree n — n is squarefree: no square bigger than 1 divides it

StrictAnti

StrictAnti f — f is strictly decreasing

StrictMono

StrictMono f — f is strictly increasing: a bigger input gives a bigger output

StronglyMeasurable

StronglyMeasurable f — f is strongly measurable

Summable

Summable a — the series of the terms a adds up to a finite value

Surjective

Surjective f — f is surjective: every possible output is reached

SurjOn

SurjOn f s t — f maps s onto all of t

Tendsto

Tendsto f atTop (𝓝 0) — f tends to 0 as the input grows without bound

Transcendental

Transcendental ℤ x — x is transcendental: not a root of any nonzero polynomial with integer coefficients

UniformContinuous

UniformContinuous f — f is uniformly continuous

Wbtw

Wbtw ℝ x y z — y lies between x and z

Symbols

Notation a newcomer may not know. A Reading lists the ones its statement uses.

#s, card

the number of elements

%

remainder after division

.Finite

the set has finitely many elements

.Infinite

the set has infinitely many elements

/

division; on ℕ and ℤ it rounds down

^

a power

A × B

pairs (a, b) with a from A and b from B

answer(…)

marks the answer the problem asks for; answer(sorry) means the answer is not filled in

atTop

“as the input goes to infinity”

choose

binomial coefficient: the number of ways to pick k things from n

deriv

the derivative

exp

the exponential function eˣ

f '' s

the image: all outputs f gives on s

f =O[l] g

big O: f is at most a constant times g, along l

f =o[l] g

little o: f is negligible compared with g, along l

f ⁻¹' s

the preimage: all inputs that f sends into s

f ∘ g

composition: first g, then f

f ≪ g

f is at most a constant times g (for large inputs)

Finset.range n

the numbers 0, 1, …, n − 1

fun x ↦ …

a function: send x to …

gcd

greatest common divisor

lcm

least common multiple

log

the natural logarithm

n !

factorial: 1 · 2 · … · n

Set.Icc a b

the closed interval [a, b]

Set.Ioo a b

the open interval (a, b)

sᶜ

the complement: everything not in s

x⁻¹

the inverse, 1 / x for numbers

{x | p x}

the set of all x with property p

|x|

absolute value

¬

“not”

π

pi

‖x‖

the norm (length) of x

ℂ

the complex numbers

ℕ

the natural numbers 0, 1, 2, … (in Lean ℕ starts at 0)

ℚ

the rational numbers (fractions)

ℝ

the real numbers

ℤ

the integers …, −2, −1, 0, 1, 2, …

↑x

x viewed in a bigger number system, such as a natural number as a real number

→

“implies”, or for functions “to”

↔

“if and only if”: both directions hold

∀

“for every”

∃

“there exists”

∃!

“there is exactly one”

∏

a product over a range or a finite set

∑

a sum over a range or a finite set

√

square root

∣

“divides”: a ∣ b means b is a multiple of a

∧

“and”

∨

“or”

∩

intersection: what both sets have in common

∪

union: everything in either set

∫

an integral

≡ [MOD n]

same remainder when divided by n

⌈x⌉

ceiling: the smallest integer at least x

⌊x⌋

floor: the largest integer at most x

𝓝 x

“near x”: used for limits

Tactics

Steps inside a proof that starts with by. Each says what the tactic does in general; the goal it leaves depends on the proof.

abel

Both sides are equal by rearranging sums (abel: algebra in commutative groups).

absurd

absurd h h' — Two facts contradict each other: h h'.

admit

Not proved yet: admit is a placeholder, so this proof is unfinished.

aesop

Search automatically for a proof using many small rules (aesop).

all_goals

all_goals simp — On every remaining goal: Simplify with Lean's standard simplification rules.

and_intros

Split the “and” goal into its parts.

any_goals

any_goals simp — On every goal where it works: Simplify with Lean's standard simplification rules.

apply

apply h — Work backwards with h: it gives the goal once its own conditions hold, so those conditions become the new goals.

apply_fun

apply_fun f at h — Apply f to both sides in h.

assumption

The goal is exactly one of the assumptions.

bound

Prove the bound by combining standard inequalities.

by_cases

by_cases h : x = 0 — Split into two cases: x = 0 is true, or it is false.

by_contra

Proof by contradiction: assume the opposite and reach something false.

by_contra!

Proof by contradiction, with the assumed opposite already simplified.

calc

A chain of steps, each one justified on its own line.

case

case zero => simp — The case zero.

cases

cases h — Split into cases on how h can be built.

cases'

cases' h with x hx — Split into cases on how h can be built.

change

change a + 0 = a — Restate the goal as a + 0 = a (the same thing, written differently).

choose

choose f hf using h — From “for every x there is a y”, pick a function giving such a y: f hf using h.

classical

Allow classical reasoning from here on (every statement is true or false, even if we cannot compute which).

clear

clear h — Forget the assumptions h; they are not needed any more.

congr

Reduce to showing the matching parts of both sides are equal.

constructor

constructor function Object() { [native code] } — Split the goal into its parts: for “A and B” prove A and B, for “A iff B” prove both directions.

constructorm

Split every “and”-like assumption or goal into its parts.

continuity

Built automatically from the rules for continuous functions.

contradiction

Two assumptions contradict each other, so this case is done.

contrapose

Prove the contrapositive: if the conclusion fails, then so does the assumption.

contrapose!

Prove the contrapositive, with the negations pushed inward.

conv

Rewrite inside one chosen part of the goal.

conv_lhs

Rewrite inside the left-hand side only.

conv_rhs

Rewrite inside the right-hand side only.

convert

convert h using 1 — Close the goal with h, which almost matches; any differences become new goals.

decide

Lean checks it by direct computation (decide).

delta

delta f — Expand the definition of f.

dsimp

Simplify by unfolding definitions.

erw

erw [h] — Rewrite using h, matching up to unfolding definitions.

exact

exact h — Finish: h is exactly what is needed.

exact_mod_cast

exact_mod_cast h — Finish with h, ignoring conversions between number systems.

exacts

exacts [h₁, h₂] — Finish each remaining goal with [h₁, h₂].

exfalso

Switch to proving False: this case is impossible.

exists

exists 2 — Give 2 as the example that exists.

existsi

existsi 2 — Give 2 as the example that exists.

ext

Two functions (or sets) are equal when they agree at every input.

ext1

Two functions (or sets) are equal when they agree at every input.

field

Both sides are equal by algebra with division (field).

field_simp

Clear the denominators.

filter_upwards

Reduce a statement about “eventually” or “almost everywhere” to one about each point.

fin_cases

fin_cases i — Try each of the finitely many values of i, one case each.

finiteness

The quantity is finite (not ∞), checked automatically (finiteness).

first

first | simp | ring — Try these in order until one works: simp, ring

focus

Work on the first goal only.

fun_prop

Built automatically from the rules for continuity, differentiability or measurability (fun_prop).

funext

Two functions are equal when they agree at every input.

gcongr

Compare the two sides piece by piece: if each part on the left is at most the matching part on the right, so is the whole (gcongr).

generalize

generalize e : f x = y — Replace a specific expression by a general variable: e : f x = y.

grind

Automated reasoning that combines equalities, cases and arithmetic (grind).

group

Both sides are equal by the rules of a group (group).

grw

grw [h] — Rewrite with an inequality (or another relation) instead of an equation: h.

have

have h : 0 < 2 := by norm_num — Establish an intermediate fact h: 0 is less than 2. Proved by: Do the arithmetic: norm_num proves number facts such as 2 + 2 = 4, 7 ≠ 0 or that 13 is prime.

have'

have' h : 0 < 2 := by norm_num — Establish an intermediate fact h: 0 is less than 2. Proved by: Do the arithmetic: norm_num proves number facts such as 2 + 2 = 4, 7 ≠ 0 or that 13 is prime.

haveI

haveI h : 0 < 2 := by norm_num — Establish an intermediate fact h: 0 is less than 2. Proved by: Do the arithmetic: norm_num proves number facts such as 2 + 2 = 4, 7 ≠ 0 or that 13 is prime.

if

Split on a condition, if-then-else.

induction

induction n with — Prove it by induction on n: first a starting case, then a step from each case to the next.

induction'

induction' n with n ih — Prove it by induction on n: a starting case, then the step to the next case.

infer_instance

Lean finds this automatically from known structures.

interval_cases

interval_cases n — Try every possible value of n in its known range, one case each.

intro

Move the next variable or assumption of the goal into view.

intros

Introduce everything the goal starts with.

left

Prove the left side of the “or”.

let

let y := x + 1 — Give a name to a value: y := x + 1.

letI

letI inst := Classical.decEq α — Give a name to a structure for Lean to use: inst := Classical.decEq α.

lia

Whole-number arithmetic, decided automatically (lia: linear integer arithmetic).

lift

lift n to ℕ using hn — Treat n to ℕ using hn as a value of a smaller number system, since it is known to fit.

linarith

It follows by adding up the linear inequalities in the assumptions (linarith).

linear_combination

linear_combination h₁ - h₂ — The goal is exactly this combination of the assumptions: h₁ - h₂.

match

match n with — Split on the shape of n, one case per pattern.

measurability

Built automatically from the rules for measurable functions.

module

Both sides are equal by algebra with vectors and scalars (module).

native_decide

Checked by running compiled code (native_decide). This also trusts the compiler, an extra axiom.

next

The next case.

nlinarith

Like linarith, but also multiplies assumptions together, which handles squares and products.

nofun

No case can occur, so there is nothing to prove.

nomatch

nomatch h — No case of h can occur.

noncomm_ring

Both sides are equal by algebra where multiplication need not commute (noncomm_ring).

norm_cast

Move the statement between number systems (ℕ, ℤ, ℚ, ℝ) to where it is simplest.

norm_num

Do the arithmetic: norm_num proves number facts such as 2 + 2 = 4, 7 ≠ 0 or that 13 is prime.

norm_num1

Do the arithmetic.

nth_rewrite

nth_rewrite 2 [h] — Rewrite one chosen occurrence using h.

nth_rw

nth_rw 2 [h] — Rewrite one chosen occurrence using h.

obtain

obtain ⟨x, hx⟩ := h — Unpack h into its pieces ⟨x, hx⟩.

omega

Whole-number arithmetic with +, −, constants and comparisons, decided automatically (omega).

on_goal

on_goal 2 => simp — On one chosen goal: 2 => simp.

order

It follows from the order facts in the assumptions (order).

peel

peel h with x hx — Strip matching quantifiers from both sides: h with x hx.

polyrith

The goal is a combination of the equations in the assumptions (polyrith).

positivity

The expression is positive (or at least 0), checked term by term (positivity).

push

Push the operation inward.

push_cast

Push the number-system conversions (↑) inward.

push_neg

Push the “not” inward: not-for-every becomes there-is-a-counterexample, and so on.

qify

Move the statement to ℚ, where division behaves normally.

rcases

rcases h with ⟨x, hx⟩ — Unpack h into its pieces ⟨x, hx⟩, one case per alternative.

refine

refine ⟨?_, ?_⟩ — Fill in the goal with ⟨?_, ?_⟩; every ?_ hole becomes a new goal.

refine'

refine' ⟨_, _⟩ — Fill in the goal with ⟨_, _⟩; every _ hole becomes a new goal.

rename_i

rename_i x y — Name the unnamed variables x, y.

repeat

repeat rw [h] — Repeat as long as it works: Rewrite using h.

replace

replace h : 0 < x := by linarith — Replace an assumption with a stronger form: the fact h: 0 is less than x. Proved by: It follows by adding up the linear inequalities in the assumptions (linarith).

revert

revert x — Put x back into the goal, so the goal is about every possible value of it.

rewrite

rewrite [h] — Rewrite using h.

rfl

Both sides are the same by definition (rfl).

right

Prove the right side of the “or”.

ring

Both sides are equal by algebra: expand and collect like terms (ring).

ring_nf

Put the expressions into a standard algebraic form.

rintro

rintro ⟨x, hx⟩ — Introduce and unpack in one go: ⟨x, hx⟩.

rotate_left

Change the order of the goals.

rw

rw [h] — Rewrite using h.

rwa

rwa [h] at h₁ — Rewrite using h in h₁, and then the goal is one of the assumptions.

set

set y := x + 1 with hy — Give a name to an expression and use the name from now on: y := x + 1.

show

show a + 0 = a — Restate the goal as a + 0 = a.

simp

Simplify with Lean's standard simplification rules.

simp_all

Simplify the goal and all the assumptions together.

simp_arith

Simplify, including arithmetic on natural numbers.

simp_rw

simp_rw [h] — Rewrite using h, also inside “for every” and “there is”.

simpa

Simplify, and the goal closes.

sorry

Not proved yet: sorry is a placeholder, so this proof is unfinished.

specialize

specialize h 2 — Use the assumption h for the specific 2.

split

Split into one case for each branch of the if-then-else or match.

split_ifs

Split into a case for each branch of every if-then-else.

subst

subst h — Replace h by what it equals, everywhere.

suffices

suffices h : 0 < x by linarith — It is enough to prove 0 < x; that is shown next, then used to finish.

swap

Work on the second goal first.

symm

Swap the two sides.

tauto

Pure logic: it follows from the assumptions by the rules of and, or, not and implies (tauto).

trans

trans b — Go through a middle point b.

trivial

This goal is immediate.

try

try linarith — Try this, and carry on if it fails: It follows by adding up the linear inequalities in the assumptions (linarith).

unfold

unfold f — Expand the definition of f.

use

use 2 — Give 2 as the example that exists; what remains is to check it works.

wlog

wlog h : a ≤ b with H — Without loss of generality, h : a ≤ b; the other case follows the same way.

zify

Move the statement from ℕ to ℤ, where subtraction behaves normally.

Lean words

Words of the Lean language itself, and of how its projects are organized.

#check, #eval

#eval 2 + 2 — Commands that ask Lean a question while you write: the type of a term, or its value.

:=

def two : ℕ := 2 — “is defined as” or “is proved by”: what comes after it is the value or the proof.

@[simp] (attribute)

@[simp] theorem add_zero' (n : ℕ) : n + 0 = n := rfl — Attributes add information to a declaration: @[simp] tells the simp tactic to use it.

_ and ?_

refine ⟨?_, ?_⟩ — A hole: Lean fills in _ by itself, and ?_ becomes a new goal to prove.

abbrev

abbrev Point := ℝ × ℝ — A definition that Lean unfolds freely, like a shorthand.

anonymous constructor ⟨ ⟩

⟨2, by norm_num⟩ — Builds an object from its parts: a pair, a structure, or a proof of “and” or “there exists”.

axiom

axiom my_assumption : 1 = 1 — Something assumed without proof. Lean's three standard axioms (propext, Classical.choice, Quot.sound) are normal; anything beyond them is worth a closer look.

by

theorem t : 1 + 1 = 2 := by norm_num — Starts a proof made of tactics.

class

class Zero (α : Type) where zero : α — A structure that Lean finds by itself when it is needed (a type class), such as “this type has an addition”.

class inductive

class inductive Decidable (p : Prop) — A class given by the ways to build it, like inductive.

declaration

Any named thing in Lean: a theorem, a definition, and so on. Each one has a line on its file page.

def (definition)

def double (n : ℕ) : ℕ := 2 * n — A name for a precise idea or a computation, such as “continuous” or “double a number”.

dot notation

n.succ — x.foo means Foo.foo x, where Foo is the type of x: n.succ is Nat.succ n.

example

example : 2 + 2 = 4 := rfl — A statement proved without a name, to show that something works.

explicit argument ( )

(n : ℕ) — An argument you write when you use the result.

goal

What is left to prove at a point in a proof. Each tactic changes the goal.

h.1, h.2

h.1 — The first and second part of h, for example of an “and”.

hypothesis (assumption)

(h : 0 < n) — A named fact you may use in a proof, such as h : 0 < n.

implicit argument { }

{α : Type} — An argument Lean works out by itself from the others.

import

import Mathlib.Data.Real.Basic — Brings in the declarations of another file or library.

inductive

inductive Color | red | green — A new type given by the ways to build its elements. The natural numbers are 0, or one more than a natural number.

instance

instance : Zero ℕ := ⟨0⟩ — A proof or construction that a type belongs to a class. Lean then finds it by itself.

instance argument [ ]

[Field K] — An argument Lean finds by itself among the class instances it knows.

kernel

The small core of Lean that finally accepts or rejects a proof.

Lake

lake build — Lean's build tool. A project's lakefile says which libraries it has and which it needs.

lemma

lemma helper (n : ℕ) : n ≤ n + 1 := by omega — A theorem, usually a smaller helper for a bigger one.

Mathlib

import Mathlib — The big shared library of formalized mathematics that many Lean projects build on.

namespace

namespace Nat … end Nat — A family name for declarations: inside namespace Nat, succ_le means Nat.succ_le.

noncomputable

noncomputable def half : ℝ := 1 / 2 — Marks a definition Lean cannot run as a program, usually because it uses choice or real numbers.

opaque

opaque secret : ℕ — A definition whose value Lean keeps hidden: only its type is known.

open

open Real — Lets you use short names: after open Real, pi means Real.pi.

private, protected

private theorem helper : True := trivial — private: usable only in this file. protected: must always be written with its full name.

proof

The argument. In Lean, a proof is code, and Lean checks every step of it.

Prop

(p : Prop) — The type of statements. A statement is true or false; its proofs are its elements.

section

section … end — A part of a file whose variables and open commands end with it.

sorry

theorem later : 1 = 1 := sorry — Lean's “I have not proved this yet”. A result that uses it is not finished, and the site flags it.

structure

structure Point where x : ℝ y : ℝ — A new kind of object made of named parts (its fields).

tactic

by rw [h] ring — One command inside a proof that starts with by, such as “rewrite using this equation”. The Reading explains each one.

termination_by

termination_by n — Says why a recursive definition stops: something gets smaller each time.

theorem

theorem two_pos : 0 < 2 := by norm_num — A statement that has been proved. The proof follows :=.

universe

universe u — The size level of types (Type u). You can usually ignore it.

variable

variable (n : ℕ) (hn : 0 < n) — Names (and assumptions) used by every result below it, until its section ends.

· (focusing dot)

constructor · norm_num · simp — Starts the proof of one goal when there are several.