Documentation

Counterexamples.SeminormLatticeNotDistrib

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 #

@[simp]
theorem Counterexample.SeminormNotDistrib.p_toFun :
∀ (a : × ), Counterexample.SeminormNotDistrib.p a = |a.1| |a.2|
@[simp]
theorem Counterexample.SeminormNotDistrib.q1_toFun (x : × ) :
Counterexample.SeminormNotDistrib.q1 x = 4 |x.1|
@[simp]
theorem Counterexample.SeminormNotDistrib.q2_toFun (x : × ) :
Counterexample.SeminormNotDistrib.q2 x = 4 |x.2|