5.1.1. Notation and naming conventions🔗

Several symbols below are unicode characters typed in VS Code via a backslash escape (e.g. \le produces ≤). Hover over a symbol in the editor to see how to type it.

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.

5.1.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).

5.1.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.

5.1.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

5.1.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.

5.1.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.

5.1.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.

5.1.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.

5.2.1. Notation and naming conventions🔗

Unicode symbols can be typed via a backslash escape (e.g. \inv produces ⁻¹). Hover over a symbol in VS Code to see how to type it.

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.).

5.2.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.

5.2.3. Groups🔗

A group is a monoid where every element has an inverse.

• Group α : multiplicative group (inverse written a⁻¹, typed \inv or \-1).

• AddGroup α : additive group (inverse written -a).

• CommGroup α, AddCommGroup α : commutative (abelian) versions.

5.2.4. Rings and fields🔗

A ring has both addition (forming an abelian group) and multiplication (forming a monoid), linked by distributivity.

• Ring α : a (unital) ring.

• CommRing α : a commutative ring.

• Field α : a field (commutative ring where every nonzero element is invertible).

Mathlib also provides ordered variants:

• OrderedRing α : a ring with a compatible order.

• LinearOrderedField α : a linearly ordered field (like ℝ or ℚ).

5.2.5. Morphisms🔗

Algebraic morphisms are functions that preserve the relevant structure. Mathlib uses bundled morphisms (structures carrying both the function and the proof of preservation).

• MonoidHom (notation →*) : maps preserving * and 1.

• AddMonoidHom (notation →+) : maps preserving + and 0.

• RingHom (notation →+*) : maps preserving both +, *, 0, 1.

5.2.6. Substructures🔗

Mathlib provides types for substructures of algebraic objects:

• Subgroup G : a subgroup of G.

• Subring R : a subring of R.

• Subalgebra R A : a subalgebra of A over R.

• Ideal R : an ideal of a (commutative) ring R.

These are bundled: a Subgroup G consists of a carrier set together with proofs that it is closed under the group operations.

5.2.7. Quotient structures🔗

Given a normal subgroup N of a group G, the quotient G ⧸ N is again a group. Similarly, given an ideal I of a ring R, the quotient R ⧸ I is a ring.

The quotient map is a ring homomorphism:

Ideal.Quotient.mk.{u} {R : Type u} [Ring R] (I : Ideal R)
  [I.IsTwoSided] : R →+* R ⧸ I
Ideal.Quotient.mk.{u} {R : Type u}
  [Ring R] (I : Ideal R) [I.IsTwoSided] :
  R →+* R ⧸ I

5.2.8. The ext tactic for algebraic structures🔗

The ext tactic is very useful when proving equalities between algebraic objects. For instance, two subgroups are equal if they have the same elements; two morphisms are equal if they agree on all inputs.

5.2.9. Navigating the hierarchy🔗

When working with Mathlib's algebraic hierarchy, recall the exploration commands introduced in the Lean chapter: #check for types, #print for definitions and fields of typeclasses, inferInstance for checking whether a given instance exists, and exact? / apply? for lemma search. In addition:

• Look at Mathlib.Algebra and Mathlib.GroupTheory for the files relevant to the structure you are working with.

• Lemma names follow the predictable pattern <operation>_<result>, e.g. mul_assoc, add_comm, map_mul, inv_inv.

The ring tactic is a powerful decision procedure that closes goals that are identities in commutative (semi)rings. Similarly, group works for group identities, and field_simp helps simplify field expressions involving division.

5.3.1. Notation and naming conventions🔗

Many filter-related symbols are unicode and typed via backslash escapes in VS Code (hover over a symbol to see its input sequence).

Naming hints.

• F ≤ G is pronounced "F is finer than G": smaller filters contain more sets. The slogan is: the smaller the filter, the bigger its collection of sets.

• The prefix mem_ (as in mem_principal, mem_atTop_sets, mem_nhds_iff) names lemmas that characterize membership in a given filter.

• 𝓟 and 𝓝 are mathematical script letters, typed \McP and \nhds; they are notation, not definitions.

• ⁻¹' is the preimage of a set under a function (not to be confused with the inverse ⁻¹ of a group element); it is typed \inv' (or \i\n\v ' in sequence).

5.3.2. Motivation: why filters?🔗

In a traditional analysis course one meets many similar-looking definitions:

• A sequence a : ℕ → ℝ converges to l if for every ε > 0 there exists N such that for all n ≥ N, |a n - l| < ε.

• A function f : ℝ → ℝ has limit l at x₀ if for every ε > 0 there exists δ > 0 such that for all x with 0 < |x - x₀| < δ, |f x - l| < ε.

• A function f : ℝ → ℝ tends to +∞ as x → +∞ if for every M there exists N such that for all x ≥ N, f x ≥ M.

All of these have the shape: "for sufficiently large/close inputs, the output lies in a given set." Filters capture this pattern abstractly.

5.3.3. Filters as generalized subsets🔗

Morally, a filter on a type α is a generalized subset of α. Every ordinary subset gives rise to a filter, but there are other filters representing "ideas" that cannot be described by a single subset, such as an infinitesimal neighborhood of a point in a topological space, or a neighborhood of ∞ in a totally ordered set. Isaac Newton wanted dx to be "a real number infinitesimally close to 0"; filters are a modern way to recover such thoughts.

The property we want a generalized subset F to have is that it is uniquely determined by the actual subsets which contain F. If F is a generalized subset of α, what properties should the collection of actual subsets containing F have?

1. If S contains F and S ⊆ T, then T contains F.

2. If S and T both contain F, then so does S ∩ T.

3. The whole type Set.univ : Set α contains F.

These three axioms turn out to be enough: a filter is modelled precisely as a collection of subsets of α satisfying them.

5.3.4. The formal definition🔗

The Mathlib definition, rendered directly from the library:

Filter.{u_1} (α : Type u_1) : Type u_1
Filter.{u_1} (α : Type u_1) : Type u_1

Filter.mk.{u_1}

sets : Set (Set α)

univ_sets : Set.univ ∈ self.sets

sets_of_superset : ∀ {x y : Set α}, x ∈ self.sets → x ⊆ y → y ∈ self.sets

inter_sets : ∀ {x y : Set α}, x ∈ self.sets → y ∈ self.sets → x ∩ y ∈ self.sets

Some authors add a fourth axiom forbidding ∅ ∈ sets. Mathlib does not: this is analogous to disallowing a ring as an ideal of itself. It makes the initial definition cleaner but introduces many awkward edge cases later, so Mathlib keeps the "empty filter" ⊥ as a legitimate object.

If F : Filter α and S : Set α, the notation S ∈ F is sugar for S ∈ F.sets. Think of it as morally meaning F ⊆ S -- but of course that expression does not type-check, because F is a filter, not a set.

The axioms are restated in the Filter namespace under friendlier names, rendered here directly from Mathlib:

Filter.univ_mem.{u_1} {α : Type u_1} {f : Filter α} : Set.univ ∈ f
Filter.univ_mem.{u_1} {α : Type u_1}
  {f : Filter α} : Set.univ ∈ f

Filter.mem_of_superset.{u_1} {α : Type u_1} {f : Filter α} {x y : Set α}
  (hx : x ∈ f) (hxy : x ⊆ y) : y ∈ f
Filter.mem_of_superset.{u_1}
  {α : Type u_1} {f : Filter α}
  {x y : Set α} (hx : x ∈ f)
  (hxy : x ⊆ y) : y ∈ f

Filter.inter_mem.{u_1} {α : Type u_1} {f : Filter α} {s t : Set α}
  (hs : s ∈ f) (ht : t ∈ f) : s ∩ t ∈ f
Filter.inter_mem.{u_1} {α : Type u_1}
  {f : Filter α} {s t : Set α}
  (hs : s ∈ f) (ht : t ∈ f) : s ∩ t ∈ f

5.3.5. The order on filters🔗

Filters form a partial order by ≤. The definition is

F ≤ G ↔ G.sets ⊆ F.sets

which looks reversed, but matches the "generalized subset" intuition: if F is contained in G as generalized subsets, then every actual subset containing G also contains F, so G.sets ⊆ F.sets. A useful slogan:

The smaller the filter, the more sets it has.

The API lemma is:

Filter.le_def.{u_1} {α : Type u_1} {f g : Filter α} :
  f ≤ g ↔ ∀ x ∈ g, x ∈ f
Filter.le_def.{u_1} {α : Type u_1}
  {f g : Filter α} :
  f ≤ g ↔ ∀ x ∈ g, x ∈ f

5.3.6. The principal filter🔗

The simplest filter is the principal filter, with notation 𝓟 s. It is the filter whose sets are exactly the supersets of s -- i.e. the generalized subset corresponding to the ordinary subset s.

Filter.principal.{u_1} {α : Type u_1} (s : Set α) : Filter α
Filter.principal.{u_1} {α : Type u_1}
  (s : Set α) : Filter α

5.3.7. The atTop filter🔗

On any preorder, Filter.atTop is the filter of sets that contain all sufficiently large elements. Morally, atTop is a "neighborhood of ∞": it represents "arbitrarily large elements" even though no single largest element exists.

Filter.atTop.{u_3} {α : Type u_3} [Preorder α] : Filter α
Filter.atTop.{u_3} {α : Type u_3}
  [Preorder α] : Filter α

5.3.8. The cofinite filter🔗

Another instructive example: on any type α, the cofinite filter consists of sets whose complement is finite.

Filter.cofinite.{u_2} {α : Type u_2} : Filter α
Filter.cofinite.{u_2} {α : Type u_2} :
  Filter α

This filter is a generalized subset of α representing "almost every element". On ℕ, the cofinite filter is strictly smaller than atTop (every cofinite set eventually contains all large n, but the set of even numbers is in atTop... wait -- actually it is not; and conversely, the set of even numbers is not cofinite). Comparing these two filters is a good way to train the "generalized subset" intuition.

5.3.9. Filter.map: the pushforward🔗

Given F : Filter α and m : α → β, there is a natural way to build a filter on β: a set s : Set β is in the pushforward if its preimage is in F. This is the filter-theoretic counterpart of the image of a subset.

Filter.map.{u_1, u_2} {α : Type u_1} {β : Type u_2} (m : α → β)
  (f : Filter α) : Filter β
Filter.map.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} (m : α → β)
  (f : Filter α) : Filter β

There is also a pullback:

Filter.comap.{u_1, u_2} {α : Type u_1} {β : Type u_2} (m : α → β)
  (f : Filter β) : Filter α
Filter.comap.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} (m : α → β)
  (f : Filter β) : Filter α

map and comap form a Galois connection:

Filter.map_le_iff_le_comap.{u_1, u_2} {α : Type u_1} {β : Type u_2}
  {f : Filter α} {g : Filter β} {m : α → β} :
  Filter.map m f ≤ g ↔ f ≤ Filter.comap m g
Filter.map_le_iff_le_comap.{u_1, u_2}
  {α : Type u_1} {β : Type u_2}
  {f : Filter α} {g : Filter β}
  {m : α → β} :
  Filter.map m f ≤ g ↔
    f ≤ Filter.comap m g

5.3.10. Filter.Tendsto: the general notion of limit🔗

With map in hand, the general definition of a limit is strikingly short:

Filter.Tendsto.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β)
  (l₁ : Filter α) (l₂ : Filter β) : Prop
Filter.Tendsto.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} (f : α → β)
  (l₁ : Filter α) (l₂ : Filter β) : Prop

Unpacking: Tendsto f l₁ l₂ says that for every s ∈ l₂, the preimage f ⁻¹' s is in l₁. In the generalized-subset picture, it says that f sends the generalized subset l₁ into the generalized subset l₂.

This single definition unifies all classical limits:

Composition: if a → l and f is continuous at l, then f ∘ a → f l:

Filter.Tendsto.comp.{u_1, u_2, u_3} {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {f : α → β} {g : β → γ} {x : Filter α} {y : Filter β}
  {z : Filter γ} (hg : Filter.Tendsto g y z)
  (hf : Filter.Tendsto f x y) : Filter.Tendsto (g ∘ f) x z
Filter.Tendsto.comp.{u_1, u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {f : α → β} {g : β → γ}
  {x : Filter α} {y : Filter β}
  {z : Filter γ}
  (hg : Filter.Tendsto g y z)
  (hf : Filter.Tendsto f x y) :
  Filter.Tendsto (g ∘ f) x z

5.3.11. Filter.Eventually and Filter.Frequently🔗

Filters let us speak precisely about something being true "eventually". Filter.Eventually p F, with notation ∀ᶠ x in F, p x, is defined as {x | p x} ∈ F. Read it as: "p holds for generalized-almost-all x with respect to F."

• For F = atTop on ℕ, ∀ᶠ n in atTop, p n means "for all sufficiently large n, p n".

• For F = nhds x₀, ∀ᶠ x in nhds x₀, p x means "p holds on a neighborhood of x₀".

• For F = cofinite, it means "p holds off a finite set".

The dual Filter.Frequently p F (notation ∃ᶠ x in F, p x) is the negation of Eventually (¬ p) and means "p holds on an F-non-negligible set".

When you have several ∀ᶠ-hypotheses and want to conclude another ∀ᶠ-statement pointwise, the dedicated tactic filter_upwards [h₁, h₂, …] with x h₁ h₂ … intersects them and hands you the pointwise goal: