2.1.1. Sets versus types🔗

The first reflex to unlearn is the set-theoretic one that everything is a set. In set theory ∈ is the single primitive, an object can be a member of many sets, and there is no fixed notion of "the type of x". Type theory inverts this: the primitive is the type, and every term a : α has exactly one type, fixed once and for all.

A set in Lean is not a new type. A Set α is a predicate on the already-existing type α, carving out some of its terms. An element of s : Set α therefore still has type α; the set records only which terms of α lie in it.

Three notions are worth keeping firmly apart:

• a type α -- the ambient collection of terms;

• a set s : Set α -- a predicate selecting terms of α, whose elements keep their type α;

• a subtype { x : α // p x } (see Subtypes) -- a genuinely new type, whose terms are pairs of a value and a proof that it satisfies p.

So there is a difference between a set and a type, and it is the one a mathematician must internalize. The rest of this chapter makes it precise: sets as predicates and their operations, when two sets are equal, and finally how to cross the gap -- turning a set back into a type.

2.1.2. Notation and naming conventions🔗

The set-theoretic symbols below are unicode characters typed in VS Code via a backslash escape. Hover over a symbol in the editor to see its input sequence.

2.1.3. Sets are predicates🔗

Set α is definitionally the function type α → Prop. The term a : α belongs to s : Set α exactly when s a holds, and a ∈ s is notation for that.

Because a set is a predicate, two predicates that hold of exactly the same elements describe the same set -- set equality is extensional. We make this precise just below.

2.1.4. Subset, union, intersection, complement🔗

The usual Boolean operations on sets are all defined pointwise on the underlying predicates, so each unfolds to a familiar logical connective.

2.1.5. Indexed unions and intersections🔗

The binary ∪ and ∩ extend to arbitrary families. Given s : ι → Set α -- a set s i for each index i : ι -- the indexed union ⋃ i, s i and indexed intersection ⋂ i, s i collect members across the whole family.

Set.iUnion.{u, v} {α : Type u} {ι : Sort v} (s : ι → Set α) : Set α
Set.iUnion.{u, v} {α : Type u}
  {ι : Sort v} (s : ι → Set α) : Set α

Set.iInter.{u, v} {α : Type u} {ι : Sort v} (s : ι → Set α) : Set α
Set.iInter.{u, v} {α : Type u}
  {ι : Sort v} (s : ι → Set α) : Set α

As always, membership just unfolds to a quantifier:

A common variant restricts the index to a set a : Set ι rather than the whole index type -- written ⋃ i ∈ a, s i and ⋂ i ∈ a, s i. This is just the indexed operation ranging over the members of a, and membership carries the bound along:

When the family is given not by an index but as a set of sets S : Set (Set α), the same operations are written ⋃₀ S (sUnion) and ⋂₀ S (sInter):

Set.sUnion.{u} {α : Type u} (S : Set (Set α)) : Set α
Set.sUnion.{u} {α : Type u}
  (S : Set (Set α)) : Set α

Set.sInter.{u} {α : Type u} (S : Set (Set α)) : Set α
Set.sInter.{u} {α : Type u}
  (S : Set (Set α)) : Set α

These are exactly the set/indexed suprema and infima of the complete lattice of sets: ⋃ i, s i is iSup s, and ⋃₀ S is sSup S. They are also what σ-algebras are closed under -- a countable union or intersection is just the indexed one over ι = ℕ.

2.1.6. Set equality🔗

Two sets are equal exactly when they have the same members: the set extensionality principle Set.ext. This is not a definition but a consequence of the axioms -- a set is a function into Prop, so it rests on the extensionality axioms taken up in the next chapter. Here we simply use it.

2.1.7. From a set back to a type: subtypes and coercion🔗

A set is not a type, and sometimes you need one: to speak of a function defined only on s, or to sum over its elements. A set is promoted to a type by coercion: ↥s denotes the subtype { x // x ∈ s } of its members, a genuinely new type whose terms pair an element of α with a proof of membership.

With sets, subtypes, and their relationship to types in hand, we are ready to look at the structures Mathlib builds on top of them.

2.2.1. The universe hierarchy🔗

The universe hierarchy was given in Part 1: Prop = Sort 0, Type = Type 0 = Sort 1, Type u = Sort (u+1), the rule Sort u : Sort (u + 1), and universe-polymorphism via Type*. We now show why the absence of Type : Type is not optional. Were Type : Type to hold, one could reproduce Russell's paradox at the level of types -- Girard's paradox -- and thereby prove False. The stratification

is exactly what blocks this, and it is what keeps the whole system consistent. Everything else in this chapter -- the axioms, proof irrelevance, the CIC -- rests on top of it.

How the collapse would actually unfold -- building Girard's paradoxical universe in Lean, watching exactly where the type-checker stops it, and deriving False from the hypothesis that the stratification were absent -- is not treated here: it is the subject of Project 1 in the Projects chapter.

2.2.2. Prop vs Type: proof irrelevance🔗

Prop differs from every Type n by proof irrelevance (see why Prop is special): if P : Prop and h1 h2 : P, then h1 = h2. What follows is the foundational side of that.

This is a deliberate design choice. It means:

• You cannot pattern-match on a proof to extract computational data.

• Proofs can be erased at compile time without affecting program behavior.

• Two mathematical proofs of the same theorem are interchangeable.

That any two proofs of the same P : Prop are equal is itself provable by rfl and costs no axiom; this, and the reason an existential therefore lives in Prop -- so that recovering its witness needs choice -- are taken up in Declared axioms vs. what the kernel bakes in below.

The distinction between Prop and Type corresponds to the mathematical distinction between "asserting that something exists" (Prop) and "constructing a specific example" (Type).

2.2.3. The Calculus of Inductive Constructions🔗

The universe hierarchy, Prop with its proof irrelevance, dependent functions and inductive types form a single formal system, and that system is what Lean's kernel implements (de Moura and Ullrich, 2021)Leonardo de Moura and Sebastian Ullrich, 2021. “The Lean 4 Theorem Prover and Programming Language”. In Automated Deduction – CADE 28. (Lecture Notes in Computer Science 12699) -- the Calculus of Inductive Constructions, or CIC. The CIC is the entire trusted core of Lean: every definition, theorem, and tactic ultimately elaborates down to terms that the kernel re-checks against these rules, and nothing outside them is trusted.

The CIC is built from exactly three ideas:

1. Dependent functions -- the "Constructions". This is the Calculus of Constructions of Coquand and Huet (1988)Thierry Coquand and Gérard Huet (1988). “The Calculus of Constructions”. Information and Computation. 76(2–3), pp. 95–120.: a typed lambda calculus in which the type of the output may depend on the value of the input, giving the Π-types written (x : α) → β x. In one stroke this subsumes ordinary functions, polymorphic functions (which take types as arguments), and type-level functions.

2. Inductive types -- the "Inductive", added by Coquand and Paulin-Mohring (1990)Thierry Coquand and Christine Paulin-Mohring, 1990. “Inductively Defined Types”. In COLOG-88. (Lecture Notes in Computer Science 417). This is the rule that introduces a new type by listing its constructors. Both data and logic are built from it: Nat, List, and Prod are inductive types, but so are the logical connectives And, Or, False, and even equality Eq.

Defining your own inductive type uses exactly the same mechanism the standard library does -- there is no special magic reserved for the built-in types:

3. A universe hierarchy (Prop, Type 0, Type 1, ...), exactly as in the first section, which keeps the system logically consistent by forbidding Type : Type.

On top of these three ingredients the kernel bakes in one thing that set theory has no notion of: computation. Terms reduce, so (fun n => n + 1) 2 and 3 are not merely provably equal but definitionally equal, and the kernel checks this by evaluating. This is the same reduction that makes Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling it and running the compiled code. It then prints the resulting value. * The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result. * If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m` to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`. Users can define `MonadEval` instances to extend the list of supported monads. The `#eval` command gracefully degrades in capability depending on what is imported. Importing the `Lean.Elab.Command` module provides full capabilities. Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly, since the presence of `sorry` can lead to runtime instability and crashes. This check can be overridden with the `#eval! e` command. Options: * If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances. * If `eval.type` is true (default: false) then pretty prints the type of the evaluated value. * If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance when there is no other way to print the result. See also: `#reduce e` for evaluation by term reduction. #eval and the decide tactic work, and it is what lets us speak of computable functions at all.

The CIC is small. A type checker for it is a few thousand lines of code, and that program is the whole of what you must trust in order to believe a Lean proof. Everything in Mathlib -- the integers, the real numbers, manifolds, schemes -- is in the end a tower of inductive types and dependent functions resting on this kernel.

2.2.4. The axioms of Lean🔗

The CIC by itself is minimal and constructive: a handful of principles that working mathematicians use without a second thought cannot be proved in it. Lean therefore adds axioms on top of the kernel. There are exactly three, and we can ask Lean itself to confirm it with the #print axioms command, which traces a constant back to the axioms it ultimately depends on:

Each of the three depends only on itself -- the signature of a genuine axiom. Everything else that looks axiomatic -- function extensionality, the law of excluded middle, the set-theoretic axiom of choice -- is in fact a theorem derived from these three, as we verify below. We take the three axioms first.

2.2.5. What is not an axiom: funext and excluded middle🔗

Two principles that mathematicians treat as bedrock are not axioms in Lean. They are theorems derived from the three above.

2.2.6. Declared axioms vs. what the kernel bakes in🔗

Saying Lean has "exactly three axioms" is precise about declared axioms -- the axiom constants, which are exactly what #print axioms reports. But the kernel's typing and definitional-equality rules quietly build in further logical principles that are not axioms and leave no trace in #print axioms. Unlike the three axioms, you cannot opt out of them.

The clearest are definitional: they hold by rfl, yet cost nothing.

So the following are all built into the kernel, not assumed on top of it:

2.2.7. Constructive vs classical logic🔗

By default, Lean's type theory is constructive: proofs must provide explicit witnesses and constructions. The axiom of choice introduces classical reasoning, which allows non-constructive arguments.

2.2.8. Comparison with ZFC set theory🔗

Most mathematicians are (at least implicitly) trained in ZFC set theory. Here are the key differences from Lean's type theory:

A key practical difference: in ZFC, you can ask nonsensical questions like "is 3 ∈ π?" and get an answer. In Lean, comparing objects of different types is a type error, which catches many mistakes early.

Both foundations are equiconsistent for most of mathematics. Nearly everything that can be formalized in ZFC can also be formalized in Lean's type theory (and vice versa).

2.2.9. Brief mention of other type theories🔗

Lean's type theory is one of several:

• Simply typed lambda calculus (Church, 1940): No dependent types. Foundation for Haskell, OCaml.

• System F (Girard, Reynolds, 1970s): Adds polymorphism but not full dependent types. (Girard, 1972)Jean-Yves Girard, 1972. Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. PhD thesis, Université Paris VII

• Martin-Löf Type Theory (MLTT, 1971+): The origin of dependent types in proof assistants. Used in Agda. (Martin-Löf, 1975)Per Martin-Löf, 1975. “An Intuitionistic Theory of Types: Predicative Part”. In Logic Colloquium '73. (Studies in Logic and the Foundations of Mathematics 80)

• Calculus of Inductive Constructions (CIC): the system Lean's kernel implements, described earlier in this chapter; also used, in a closely related form, by Coq/Rocq.

• Homotopy Type Theory (HoTT, 2013): Interprets types as topological spaces and equality as paths. Adds the univalence axiom (due to Voevodsky): equivalent types are equal. This is incompatible with Lean's proof irrelevance for Prop, so HoTT uses different proof assistants (Agda, cubical Agda, or specialized Lean forks).

• Cubical Type Theory (2015+): Makes HoTT computational by using a cube category to model paths. (Cohen et al., 2018)Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg, 2018. “Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom”. arXiv:1611.02108

For this course, Lean's type theory (CIC + proof irrelevance + quotients + choice) is the framework we work in. It is expressive enough to formalize virtually all of modern mathematics, as the Mathlib library demonstrates.

2.3.1. Accessibility and well-founded relations🔗

The first mechanism lives inside a type and governs recursion. A relation r : α → α → Prop is well-founded when there are no infinite descending chains … r a₂ r a₁ r a₀ -- following r-predecessors downward, you always hit bottom after finitely many steps.

Why care? Well-foundedness is exactly the condition that makes recursion and induction legitimate. If f x is defined in terms of f y for r-smaller y, the computation terminates only because you cannot descend forever; and the induction principle "to prove P x, assume P y for every y with r y x" is valid precisely when r is well-founded. In one phrase: well-founded means "you may recurse and induct along r".

Lean expresses this through the inductive predicate Acc ("accessible"):

inductive Acc (r : α → α → Prop) : α → Prop where
  | intro (x : α) (h : ∀ y, r y x → Acc r y) : Acc r x

Read the constructor as: x is accessible once all of its r-predecessors y (those with r y x) are themselves accessible. A relation is well-founded when every element is accessible:

Acc is an inductive type -- the least fixed point, so it is finitely generated. The constructor for Acc r x demands accessibility of every predecessor, so the only way to build the proof is for every downward branch to bottom out after finitely many steps: a proof of Acc r x is a finite tree. An infinite descending chain would force an infinitely deep proof, which no inductive type admits -- so, where every element is accessible, no such chain exists. (Were Acc instead coinductive, the greatest fixed point, infinite proofs would be allowed and every element would count as accessible; the definition would be vacuous. The induction is the whole point.) This is exactly what powers well-founded recursion (WellFounded.fix): you may recurse along r because every descent terminates, and termination_by / decreasing_by use precisely this.

It helps to see what fails. These relations are not well-founded:

• < on the integers ℤ: the chain 0 > -1 > -2 > … descends forever, with no bottom.

• < on ℚ or ℝ: 1 > ½ > ¼ > … never terminates.

• greater-than > on ℕ: the chain 0 < 1 < 2 < … is an infinite >-descending chain.

For none of these can Lean offer well-founded recursion -- there is no terminating direction to recurse in. The contrast between < and > on ℕ is the lesson: less-than bottoms out at 0, greater-than runs off to infinity.

Concretely, this abstract picture is realized in Lean in two ways. Each inductive type comes with an auto-generated recursor (Nat.rec, List.rec, ...) that is its structural induction and recursion principle -- well-foundedness for that type, guaranteed by the kernel. And for a uniform supply of well-founded relations, every inductive type carries a SizeOf instance, which sizeOfWFRel turns into a WellFoundedRelation whose well-foundedness is pulled back from < on Nat through InvImage.wf. So "inductive, hence finite trees, hence well-founded" becomes, in practice, the single fact Nat.lt_wfRel.wf transported along sizeOf.

2.3.2. Why Nat is well-founded🔗

The relation < on Nat is well-founded:

One proves Acc (· < ·) n by induction on n:

• 0 is accessible vacuously -- there is no m < 0.

• n + 1 is accessible because every m < n + 1 (that is, m ≤ n) is accessible by the induction hypothesis.

The deeper reason is that Nat is itself an inductive type (zero | succ): every natural number is a finite tower of succ over zero, so there is no infinite natural number to descend through. Structural recursion on Nat is the prototype of well-founded recursion, and the well-foundedness of < is just a restatement of it.

In practice you almost never prove well-foundedness yourself. Mathlib already supplies it -- the Nat.lt_wfRel.wf above is one of many WellFoundedRelation instances -- and when you write a recursive definition with termination_by (see the Function definitions chapter in Part 1), Lean finds the well-founded relation automatically and asks you only, via decreasing_by, to show that your measure decreases. The induction argument just given is the one-time justification the library performs, not something you repeat; you would do it by hand only for a genuinely new, exotic relation.

2.3.3. Why s ∈ s is impossible🔗

The second mechanism is typing, and it is what blocks self-membership and Russell's paradox. Unlike ZFC, Lean has no global membership relation: ∈ is typed. The instance behind it,

says that x ∈ s requires x : α and s : Set α. For s ∈ s the same s would need type α and type Set α at once -- that is, α = Set α, i.e. α = (α → Prop) (recall that a set is just a predicate). No such type exists (there is no matching Membership instance, and by Cantor's theorem α ≄ (α → Prop)). So s ∈ s is not a false statement; it is ill-formed:

Consequently Russell's set {x | x ∉ x} cannot even be written in Lean. Compare ZFC (see the ZFC comparison), where s ∈ s is a well-formed proposition and is excluded only by the separate axiom of foundation. Lean rules it out one step earlier, by typing.

Cantor's theorem, invoked above, states that for any type α there is no surjection α → Set α: the type of subsets Set α = α → Prop is always strictly larger than α itself (Mathlib's Function.cantor_surjective). In particular α and α → Prop can never be the same type, which is exactly what rules out α = Set α. The proof is a diagonal argument: given any candidate surjection f : α → Set α, the "diagonal" subset {x | x ∉ f x} is hit by no f x at all -- if f a were equal to it, then a ∈ f a and a ∉ f a would coincide. That diagonal subset is precisely Russell's {x | x ∉ x}: Cantor's theorem and Russell's paradox are the same construction, with Cantor drawing the consistent conclusion (no such surjection exists) exactly where naive set theory runs into a contradiction.

The very same typing discipline, one level up, forbids Type : Type: were Type to contain itself, Girard's paradox -- a type-theoretic Russell -- would make every proposition provable, and the universe hierarchy is exactly what rules it out. Building Girard's term in Lean and tracing where predicativity stops it is one of the course projects.

2.3.4. Two kinds of "no vicious circle"🔗

It is worth holding the two mechanisms apart -- they forbid circularity at different places:

Both express the intuition "no self-swallowing circles", but the first is a theorem-level tool you invoke for recursion, while the second is baked into the well-formedness rules of the language.

2.4.1. Notation and naming conventions🔗

Naming hints:

• The prefix s in sSup, sInf stands for set: it takes a Set α.

• The prefix i in iSup, iInf stands for indexed: it takes a function.

• The bare operators ⊔ and ⊓ are binary; sSup, sInf, iSup, iInf are their set/indexed counterparts.

• Lemma naming follows the convention le_sup_left, inf_le_right, le_antisymm, etc.: the conclusion is named first, then the hypotheses in order.

2.4.2. Partial orders🔗

A partial order on a type α is a reflexive, transitive, and antisymmetric relation ≤. In Mathlib this is captured by the typeclass PartialOrder α, which extends Preorder α (reflexive and transitive) with antisymmetry.

Key lemmas:

• le_refl a : a ≤ a

• le_trans : a ≤ b → b ≤ c → a ≤ c

• le_antisymm : a ≤ b → b ≤ a → a = b

A linear order (LinearOrder α) additionally satisfies totality: for every a b : α, either a ≤ b or b ≤ a. The natural numbers, integers, and reals all carry linear orders.

The strict order < is defined in terms of ≤: a < b ↔ a ≤ b ∧ a ≠ b (or equivalently a ≤ b ∧ ¬ b ≤ a).

2.4.3. The power set as a partial order🔗

For any type α, the type Set α carries a partial order given by set inclusion ⊆. This is a canonical example of a partial order that is not linear in general.

2.4.4. Lattices🔗

A lattice is a partial order in which every pair of elements has a least upper bound (supremum, join) and a greatest lower bound (infimum, meet).

In Mathlib:

• ⊔ (typed \sup) denotes the join (supremum of two elements).

• ⊓ (typed \inf) denotes the meet (infimum of two elements).

• The typeclass is Lattice α.

Key API:

• le_sup_left : a ≤ a ⊔ b

• le_sup_right : b ≤ a ⊔ b

• sup_le : a ≤ c → b ≤ c → a ⊔ b ≤ c

• inf_le_left : a ⊓ b ≤ a

• inf_le_right : a ⊓ b ≤ b

• le_inf : c ≤ a → c ≤ b → c ≤ a ⊓ b

2.4.5. Complete lattices🔗

A complete lattice is a partial order in which every subset has a supremum and an infimum (not just pairs). In Mathlib the typeclass is CompleteLattice α.

The operations are:

• sSup S : the supremum of a set S : Set α

• sInf S : the infimum of a set S : Set α

• ⊤ (\top) : the greatest element (= sSup Set.univ)

• ⊥ (\bot) : the least element (= sInf Set.univ)

• iSup and iInf for indexed suprema and infima.

2.4.6. Monotone and antitone functions🔗

A function f : α → β between preorders is monotone if a ≤ b → f a ≤ f b, and antitone if a ≤ b → f b ≤ f a. Mathlib provides Monotone f and Antitone f.

There is also StrictMono f for strictly increasing functions.

2.4.7. The Knaster-Tarski fixed point theorem🔗

The Knaster-Tarski theorem is one of the cornerstones of fixed point theory. It generalizes Tarski's earlier fixed point theorem for the real line and has applications in logic, denotational semantics, and set theory (e.g. the Schröder-Bernstein theorem).

Theorem (Knaster-Tarski). Let α be a complete lattice and let f : α → α be a monotone function. Then:

1. f has a least fixed point, given by sInf {x | f x ≤ x}.

2. f has a greatest fixed point, given by sSup {x | x ≤ f x}.

3. Moreover, the set of fixed points of f is itself a complete lattice under the induced order.

The proof of the first part is short and instructive. Let S = {x | f x ≤ x} (the prefixed points) and set a = sInf S. Since f is monotone and a ≤ x for every x ∈ S, we get f a ≤ f x ≤ x for all x ∈ S, so f a is a lower bound of S, hence f a ≤ a. Thus a ∈ S. Applying f monotonically gives f (f a) ≤ f a, so f a ∈ S, hence a ≤ f a. Antisymmetry yields f a = a, and any other fixed point y = f y belongs to S, so a ≤ y.

In Mathlib this theorem is available through the OrderHom API. The least fixed point is OrderHom.lfp and the greatest is OrderHom.gfp:

The least fixed point and the key lemmas:

OrderHom.lfp.{u} {α : Type u} [CompleteLattice α] : (α →o α) →o α
OrderHom.lfp.{u} {α : Type u}
  [CompleteLattice α] : (α →o α) →o α

OrderHom.map_lfp.{u} {α : Type u} [CompleteLattice α] (f : α →o α) :
  f (OrderHom.lfp f) = OrderHom.lfp f
OrderHom.map_lfp.{u} {α : Type u}
  [CompleteLattice α] (f : α →o α) :
  f (OrderHom.lfp f) = OrderHom.lfp f

OrderHom.lfp_le.{u} {α : Type u} [CompleteLattice α] (f : α →o α)
  {a : α} (h : f a ≤ a) : OrderHom.lfp f ≤ a
OrderHom.lfp_le.{u} {α : Type u}
  [CompleteLattice α] (f : α →o α) {a : α}
  (h : f a ≤ a) : OrderHom.lfp f ≤ a

Dually, the greatest fixed point:

OrderHom.gfp.{u} {α : Type u} [CompleteLattice α] : (α →o α) →o α
OrderHom.gfp.{u} {α : Type u}
  [CompleteLattice α] : (α →o α) →o α

OrderHom.map_gfp.{u} {α : Type u} [CompleteLattice α] (f : α →o α) :
  f (OrderHom.gfp f) = OrderHom.gfp f
OrderHom.map_gfp.{u} {α : Type u}
  [CompleteLattice α] (f : α →o α) :
  f (OrderHom.gfp f) = OrderHom.gfp f

OrderHom.le_gfp.{u} {α : Type u} [CompleteLattice α] (f : α →o α)
  {a : α} (h : a ≤ f a) : a ≤ OrderHom.gfp f
OrderHom.le_gfp.{u} {α : Type u}
  [CompleteLattice α] (f : α →o α) {a : α}
  (h : a ≤ f a) : a ≤ OrderHom.gfp f

Note that α →o α is the type of monotone self-maps of α (the arrow →o denotes an OrderHom). A useful small example:

Applications.

• Recursive definitions. The semantics of recursion in programming languages is given by least fixed points of monotone functionals on a domain of partial functions.

• The Schröder-Bernstein theorem. Given injections f : α → β and g : β → α, one constructs a bijection by taking the least fixed point of a certain monotone operator on Set α.

• Inductively defined sets. Many sets in mathematics (the natural numbers, syntactic terms, well-founded relations) are defined as least fixed points of monotone operators.

2.4.8. Summary of key API🔗

Here is a quick reference for the most important order-theoretic lemmas:

The omega tactic is very useful for goals involving natural number and integer inequalities. For more general ordered structures, gcongr can help with monotonicity goals.

2.4.9. Exercises🔗

Now try it yourself. The exercise sheet 06-a-Orders.lean turns the material above into sorry-holes to fill in your editor -- partial orders, lattices, sSup/sInf, and monotone functions. To run it in the browser with no local install (the first launch builds Mathlib, so give it a minute), open the repository in Gitpod and go to that file.

2.5.1. Notation and naming conventions🔗

Naming hints.

• Additive versus multiplicative. Mathlib systematically duplicates algebraic notions into an additive (Add, +, 0, -a) and a multiplicative (Mul, *, 1, a⁻¹) version. Lemmas for the additive side are prefixed with add_: add_assoc, add_comm, add_zero, neg_add_cancel, etc.

• "Class" suffix. MulOneClass, AddZeroClass are the bare algebraic laws for unit elements; they are weaker than a full monoid.

• Bundled morphisms. →*, →+, →+* are bundled: they package a function together with proofs that it preserves the relevant operations. Lemmas are named map_mul, map_add, map_one, map_zero, map_pow, map_neg.

• Subgroups and ideals. Subgroup G, Subring R, Ideal R are bundled sub-objects with membership a ∈ H, closed under the relevant operations (H.mul_mem, H.inv_mem, H.add_mem, etc.).

2.5.2. From operations to monoids🔗

At the bottom of the hierarchy sit the basic operation typeclasses:

• Mul α provides a multiplication * on α.

• Add α provides an addition + on α.

• One α provides a distinguished element 1 : α.

• Zero α provides a distinguished element 0 : α.

These are combined step by step:

• MulOneClass α : a type with * and 1, satisfying 1 * a = a and a * 1 = a.

• Monoid α : a MulOneClass with associativity of *.

• AddMonoid α : the additive version (with + and 0).

• CommMonoid α : a monoid where * is commutative.