Theorem Finset.HasAntidiagonal.tendsto_sup'_antidiagonal_cofinite

Modification history

2026-06-29 09:26
Mathlib/Algebra/Order/Antidiag/Tendsto.lean
feat: define multivariate restricted power series (#32692) …
Added Finset.HasAntidiagonal.tendsto_sup'_antidiagonal_cofiniteView on Github →