The lattice of seminorms is not distributive #
We provide an example of three seminorms over the ℝ-vector space ℝ×ℝ which don't satisfy the lattice
distributivity property (p ⊔ q1) ⊓ (p ⊔ q2) ≤ p ⊔ (q1 ⊓ q2)
.
This proves the lattice Seminorm ℝ (ℝ × ℝ)
is not distributive.
References #
- https://en.wikipedia.org/wiki/Seminorm#Examples
@[simp]
@[simp]
theorem
Counterexample.SeminormNotDistrib.q1_toFun
(x : ℝ × ℝ)
:
↑Counterexample.SeminormNotDistrib.q1 x = 4 • |x.fst|
@[simp]
theorem
Counterexample.SeminormNotDistrib.q2_toFun
(x : ℝ × ℝ)
:
↑Counterexample.SeminormNotDistrib.q2 x = 4 • |x.snd|
This is a counterexample to the distributivity of the lattice Seminorm ℝ (ℝ × ℝ)
.