Theorem tendsto_seminormFromConst_seq_atTop

Modification history

2026-01-28 02:37

Mathlib/Analysis/Normed/Unbundled/SeminormFromConst.lean

chore(Analysis/Normed): redefine `seminormFromConst'` without `choose` (#33939) …

Added tendsto_seminormFromConst_seq_atTop View on Github →