mathlib3 documentation

mathlib-counterexamples / seminorm_lattice_not_distrib

The lattice of seminorms is not distributive #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

source
@[simp]
theorem counterexample.seminorm_not_distrib.p_to_fun (ᾰ : ℝ × ℝ) :
⇑counterexample.seminorm_not_distrib.p ᾰ = |ᾰ.fst| ⊔ |ᾰ.snd|
source
noncomputable def counterexample.seminorm_not_distrib.p  :
seminorm ℝ (ℝ × ℝ)
Equations
source
@[simp]
theorem counterexample.seminorm_not_distrib.q1_to_fun (x : ℝ × ℝ) :
⇑counterexample.seminorm_not_distrib.q1 x = 4 • |x.fst|
source
noncomputable def counterexample.seminorm_not_distrib.q1  :
seminorm ℝ (ℝ × ℝ)
Equations
source
@[simp]
theorem counterexample.seminorm_not_distrib.q2_to_fun (x : ℝ × ℝ) :
⇑counterexample.seminorm_not_distrib.q2 x = 4 • |x.snd|
source
noncomputable def counterexample.seminorm_not_distrib.q2  :
seminorm ℝ (ℝ × ℝ)
Equations
source
theorem counterexample.seminorm_not_distrib.eq_one  :
⇑(counterexample.seminorm_not_distrib.p ⊔ counterexample.seminorm_not_distrib.q1 ⊓ counterexample.seminorm_not_distrib.q2) (1, 1) = 1
source
theorem counterexample.seminorm_not_distrib.not_distrib  :
¬(counterexample.seminorm_not_distrib.p ⊔ counterexample.seminorm_not_distrib.q1) ⊓ (counterexample.seminorm_not_distrib.p ⊔ counterexample.seminorm_not_distrib.q2) ≤ counterexample.seminorm_not_distrib.p ⊔ counterexample.seminorm_not_distrib.q1 ⊓ counterexample.seminorm_not_distrib.q2

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