Riddle about SeminormedAddGroup

Stream: maths

[Kenny Lau]

Is there a SeminormedAddGroup where the image of the norm is (similar enough to) the set {0, 1+1, 1+1/2, 1+1/3, 1+1/4, ...}?

[Kenny Lau]

(where "similar enough to" means that it's order-isomorphic and 0 is still not the limit)

[Matthew Jasper]

ℕ →₀ ZMod 2 with ‖f‖ = 1 + 1 / (1 + inf {n|f n ≠ 0})

[Edward van de Meent]

i'm not sure that works? surely you must have that ‖0‖=0?

[Edward van de Meent]

or am i overlooking something?

[Matthew Jasper]

I meant for the equality to be for non-zero f

[Kenny Lau]

so i wanted to prove that the nhds 0 is generated by { y : |y| < |x| } for x such that |x|>0 but i couldn’t rule out this case (following mathlib’s convention i would prove it in the highest generality, since this is obviously true for fields)

[Kenny Lau]

so this counterexample is interesting because {0} is open but you cant write it “internally” using B(0,|x|)

[Kenny Lau]

cc @Andrew Yang

[Yakov Pechersky]

Since you have a singleton open, you have a discrete topology. This is finer than docs#Valuation.subgroups_basis