structure VecLatHom (X : Type u_1) (Y : Type u_2) [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] extends X →ₗ[ℝ] Y, LatticeHom X Y : Type (max u_1 u_2)

• toFun : X → Y
• map_add' (x y : X) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : ℝ) (x : X) : self.toFun (m • x) = (RingHom.id ℝ) m • self.toFun x
• map_sup' (a b : X) : self.toFun (a ⊔ b) = self.toFun a ⊔ self.toFun b
• map_inf' (a b : X) : self.toFun (a ⊓ b) = self.toFun a ⊓ self.toFun b

structure IsVecLatHom {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (f : X → Y) extends IsLinearMap ℝ f : Prop

• map_add (x y : X) : f (x + y) = f x + f y
• map_smul (c : ℝ) (x : X) : f (c • x) = c • f x
• map_sup' (x y : X) : f (x ⊔ y) = f x ⊔ f y
• map_inf' (x y : X) : f (x ⊓ y) = f x ⊓ f y

instance VecLatHom.instFunLike {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] : FunLike (VecLatHom X Y) X Y

Equations

• VecLatHom.instFunLike = { coe := fun (f : VecLatHom X Y) => f.toFun, coe_injective' := ⋯ }

theorem VecLatHom.isVecLatHom {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (f : VecLatHom X Y) : IsVecLatHom ⇑f

def VecLatHom.of_isVecLatHom {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (f : X → Y) (h : IsVecLatHom f) : VecLatHom X Y

Equations

• VecLatHom.of_isVecLatHom f h = { toFun := f, map_add' := ⋯, map_smul' := ⋯, map_sup' := ⋯, map_inf' := ⋯ }

instance VecLatHom.instLatticeHomClass {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] : LatticeHomClass (VecLatHom X Y) X Y

instance VecLatHom.instLinearMapClass {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] : LinearMapClass (VecLatHom X Y) ℝ X Y

@[simp]

theorem VecLatHom.toFun_eq_coe {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] {f : VecLatHom X Y} : f.toFun = ⇑f

theorem VecLatHom.map_abs {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (f : VecLatHom X Y) (x : X) : f |x| = |f x|

theorem VecLatHom.monotone {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (f : VecLatHom X Y) : Monotone ⇑f

def VecLatHom.of_abs {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (f : X →ₗ[ℝ] Y) (abs : ∀ (x : X), f |x| = |f x|) : VecLatHom X Y

Equations

• VecLatHom.of_abs f abs = { toLinearMap := f, map_sup' := ⋯, map_inf' := ⋯ }

def VecLatHom.comp {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] {Z : Type u_3} [AddCommGroup Z] [Lattice Z] [IsOrderedAddMonoid Z] [VectorLattice Z] (g : VecLatHom Y Z) (f : VecLatHom X Y) : VecLatHom X Z

Equations

• g.comp f = { toLinearMap := g.toLinearMap ∘ₗ f.toLinearMap, map_sup' := ⋯, map_inf' := ⋯ }

theorem VecLatHom.comp_apply {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] {Z : Type u_3} [AddCommGroup Z] [Lattice Z] [IsOrderedAddMonoid Z] [VectorLattice Z] (g : VecLatHom Y Z) (f : VecLatHom X Y) (x : X) : (g.comp f) x = g (f x)

noncomputable def VecLatHom.symm {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (f : VecLatHom X Y) (h : Function.Bijective ⇑f) : VecLatHom Y X

Equations

• f.symm h = { toLinearMap := ↑(LinearEquiv.ofBijective f.toLinearMap h).symm, map_sup' := ⋯, map_inf' := ⋯ }

theorem VecLatHom.symm_apply {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (f : VecLatHom X Y) (h : Function.Bijective ⇑f) (x : X) (y : Y) : (f.symm h) y = x ↔ y = f x

def IsVecLatHom.mk' {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (f : X → Y) (vlh : IsVecLatHom f) : VecLatHom X Y

Equations

• IsVecLatHom.mk' f vlh = { toFun := f, map_add' := ⋯, map_smul' := ⋯, map_sup' := ⋯, map_inf' := ⋯ }

@[simp]

theorem IsVecLatHom.mk'_apply {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] {f : X → Y} (vlh : IsVecLatHom f) (x : X) : (mk' f vlh) x = f x

theorem IsVecLatHom.of_abs {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] {f : X → Y} (lin : IsLinearMap ℝ f) (abs : ∀ (x : X), f |x| = |f x|) : IsVecLatHom f