Lattice seminorms

A seminorm monotone with respect to absolute value, together with its solid balls. Extracted from BanLat LocallySolid/WithSeminorms.lean at b00e59836016aa1099b8011add6b07385e66428e.

structure LatticeSeminorm (E : Type u) [AddCommGroup E] [Lattice E] [IsOrderedAddMonoid E] [VectorLattice E] extends Seminorm ℝ E : Type u

A lattice seminorm on a vector lattice is a seminorm that is monotone with respect to the lattice absolute value.

• toFun : E → ℝ
• map_zero' : self.toFun 0 = 0
• add_le' (r s : E) : self.toFun (r + s) ≤ self.toFun r + self.toFun s
• neg' (r : E) : self.toFun (-r) = self.toFun r
• smul' (a : ℝ) (x : E) : self.toFun (a • x) = ‖a‖ * self.toFun x
• monotone_abs' {x y : E} : |x| ≤ |y| → self.toSeminorm x ≤ self.toSeminorm y

  Monotonicity with respect to the lattice absolute value.

@[reducible, inline]

abbrev LatticeSeminorm.toSeminormFamily {E : Type u} [AddCommGroup E] [Lattice E] [IsOrderedAddMonoid E] [VectorLattice E] {ι : Type v} (p : ι → LatticeSeminorm E) : SeminormFamily ℝ E ι

The underlying seminorm family of a lattice seminorm family.

Equations

• LatticeSeminorm.toSeminormFamily p i = (p i).toSeminorm

theorem LatticeSeminorm.isSolid_of_mem_basisSets {E : Type u} [AddCommGroup E] [Lattice E] [IsOrderedAddMonoid E] [VectorLattice E] {ι : Type v} (p : ι → LatticeSeminorm E) {s : Set E} (hs : s ∈ (toSeminormFamily p).basisSets) : LatticeOrderedAddCommGroup.IsSolid s

Every basis set of the seminorm family associated to a family of lattice seminorms is solid.