[codex] Add finset supremum and infimum convergence lemmas#8

Draft

CoolRmal wants to merge 25 commits into

mainfrom

codex/tendsto-finset-sup-isup

Commits on Jun 13, 2026

feat(Combinatorics/SimpleGraph/Maps): add theorems about composition (#37624)
IvanRenison
committed
feat(RingTheory/Extension): `h1CotangentEquivCotangent` (#39520)
BryceT233
committed
feat: connections between order, `realPart` and `imaginaryPart` in star ordered rings (#40565)
j-loreaux
committed
chore(CategoryTheory/Filtered): generalise criteria for filteredness of `CostructuredArrow` (#40559)
chrisflav
committed
feat: the canonical approximate unit in a C⋆-algebra is not `⊥` (#40566)
j-loreaux
committed
feat(Order/ConditionallyCompleteLattice/Finset): `sSup s ≠ ⊤` in a `CompleteLinearOrder` for a finite set without `⊤` (#38356)
SnirBroshi
committed
feat: use `alias_in` attribute for CW complexes (#38785)
scholzhannah
committed
feat(Probability/Decision): Bayes estimators (#39810)
RemyDegenne
committed
feat: variants of lemmas in CondJensen with a.e. inequalities for the trimmed measure (#39819)

mathlib-splicebot[bot]
and
RemyDegenne
committed
chore: replace `(by rfl)` with `rfl` (#40371)
felixpernegger
committed
feat: clean up `PositiveLinearMap` and add API (#40492)
j-loreaux
committed
feat: selfadjointness for comparable elements in a star ordered ring (#40513)
j-loreaux
committed
feat(Analysis/Complex/Exponential): add new bounds on exponential (#39690)
b-mehta
committed

Commits on Jun 14, 2026