Glossary

Every word this site uses, in one place: what this project defines, the words its explanations and readings use, and Lean's own words. Type in the box to filter.

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 · H · I · J · K · L · M · N · O · P · R · S · T · U · V · W

A

aboveCycleEdges def
A concrete graph where one node relies on a cycle. · Hyperfields.Fields.Hyperorganization.aboveCycleEdges
add def
The sum of two values over the same scale. · Hyperfields.Exact.Value.add
allEntries def
Every entry the registry holds, in the order the portal lists them. · Hyperfields.Manifest.allEntries
allIds def
Every field the catalogue carries, in derivation order. · Hyperfields.Architecture.allIds
amount def
The count in a place, if the place has one. · Hyperfields.Fields.Hypermechanics.MechanismState.amount
applyRule def
Apply a rule to a state. -- L4DEL: title: Fire a rule -- L4DEL: intuition: A rule fires only when every guard holds and no count would go negative, and otherwise it does not fire at all. -- L4DEL: prereq: … · Hyperfields.Fields.Hypermechanics.applyRule
authorityHeight def
The authority height of a rule: the number of governors above it before the chain ends. · Hyperfields.Fields.Hyperorganization.authorityHeight
awaitingOwnerReview def
No entry may claim owner review merely because this Lean catalogue compiles. · Hyperfields.Entry.awaitingOwnerReview
Axis inductive
The four semantic axes a field may occupy. · Hyperfields.Architecture.Axis
AxisProfile abbrev
The axes a field occupies. · Hyperfields.Architecture.AxisProfile
axisProfile def
The axis profile of every field. · Hyperfields.Architecture.axisProfile

B

boundary def
The boundary of a subset: the intersection of its closure with the closure of its complement. · Hyperfields.Fields.Hypertopology.FiniteTopology.boundary
Bridge structure
One declared cross-field correspondence. · Hyperfields.Bridges.Bridge
BridgeRelation inductive
The role a bridge claims to play. · Hyperfields.Bridges.BridgeRelation
BridgeStatus inductive
The declared status of a bridge. · Hyperfields.Bridges.BridgeStatus

C

canonical def
Order a list so that equal contents give equal lists. · Hyperfields.Finite.canonical
carrier def
The full carrier of n points. · Hyperfields.Finite.carrier
chainAbove def
The rules above a rule, in order, and whether the chain ended. · Hyperfields.Fields.Hyperorganization.chainAbove
chainEdges def
A concrete graph: 0 relies on 1, 1 relies on 2, and 2 relies on nothing. · Hyperfields.Fields.Hyperorganization.chainEdges
chainSystem def
A concrete transition system: a steps to b, b steps to c, and c steps to nothing. · Hyperfields.Fields.Hyperdynamics.chainSystem
chainTopology def
A concrete three-point topology used to check the axioms and the operations. · Hyperfields.Fields.Hypertopology.chainTopology
changeOf def
The change a rule makes to a place, if it makes one. · Hyperfields.Fields.Hypermechanics.RewriteRule.changeOf
ChartTransition structure
A chart transition: a bijection of points between two metric spaces that preserves every distance. · Hyperfields.Fields.Hypergeometry.ChartTransition
closure def
The closure of a subset: the intersection of every closed superset of it. · Hyperfields.Fields.Hypertopology.FiniteTopology.closure
constitution def
A concrete constitution: rule 0 is governed by rule 1, rule 1 is governed by rule 2, and rule 2 is governed by nothing. · Hyperfields.Fields.Hyperorganization.constitution
containmentAcyclic def
Whether the containment relation is acyclic. -- L4DEL: title: Containment has no cycle -- L4DEL: intuition: A node that can reach itself by following containment is contained in itself, which no well-founded whole allows. -- L4DEL: step: … · Hyperfields.Fields.Hyperstructure.RecursiveStructure.containmentAcyclic
continuousBetween def
Whether a map between two finite topologies is continuous. · Hyperfields.Fields.Hypertopology.continuousBetween
creatingRule def
A concrete rule that creates a unit, and is therefore not admissible. · Hyperfields.Fields.Hypermechanics.creatingRule
cyclicConstitution def
A concrete constitution with a cycle: rule 0 is governed by rule 1 and rule 1 is governed by rule 0. · Hyperfields.Fields.Hyperorganization.cyclicConstitution
cyclicEdges def
A concrete graph with a cycle: 0 relies on 1 and 1 relies on 0. · Hyperfields.Fields.Hyperorganization.cyclicEdges
cyclicSystem def
A concrete transition system with a cycle: a steps to b and b steps back to a. · Hyperfields.Fields.Hyperdynamics.cyclicSystem

D

declaredBridges def
The three declared cross-field bridges. · Hyperfields.Bridges.declaredBridges
declaresAllRequiredKinds def
Whether every designated kind is declared. · Hyperfields.Fields.Hyperstructure.declaresAllRequiredKinds
diff def
The difference of two finite sets: the elements of xs that are not in ys. · Hyperfields.Finite.diff
discreteTwo def
The discrete topology on two points: every subset is open. · Hyperfields.Fields.Hypertopology.discreteTwo
display def
Render a grounding as the sentence the catalogue publishes. · Hyperfields.Grounding.display
displayName def
The published display name of a repository. · Hyperfields.RepoId.displayName
distance def
The distance between two points, as a numerator over the matrix scale. · Hyperfields.Exact.distance

E

EcosystemRole inductive
A repository's role is distinct from whether its internal account is grounded. · Hyperfields.EcosystemRole
emptyState def
A state whose first place is empty. · Hyperfields.Fields.Hypermechanics.emptyState
Entry structure
One ecosystem entry. summary is explanatory prose; its review field prevents that prose from being confused with a kernel-checked theorem. · Hyperfields.Entry
entry def
The canonical Grounded Hypercalculi record used by the unified portal. · Hyperfields.Fields.GroundedHypercalculi.entry
entry def
The canonical Grounded Hyperset Theory record used by the unified portal. · Hyperfields.Fields.GroundedHypersetTheory.entry
entry def
The canonical Hyperbiology record used by the unified portal. · Hyperfields.Fields.Hyperbiology.entry
entry def
The canonical Hyperchaos record used by the unified portal. · Hyperfields.Fields.Hyperchaos.entry
entry def
The canonical Hyperchemistry record used by the unified portal. · Hyperfields.Fields.Hyperchemistry.entry
entry def
The canonical Hyperdynamics record used by the unified portal. · Hyperfields.Fields.Hyperdynamics.entry
entry def
The canonical Hyperemergence record used by the unified portal. · Hyperfields.Fields.Hyperemergence.entry
entry def
The canonical Hyperethics record used by the unified portal. · Hyperfields.Fields.Hyperethics.entry
entry def
The canonical Hypergeometry record used by the unified portal. · Hyperfields.Fields.Hypergeometry.entry
entry def
The canonical Hypergrammar record used by the unified portal. · Hyperfields.Fields.Hypergrammar.entry
entry def
The canonical Hyperlogic record used by the unified portal. · Hyperfields.Fields.Hyperlogic.entry
entry def
The canonical Hypermath record used by the unified portal. · Hyperfields.Fields.Hypermath.entry
entry def
The canonical Hypermechanics record used by the unified portal. · Hyperfields.Fields.Hypermechanics.entry
entry def
The canonical Hyperobjectivity record used by the unified portal. · Hyperfields.Fields.Hyperobjectivity.entry
entry def
The canonical Hyperorder record used by the unified portal. · Hyperfields.Fields.Hyperorder.entry
entry def
The canonical Hyperorganization record used by the unified portal. · Hyperfields.Fields.Hyperorganization.entry
entry def
The canonical Hyperphysics record used by the unified portal. · Hyperfields.Fields.Hyperphysics.entry
entry def
The canonical Hyperprobability record used by the unified portal. · Hyperfields.Fields.Hyperprobability.entry
entry def
The canonical Hyperreality record used by the unified portal. · Hyperfields.Fields.Hyperreality.entry
entry def
The canonical Hyperspace record used by the unified portal. · Hyperfields.Fields.Hyperspace.entry
entry def
The canonical Hyperstratum record used by the unified portal. · Hyperfields.Fields.Hyperstratum.entry
entry def
The canonical Hyperstructure record used by the unified portal. · Hyperfields.Fields.Hyperstructure.entry
entry def
The canonical Hypersubjectivity record used by the unified portal. · Hyperfields.Fields.Hypersubjectivity.entry
entry def
The canonical Hypertime record used by the unified portal. · Hyperfields.Fields.Hypertime.entry
entry def
The canonical Hypertopology record used by the unified portal. · Hyperfields.Fields.Hypertopology.entry
entry def
The canonical Metamathethicology record used by the unified portal. · Hyperfields.Fields.Metamathethicology.entry
entry def
The canonical Meta-Morphoscripted-Origination record used by the unified portal. · Hyperfields.Fields.MetaMorphoscriptedOrigination.entry
entry def
The canonical Ordinatics record used by the unified portal. · Hyperfields.Fields.Ordinatics.entry
eq def
Whether two values over the same scale are equal. · Hyperfields.Exact.Value.eq

F

FieldClass inductive
The classification of a bridge endpoint. · Hyperfields.Bridges.FieldClass
FiniteTopology structure
A finite topology over a carrier of n points. · Hyperfields.Fields.Hypertopology.FiniteTopology
finLe def
The natural ordering on Fin n, as a Bool-valued comparison. · Hyperfields.Finite.finLe
fullStructure def
The recursive structure of the whole: five nodes, the subject containing the four members, and one operational connection between two members. · Hyperfields.Fields.Hyperstructure.fullStructure
fullView def
A presentation of a whole with four abstract members, one of each designated kind, all of them contained and all of them components. · Hyperfields.Fields.Hyperstructure.fullView

G

groundedHypercalculi def
The calculi are grounded because they operate over lower-level Hypermath and adjacent foundational concepts. · Hyperfields.groundedHypercalculi
groundedHypersetTheory def
The hyperset layer is grounded in lower-level mathematical structure while supplying APGs, AFA, and bisimulation machinery. · Hyperfields.groundedHypersetTheory
Grounding inductive
Grounding is relative to the presentation recorded here. fieldPrimitive means "presented as primitive inside this field", not "proved absolutely primitive in reality". · Hyperfields.Grounding
groundingBases def
Render the bases a grounded entry stands on, primary first. · Hyperfields.Manifest.groundingBases
groundingKindString def
Render the kind of a grounding as a closed tag. · Hyperfields.Manifest.groundingKindString
groundingString def
Render a grounding as the manifest's grounding string. · Hyperfields.Manifest.groundingString

H

hyperbiology def
Hyperbiology is registered without a public main coordinate, so its current public source remains unresolved here. · Hyperfields.hyperbiology
hyperchaos def
A deliberately unresolved field frame records uses of chaos without silently choosing a native meaning. · Hyperfields.hyperchaos
hyperchemistry def
Hyperchemistry models how operations compose inside Hyperphysics. · Hyperfields.hyperchemistry
hyperdynamics def
A finite local candidate records transitions, path lifting, and coupled products without claiming native dynamics are complete. · Hyperfields.hyperdynamics
hyperemergence def
Hyperemergence asks whether coherent behavior persists across levels rather than merely appearing at one level. · Hyperfields.hyperemergence
hyperethics def
Hyperethics applies the hyperfield programme to moral and governance structure. · Hyperfields.hyperethics
hypergeometry def
A finite local candidate records chart, metric, and transport structure without claiming a public source or native completion. · Hyperfields.hypergeometry
hypergrammar def
Hypergrammar is the communicative field for forming and relating expressions across the ecosystem. · Hyperfields.hypergrammar
hyperlogic def
Hyperlogic is presented as Hypermath's logic counterpart. · Hyperfields.hyperlogic
hypermath def
Hypermath is the ecosystem's primitive mathematical kernel and Lean-facing bridge. · Hyperfields.hypermath
hypermechanics def
A finite local candidate records guarded rewrites, conservation, noninterference, and connection rules. · Hyperfields.hypermechanics
hyperobjectivity def
Hyperobjectivity studies what remains invariant across situated presentations. · Hyperfields.hyperobjectivity
hyperorder def
Hyperorder records finite ordering structure while treating an absent relation as unknown rather than false. · Hyperfields.hyperorder
hyperorganization def
Hyperorganization is registered as a structural hub pending an owner-reviewed account of its relation to the fields. · Hyperfields.hyperorganization
hyperphysics def
Hyperphysics applies the hyperfield programme to physical law while keeping model evidence distinct from physical confirmation. · Hyperfields.hyperphysics
hyperprobability def
Hyperprobability isolates the field structure of bounded uncertainty and guaranteed outcomes. · Hyperfields.hyperprobability
hyperreality def
Hyperreality provides the repository's current taxonomy of reality presentations and their containment order. · Hyperfields.hyperreality
hyperspace def
Hyperspace records placement among observable realities without silently converting placement into passage. · Hyperfields.hyperspace
hyperstratum def
Hyperstratum organizes form, frame, field, relation, graph, structure, and representation across levels. · Hyperfields.hyperstratum
hyperstructure def
A finite local candidate separates abstract roles, containers, components, and exact presentation isomorphism. · Hyperfields.hyperstructure
hypersubjectivity def
Hypersubjectivity makes the situated perspective part of the formal object instead of erasing it. · Hyperfields.hypersubjectivity
hypertime def
Hypertime records branching and order among reality presentations without assuming an outside clock. · Hyperfields.hypertime
hypertopology def
A finite local candidate records open, closure, boundary, and continuity structure without claiming a public source or native completion. · Hyperfields.hypertopology

I

independent def
Whether two rules have disjoint footprints. -- L4DEL: title: Two rules are independent -- L4DEL: intuition: If neither rule writes a place the other writes or reads, the order they fire in cannot matter, which is a sufficient condition for … · Hyperfields.Fields.Hypermechanics.independent
indiscreteTwo def
The indiscrete topology on two points: only the empty set and the whole carrier are open. · Hyperfields.Fields.Hypertopology.indiscreteTwo
insertOrdered def
Insert an element into an ordered list, keeping the list ordered. · Hyperfields.Finite.insertOrdered
inter def
The intersection of two finite sets. · Hyperfields.Finite.inter
interior def
The interior of a subset: the union of every open set contained in it. · Hyperfields.Fields.Hypertopology.FiniteTopology.interior
isFinite def
Whether a node's phase is finite. · Hyperfields.Fields.Hyperorganization.Phase.isFinite
isIsometry def
Whether the transition's mapping preserves every distance. · Hyperfields.Fields.Hypergeometry.ChartTransition.isIsometry
isOpen def
Whether a bridge is still an open declaration. · Hyperfields.Bridges.Bridge.isOpen

J

joinNames def
Join a list of names the way the catalogue joins them, with a serial comma before the final item when there are three or more. · Hyperfields.joinNames
jsonString def
Escape a string as a JSON string literal, including the quotes. · Hyperfields.Manifest.jsonString

K

kindOfMember def
The kind assigned to a member, if any. · Hyperfields.Fields.Hyperstructure.SempiternalityView.kindOfMember
kindOfPlace def
The kind of a place, if the place has one. · Hyperfields.Fields.Hypermechanics.MechanismState.kindOfPlace
kindOfState def
The kind declared for a state, if any. · Hyperfields.Fields.Hyperdynamics.TransitionSystem.kindOfState
kindsAreDistinct def
Whether the declared kinds are pairwise distinct. · Hyperfields.Fields.Hyperstructure.kindsAreDistinct

L

le def
Compare two values over the same scale. · Hyperfields.Exact.Value.le
lookup def
Look up the image of a point in a transition's mapping. · Hyperfields.Fields.Hypergeometry.lookup

M

main def
The emitter renders the Lean registry as JSON, so the published record is a build product rather than a second copy of the declarations. · main
Mapping structure
One named correspondence between a source concept and a target concept. · Hyperfields.Bridges.Mapping
MechanismState structure
A mechanism state: named places, the exact count in each, and the kind of each place. · Hyperfields.Fields.Hypermechanics.MechanismState
mem def
Whether an element belongs to a finite set. · Hyperfields.Finite.mem
metamathethicology def
Metamathethicology combines meta-level accounts without transferring authority among them automatically. · Hyperfields.metamathethicology
metaMorphoscriptedOrigination def
This framework studies how narratives of origination are formed and transformed under limited cognition. · Hyperfields.metaMorphoscriptedOrigination
MetricSpace structure
A finite metric space over a carrier of n points. · Hyperfields.Fields.Hypergeometry.MetricSpace
mkPublicEntry def
Construct a public-main entry. · Hyperfields.mkPublicEntry
mkUnpublishedEntry def
A local candidate is registered without inventing a public source coordinate or settled grounding. · Hyperfields.mkUnpublishedEntry
modeString def
Render one operating mode as the manifest's mode string. · Hyperfields.Manifest.modeString
moduleName def
The name of the dedicated Lean module that explains this repository. · Hyperfields.RepoId.moduleName

N

noDanglingEndpoints def
Whether every endpoint of a relation is one of the structure's nodes. · Hyperfields.Fields.Hyperstructure.RecursiveStructure.noDanglingEndpoints

O

OperatingMode inductive
Multiple modes may describe one field; communicative and formative are not opposites. · Hyperfields.OperatingMode
ordinatics def
Ordinatics supplies ordinal-first arithmetic and staged semantics rather than being silently relabelled as a hyperfield. · Hyperfields.ordinatics
ownerReviewQueue def
Every initial explanation still awaits Tyler's semantic review. · Hyperfields.ownerReviewQueue

P

Pairing structure
The two declared pairings. · Hyperfields.Architecture.Pairing
pairings def
The declared pairings. · Hyperfields.Architecture.pairings
pathLifts def
Whether a path lifts through a bridge. · Hyperfields.Fields.Hyperdynamics.pathLifts
Phase inductive
The phase of a node: a natural number, or ω when the node's reliance never bottoms out. · Hyperfields.Fields.Hyperorganization.Phase
phaseOf def
The phase of one node. · Hyperfields.Fields.Hyperorganization.phaseOf
phases def
The phase of every node of a graph of reliance. · Hyperfields.Fields.Hyperorganization.phases
positiveOffDiagonal def
Whether every matrix entry is a strictly positive distance. · Hyperfields.Exact.positiveOffDiagonal
profileOf def
Look up a field's axis profile. · Hyperfields.Architecture.profileOf
protection def
The protection of a rule: the price of the cheapest procedure among the rules above it. · Hyperfields.Fields.Hyperorganization.protection

R

reachable def
The states reachable from a starting state. · Hyperfields.Fields.Hyperdynamics.reachable
RecursiveStructure structure
A finite recursive structure: its nodes and its three relations. · Hyperfields.Fields.Hyperstructure.RecursiveStructure
registry def
The complete initial catalogue, with no inference from list order. · Hyperfields.registry
relations def
The relations a member stands in, as a list of relation names. · Hyperfields.Fields.Hyperstructure.SempiternalityView.relations
render def
Render one bridge as a JSON object. · Hyperfields.Bridges.Bridge.render
render def
Render the whole manifest. · Hyperfields.Manifest.render
renderBridges def
Render the whole bridge record. · Hyperfields.Bridges.renderBridges
renderEntry def
Render one entry as a JSON object. · Hyperfields.Manifest.renderEntry
RepoId inductive
Stable identifiers for repositories and unpublished field candidates known to this catalogue. · Hyperfields.RepoId
requiredKinds def
The four designated kinds. · Hyperfields.Fields.Hyperstructure.requiredKinds
ReviewState inductive
Review state of the explanatory text in this repository, not of the source project. · Hyperfields.ReviewState
reviewString def
Render a review state as the manifest's review-state string. · Hyperfields.Manifest.reviewString
RewriteRule structure
A rewrite rule: the guard minima, the changes, and the conservation weights. · Hyperfields.Fields.Hypermechanics.RewriteRule
roleString def
Render a role as the manifest's role string. · Hyperfields.Manifest.roleString
Rule structure
A rule: the price in bits of the procedure that changes it, and the rule that governs it. · Hyperfields.Fields.Hyperorganization.Rule

S

sameDistance def
Whether two distances are the same. · Hyperfields.Fields.Hypergeometry.sameDistance
Scale structure
The scale of a rational: a strictly positive shared denominator. · Hyperfields.Exact.Scale
SempiternalityView structure
A presentation of a whole: its abstract members, their kinds, what it contains, and what it is composed of. · Hyperfields.Fields.Hyperstructure.SempiternalityView
separation def
Whether the matrix satisfies separation: zero exactly on the diagonal and strictly positive off it. · Hyperfields.Exact.separation
slug def
The catalogue slug of a repository: the URL segment the portal publishes it under. · Hyperfields.RepoId.slug
SourceCoordinate structure
Exact public bytes used as the source for an explanatory entry. · Hyperfields.SourceCoordinate
sourceOnMain def
The repository URL and exact revision are constructed together. · Hyperfields.sourceOnMain
sourceShapeFailures def
All entries whose public-source shape is internally valid. · Hyperfields.sourceShapeFailures
sourceShapeValid def
A public-main entry is internally well-shaped only when it carries an exact source coordinate. · Hyperfields.Entry.sourceShapeValid
SourceState inductive
What public source coordinate is available for an entry. · Hyperfields.SourceState
sourceStateString def
Render a source state as the manifest's source-state string. · Hyperfields.Manifest.sourceStateString
sourceWithoutMain def
A public repository with no resolvable main commit still has a true URL, and inventing a revision for it would be a false coordinate. · Hyperfields.sourceWithoutMain
stageOf def
The stage at which a field becomes available. · Hyperfields.Architecture.stageOf
string def
The published name of an axis. · Hyperfields.Architecture.Axis.string
string def
The published string of a bridge relation. · Hyperfields.Bridges.BridgeRelation.string
string def
The published string of a bridge status. · Hyperfields.Bridges.BridgeStatus.string
string def
The published string of a field classification. · Hyperfields.Bridges.FieldClass.string
subset def
Whether every element of xs is also in ys. · Hyperfields.Finite.subset
symmetric def
Whether the matrix is symmetric. · Hyperfields.Exact.symmetric

T

threePoint def
The three-point metric: points a, b, c with distances 1, 2, and 1. · Hyperfields.Fields.Hypergeometry.threePoint
toSet def
Remove duplicates from a list, keeping the first occurrence of each element. · Hyperfields.Finite.toSet
transferRule def
A concrete rule: move one unit from place 0 to place 1. · Hyperfields.Fields.Hypermechanics.transferRule
TransitionSystem structure
A finite transition system: its states, its steps, and the kind of each state. · Hyperfields.Fields.Hyperdynamics.TransitionSystem
transportPath def
Transport a point along a path of chart transitions. · Hyperfields.Fields.Hypergeometry.transportPath
triangleInequality def
Whether the matrix satisfies the triangle inequality. · Hyperfields.Exact.triangleInequality
twoPlaceState def
A concrete state: place 0 holds 2 and place 1 holds 1. · Hyperfields.Fields.Hypermechanics.twoPlaceState
twoPoint def
The two-point metric: two points at distance one. · Hyperfields.Fields.Hypergeometry.twoPoint
twoPointIdentity def
The identity transition on the two-point metric. · Hyperfields.Fields.Hypergeometry.twoPointIdentity
twoPointSwap def
The transition that swaps the two points of the two-point metric. · Hyperfields.Fields.Hypergeometry.twoPointSwap

U

union def
The union of two finite sets. · Hyperfields.Finite.union
usable def
Whether a scale is usable: its denominator must be strictly positive. · Hyperfields.Exact.Scale.usable

V

Value structure
A rational value: a numerator over a shared scale. · Hyperfields.Exact.Value

W

weightedChange def
The weighted sum of a rule's changes. · Hyperfields.Fields.Hypermechanics.RewriteRule.weightedChange
weightOf def
The weight of a place in a rule's invariant, if it has one. · Hyperfields.Fields.Hypermechanics.RewriteRule.weightOf
wellShaped def
Whether a bridge is well-shaped as a declaration. · Hyperfields.Bridges.Bridge.wellShaped
wellShaped def
Whether the system satisfies the axioms. · Hyperfields.Fields.Hyperdynamics.TransitionSystem.wellShaped
wellShaped def
Whether the matrix satisfies the metric axioms. · Hyperfields.Fields.Hypergeometry.MetricSpace.wellShaped
wellShaped def
Whether the state satisfies the axioms. · Hyperfields.Fields.Hypermechanics.MechanismState.wellShaped
wellShaped def
Whether the rule satisfies the axioms. · Hyperfields.Fields.Hypermechanics.RewriteRule.wellShaped
wellShaped def
Whether the structure satisfies the axioms. · Hyperfields.Fields.Hyperstructure.RecursiveStructure.wellShaped
wellShaped def
Whether the view satisfies the presentation axioms. · Hyperfields.Fields.Hyperstructure.SempiternalityView.wellShaped
wellShaped def
Whether the opens satisfy the topology axioms. · Hyperfields.Fields.Hypertopology.FiniteTopology.wellShaped

Terms from the explanations

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

field frame
A typed place to record a proposed field while its native axioms remain unresolved. · Hyperfields.hyperchaos

Acronyms from the explanations

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

AFA
Anti-Foundation Axiom · Hyperfields.groundedHypersetTheory
APG
accessible pointed graph · Hyperfields.groundedHypersetTheory

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.