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

source

@[simp]

theorem Counterexample.SeminormNotDistrib.p_toFun :

∀ (a : ℝ × ℝ), ↑Counterexample.SeminormNotDistrib.p a = |a.fst| ⊔ |a.snd|

source

noncomputable def Counterexample.SeminormNotDistrib.p :

Seminorm ℝ (ℝ × ℝ)

Instances For

source

@[simp]

theorem Counterexample.SeminormNotDistrib.q1_toFun (x : ℝ × ℝ) :

↑Counterexample.SeminormNotDistrib.q1 x = 4 • |x.fst|

source

noncomputable def Counterexample.SeminormNotDistrib.q1 :

Seminorm ℝ (ℝ × ℝ)

Instances For

source

@[simp]

theorem Counterexample.SeminormNotDistrib.q2_toFun (x : ℝ × ℝ) :

↑Counterexample.SeminormNotDistrib.q2 x = 4 • |x.snd|

source

noncomputable def Counterexample.SeminormNotDistrib.q2 :

Seminorm ℝ (ℝ × ℝ)

Instances For

source

theorem Counterexample.SeminormNotDistrib.eq_one :

↑(Counterexample.SeminormNotDistrib.p ⊔ Counterexample.SeminormNotDistrib.q1 ⊓ Counterexample.SeminormNotDistrib.q2) (1, 1) = 1

source

theorem Counterexample.SeminormNotDistrib.not_distrib :

¬(Counterexample.SeminormNotDistrib.p ⊔ Counterexample.SeminormNotDistrib.q1) ⊓ (Counterexample.SeminormNotDistrib.p ⊔ Counterexample.SeminormNotDistrib.q2) ≤ Counterexample.SeminormNotDistrib.p ⊔ Counterexample.SeminormNotDistrib.q1 ⊓ Counterexample.SeminormNotDistrib.q2

This is a counterexample to the distributivity of the lattice Seminorm ℝ (ℝ × ℝ).