Commit 2026-06-20 03:53 6eb4a1ce

View on Github →

feat: in a dense order, 𝓝[<] a has fun x ↦ Ico x a as a basis (#40523)

Estimated changes

added theorem nhdsGT_basis_Ioc
added theorem nhdsLT_basis_Ico