Glossary

Defined in this project

Every definition in this project, under its own name: the first paragraph of its description, or how it is declared when it has none. Theorems are not listed here: they are results, not words.

A · B · C · D · E · F · G · I · L · M · N · O · P · R · S · T · V · W · Z

A

add def

def add (a b : Point) : Point · C06S01.Point.add

add def

def add (a b : Point) : Point · C06S02.Point.add

add def

def add : MyNat → MyNat → MyNat · MyNat.add

add' def

def add' (a b : Point) : Point · C06S01.Point.add'

addAlt def

def addAlt : Point → Point → Point · C06S01.Point.addAlt

addAlt' def

def addAlt' : Point → Point → Point · C06S01.Point.addAlt'

AddCommGroup₃ class

class AddCommGroup₃ (G : Type) extends AddGroup₃ G, AddCommMonoid₃ G @[to_additive AddCommGroup₃] · AddCommGroup₃

AddCommMonoid₃ class

class AddCommMonoid₃ (α : Type) extends AddMonoid₃ α, AddCommSemigroup₃ α @[to_additive AddCommMonoid₃] · AddCommMonoid₃

AddCommSemigroup₃ class

class AddCommSemigroup₃ (α : Type) extends AddSemigroup₃ α · AddCommSemigroup₃

addGroupPoint def

def addGroupPoint : AddGroup₁ Point · C06S02.Point.addGroupPoint

AddGroup₁ structure

structure AddGroup₁ (α : Type*) · C06S02.AddGroup₁

AddGroup₂ class

class AddGroup₂ (α : Type*) · C06S02.AddGroup₂

AddGroup₃ class

class AddGroup₃ (G : Type) extends AddMonoid₃ G, Neg G · AddGroup₃

AddMonoidHom₁ structure

structure AddMonoidHom₁ (G H : Type) [AddMonoid G] [AddMonoid H] · AddMonoidHom₁

AddMonoid₃ class

class AddMonoid₃ (α : Type) extends AddSemigroup₃ α, AddZeroClass α @[to_additive AddMonoid₃] · AddMonoid₃

AddMonoid₄ class

class AddMonoid₄ (M : Type) extends AddSemigroup₃ M, AddZeroClass M · AddMonoid₄

AddSemigroup₃ class

class AddSemigroup₃ (α : Type) extends Add α · AddSemigroup₃

append def

def append {α : Type*} : List α → List α → List α · MyListSpace2.append

B

badInst def

def badInst [Monoid M] [Monoid N] [MonoidHomClass₁ F M N] : CoeFun F (fun _ ↦ M → N) · badInst

BinTree inductive

inductive BinTree · BinTree

C

CayleyIsoMorphism def

def CayleyIsoMorphism (G : Type*) [Group G] : G ≃* (toPermHom G G).range · CayleyIsoMorphism

chineseIso def

def chineseIso [Fintype ι] (f : ι → Ideal R) (hf : ∀ i j, i ≠ j → IsCoprime (f i) (f j)) : (R ⧸ ⨅ i, f i) ≃+* Π i, R ⧸ f i · chineseIso

chineseMap def

The homomorphism from R ⧸ ⨅ i, I i to Π i, R ⧸ I i featured in the Chinese Remainder Theorem. · chineseMap

circleEquation def

def circleEquation : MvPolynomial (Fin 2) ℝ · circleEquation

CommGroup₃ class

class CommGroup₃ (G : Type) extends Group₃ G, CommMonoid₃ G · CommGroup₃

CommMonoid₃ class

class CommMonoid₃ (α : Type) extends Monoid₃ α, CommSemigroup₃ α · CommMonoid₃

CommSemigroup₃ class

class CommSemigroup₃ (α : Type) extends Semigroup₃ α · CommSemigroup₃

conj def

def conj (x : GaussInt) : GaussInt · GaussInt.conj

conjugate def

def conjugate {G : Type*} [Group G] (x : G) (H : Subgroup G) : Subgroup G · conjugate

ConvergesTo def

A sequence converges to a if, for every positive epsilon, all terms past some index N stay within epsilon of a. · C03S06.ConvergesTo

ConvergesTo def

def ConvergesTo (s : ℕ → ℝ) (a : ℝ) · C03S06.ConvergesTo

ConvergesTo' def

def ConvergesTo' (s : α → ℝ) (a : ℝ) · C03S06.ConvergesTo'

D

depth def

def depth : BinTree → ℕ · BinTree.depth

DiaOneClass₁ class

class DiaOneClass₁ (α : Type) extends One₁ α, Dia₁ α · DiaOneClass₁

Dia₁ class

class Dia₁ (α : Type) · Dia₁

div' def

def div' (a b : ℤ) · Int.div'

E

eval def

def eval : PropForm → (ℕ → Bool) → Bool · PropForm.eval

evens def

def evens : Set ℕ · evens

example1 def

def example1 : Finset ℕ · example1

F

f def

def f (x : ℕ) · f

f def

def f (n : ℕ) : Int · finsets_and_fintypes.f

fac def

def fac : ℕ → ℕ · fac

fac def

def fac : ℕ → ℕ · more_induction.fac

FermatLastTheorem def

def FermatLastTheorem · FermatLastTheorem

fib def

def fib : ℕ → ℕ · more_induction.fib

fib' def

def fib' (n : Nat) : Nat · more_induction.fib'

finalIso def

def finalIso : G ≃* H × K · finalIso

flip def

def flip : BinTree → BinTree · BinTree.flip

FnEven def

def FnEven (f : ℝ → ℝ) : Prop · C03S01.FnEven

FnHasLb def

def FnHasLb (f : ℝ → ℝ) · C03S02.FnHasLb

FnHasLb def

def FnHasLb (f : ℝ → ℝ) · C03S03.FnHasLb

FnHasUb def

def FnHasUb (f : ℝ → ℝ) · C03S02.FnHasUb

FnHasUb def

def FnHasUb (f : ℝ → ℝ) · C03S03.FnHasUb

FnLb def

def FnLb (f : ℝ → ℝ) (a : ℝ) : Prop · C03S01.FnLb

FnLb def

def FnLb (f : ℝ → ℝ) (a : ℝ) : Prop · C03S02.FnLb

FnLb def

def FnLb (f : ℝ → ℝ) (a : ℝ) : Prop · C03S03.FnLb

FnOdd def

def FnOdd (f : ℝ → ℝ) : Prop · C03S01.FnOdd

FnUb def

def FnUb (f : ℝ → ℝ) (a : ℝ) : Prop · C03S01.FnUb

FnUb def

def FnUb (f : ℝ → ℝ) (a : ℝ) : Prop · C03S02.FnUb

FnUb def

def FnUb (f : ℝ → ℝ) (a : ℝ) : Prop · C03S03.FnUb

FnUb' def

def FnUb' (f : α → R) (a : R) : Prop · C03S01.FnUb'

foo def

def foo : f * 1 * g⁻¹ = g.symm.trans ((Equiv.refl α).trans f) · C06S02.foo

G

GaussInt structure

structure GaussInt · GaussInt

Group₁ structure

structure Group₁ (α : Type*) · C06S02.Group₁

Group₁ class

class Group₁ (G : Type) extends Monoid₁ G, Inv₁ G · Group₁

Group₂ class

class Group₂ (α : Type*) · C06S02.Group₂

Group₃ class

class Group₃ (G : Type) extends Monoid₃ G, Inv G · Group₃

Grp₁ structure

structure Grp₁ · C06S02.Grp₁

I

inverse def

def inverse (f : α → β) : β → α · inverse

Inv₁ class

class Inv₁ (α : Type) · Inv₁

IsLinear structure

structure IsLinear (f : ℝ → ℝ) · C06S01.IsLinear

IsLinear' def

def IsLinear' (f : ℝ → ℝ) · C06S01.IsLinear'

isMonoidHom₁ def

def isMonoidHom₁ [Monoid G] [Monoid H] (f : G → H) : Prop · isMonoidHom₁

isMonoidHom₂ structure

structure isMonoidHom₂ [Monoid G] [Monoid H] (f : G → H) : Prop · isMonoidHom₂

iso₁ def

def iso₁ : K ≃* G ⧸ H · iso₁

iso₂ def

def iso₂ : G ≃* (G ⧸ K) × (G ⧸ H) · iso₂

L

LE₁ class

class LE₁ (α : Type) · LE₁

List inductive

inductive List (α : Type*) · MyListSpace.List

LT₁ class

class LT₁ (α : Type) · LT₁

M

map def

def map {α β : Type*} (f : α → β) : List α → List β · MyListSpace2.map

midpoint def

def midpoint (n : ℕ) (a b : StandardSimplex n) : StandardSimplex n · C06S01.StandardSimplex.midpoint

midpoint def

def midpoint (a b : StandardTwoSimplex) : StandardTwoSimplex · C06S01.StandardTwoSimplex.midpoint

mk def

def QuotientMonoid.mk [CommMonoid M] (N : Submonoid M) : M → M ⧸ N · QuotientMonoid.mk

mod' def

def mod' (a b : ℤ) · Int.mod'

Module₁ class

class Module₁ (R : Type) [Ring₃ R] (M : Type) [AddCommGroup₃ M] extends SMul₃ R M · Module₁

MonoidHomClass₁ class

class MonoidHomClass₁ (F : Type) (M N : Type) [Monoid M] [Monoid N] · MonoidHomClass₁

MonoidHomClass₂ class

class MonoidHomClass₂ (F : Type) (M N : outParam Type) [Monoid M] [Monoid N] · MonoidHomClass₂

MonoidHomClass₃ class

class MonoidHomClass₃ (F : Type) (M N : outParam Type) [Monoid M] [Monoid N] extends DFunLike F M (fun _ ↦ N) · MonoidHomClass₃

MonoidHom₁ structure

structure MonoidHom₁ (G H : Type) [Monoid G] [Monoid H] · MonoidHom₁

Monoid₁ class

class Monoid₁ (α : Type) extends Semigroup₁ α, DiaOneClass₁ α · Monoid₁

Monoid₂ class

class Monoid₂ (α : Type) · Monoid₂

Monoid₃ class

class Monoid₃ (α : Type) extends Semigroup₃ α, MulOneClass α export Semigroup₃ (mul_assoc₃) export AddSemigroup₃ (add_assoc₃) whatsnew in @[to_additive] · Monoid₃

mul def

def mul : MyNat → MyNat → MyNat · MyNat.mul

myElement def

def myElement : FreeGroup S · myElement

myGroup def

def myGroup · myGroup

myMap def

def myMap : Unit → Perm (Fin 5) · myMap

myMorphism def

def myMorphism : FreeGroup S →* Perm (Fin 5) · myMorphism

MyNat inductive

inductive MyNat · MyNat

myNewMorphism def

def myNewMorphism : myGroup →* Perm (Fin 5) · myNewMorphism

myPoint1 def

def myPoint1 : Point · C06S01.myPoint1

myPoint2 def

def myPoint2 : Point · C06S01.myPoint2

myPoint3 def

def myPoint3 : Point · C06S01.myPoint3

myPoint4 def

def myPoint4 · C06S01.myPoint4

mySquare def

def mySquare {α : Type*} [Group₂ α] (x : α) · C06S02.mySquare

N

neg def

def neg (a : Point) : Point · C06S02.Point.neg

norm def

def norm (x : GaussInt) · GaussInt.norm

nsmul₁ def

def nsmul₁ {M : Type*} [Zero M] [Add M] : ℕ → M → M · nsmul₁

O

odds def

def odds : Set ℕ · odds

One₁ class

class One₁ (α : Type) · One₁

One₂ structure

structure One₂ (α : Type) · One₂

OrderedCommMonoid₁ class

class OrderedCommMonoid₁ (α : Type) · OrderedCommMonoid₁

OrderedCommMonoid₁ class

class OrderedCommMonoid₁ (α : Type) extends PartialOrder₁ α, CommMonoid₃ α · OrderedCommMonoid₁

OrderPresHom structure

structure OrderPresHom (α β : Type) [LE α] [LE β] · OrderPresHom

OrderPresHomClass class

class OrderPresHomClass (F : Type) (α β : outParam Type) [LE α] [LE β] · OrderPresHomClass

OrderPresHomClass class

class OrderPresHomClass (F : Type) (α β : outParam Type) [LE α] [LE β] extends DFunLike F α (fun _ ↦ β) · OrderPresHomClass

OrderPresMonoidHom structure

structure OrderPresMonoidHom (M N : Type) [Monoid M] [LE M] [Monoid N] [LE N] extends MonoidHom₁ M N, OrderPresHom M N · OrderPresMonoidHom

P

PartialOrder₁ class

class PartialOrder₁ (α : Type) · PartialOrder₁

PartialOrder₁ class

class PartialOrder₁ (α : Type) extends Preorder₁ α · PartialOrder₁

permGroup def

def permGroup {α : Type*} : Group₁ (Equiv.Perm α) · C06S02.permGroup

phi def

def phi : ℝ · more_induction.phi

phi' def

def phi' : ℝ · more_induction.phi'

Point structure

structure Point · C06S01.Point

Point structure

fill in the rest · C06S02.Point

Point structure

structure Point · C06S02.Point

Point' structure

structure Point' · C06S01.Point'

Point'' def

def Point'' · C06S01.Point''

PReal def

def PReal · C06S01.PReal

preimage def

def preimage {W : Type*} [AddCommGroup W] [Module K W] (φ : V →ₗ[K] W) (H : Submodule K W) : Submodule K V · preimage

Preorder₁ class

class Preorder₁ (α : Type) · Preorder₁

Preorder₁ class

class Preorder₁ (α : Type) extends LE₁ α · Preorder₁

PreOrder₂ class

class PreOrder₂ (α : Type) extends LE₁ α, LT₁ α · PreOrder₂

primes def

def primes : Set ℕ · primes

principal def

def principal {α : Type*} (s : Set α) : Filter α · principal

PropForm inductive

inductive PropForm : Type · PropForm

R

reverse def

def reverse : List α → List α · MyListSpace3.reverse

RingHom₁ structure

structure RingHom₁ (R S : Type) [Ring R] [Ring S] extends MonoidHom₁ R S, AddMonoidHom₁ R S · RingHom₁

Ring₃ class

class Ring₃ (R : Type) extends AddGroup₃ R, Monoid₃ R, MulZeroClass R · Ring₃

S

S inductive

inductive S | a | b | c open S · S

sbAux def

def sbAux : ℕ → Set α · sbAux

sbFun def

def sbFun (x : α) : β · sbFun

sbSet def

def sbSet · sbSet

Semigroup₀ class

class Semigroup₀ (α : Type) · Semigroup₀

Semigroup₁ class

class Semigroup₁ (α : Type) extends toDia₁ : Dia₁ α · Semigroup₁

Semigroup₂ class

class Semigroup₂ (α : Type) extends Dia₁ α · Semigroup₂

Semigroup₃ class

class Semigroup₃ (α : Type) extends Mul α · Semigroup₃

Setoid def

def Submonoid.Setoid [CommMonoid M] (N : Submonoid M) : Setoid M · Submonoid.Setoid

SetUb def

def SetUb (s : Set α) (a : α) · C03S01.SetUb

size def

def size : BinTree → ℕ · BinTree.size

smul def

def smul (r : ℝ) (a : Point) : Point · C06S01.Point.smul

SMul₃ class

class SMul₃ (α : Type) (β : Type) · SMul₃

StandardSimplex structure

structure StandardSimplex (n : ℕ) · C06S01.StandardSimplex

StandardSimplex' def

def StandardSimplex' (n : ℕ) · C06S01.StandardSimplex'

StandardTwoSimplex structure

structure StandardTwoSimplex · C06S01.StandardTwoSimplex

StandardTwoSimplex' def

def StandardTwoSimplex' · C06S01.StandardTwoSimplex'

StdSimplex def

def StdSimplex · C06S01.StdSimplex

SubgroupClass₁ class

class SubgroupClass₁ (S : Type) (G : Type) [Group G] [SetLike S G] : Prop extends SubmonoidClass₁ S G · SubgroupClass₁

Subgroup₁ structure

structure Subgroup₁ (G : Type) [Group G] extends Submonoid₁ G · Subgroup₁

SubmonoidClass₁ class

class SubmonoidClass₁ (S : Type) (M : Type) [Monoid M] [SetLike S M] : Prop · SubmonoidClass₁

Submonoid₁ structure

structure Submonoid₁ (M : Type) [Monoid M] · Submonoid₁

subst def

def subst : PropForm → ℕ → PropForm → PropForm · PropForm.subst

SumOfSquares def

def SumOfSquares (x : α) · C03S02.SumOfSquares

swapXy def

def swapXy (a : StandardTwoSimplex) : StandardTwoSimplex · C06S01.StandardTwoSimplex.swapXy

T

Tendsto₁ def

def Tendsto₁ {X Y : Type*} (f : X → Y) (F : Filter X) (G : Filter Y) · Tendsto₁

Tendsto₂ def

def Tendsto₂ {X Y : Type*} (f : X → Y) (F : Filter X) (G : Filter Y) · Tendsto₂

triangle def

def triangle (n : ℕ) : Finset (ℕ × ℕ) · triangle

triangle' def

def triangle' (n : ℕ) : Finset (ℕ × ℕ) · triangle'

V

vars def

def vars : PropForm → Finset ℕ · PropForm.vars

W

weightedAverage def

def weightedAverage {n : ℕ} (lambda : Real) (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1) (a b : StandardSimplex n) : StandardSimplex n · C06S01.StandardSimplex.weightedAverage

weightedAverage def

def weightedAverage (lambda : Real) (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1) (a b : StandardTwoSimplex) : StandardTwoSimplex · C06S01.StandardTwoSimplex.weightedAverage

Z

zero def

def zero : Point · C06S02.Point.zero

zsmul₁ def

def zsmul₁ {M : Type*} [Zero M] [Add M] [Neg M] : ℤ → M → M · zsmul₁

Terms from the explanations

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

calc

a chain of equalities and inequalities, each step justified by its own proof, which Lean composes into one claim. · C03S01.my_lemma4

epsilon-N definition

the formulation of a limit that quantifies over a tolerance epsilon and a cutoff index N, as used by ConvergesTo. · C03S06.ConvergesTo

namespace

a prefix that groups names, so that MyRing.add_zero and the library's add_zero are different declarations. · MyRing.add_zero

sorry

a placeholder proof; Lean accepts it but reports a warning, because nothing has actually been proved. · MyRing.add_left_cancel

surjective

a function f is surjective when every element of its target equals f x for some x. · Cantor

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.