English
LocallyFinsuppWithin(U,Y) inherits a lattice structure from Y, with lattice operations defined pointwise.
Русский
LocallyFinsuppWithin(U,Y) наследует решётку из Y, операции решётки определяются по компонентам.
LaTeX
$$$\\text{LocallyFinsuppWithin}(U,Y) \\text{ carries a lattice structure with }\\; \\vee = \\max, \\wedge = \\min$$$
Lean4
instance [Lattice Y] [Zero Y] : Lattice (locallyFinsuppWithin U Y)
where
le := (· ≤ ·)
lt := (· < ·)
le_refl := by simp [le_def]
le_trans D₁ D₂ D₃ h₁₂ h₂₃ := fun x ↦ (h₁₂ x).trans (h₂₃ x)
le_antisymm D₁ D₂ h₁₂
h₂₁ := by
ext x
exact le_antisymm (h₁₂ x) (h₂₁ x)
sup := max
le_sup_left D₁ D₂ := fun x ↦ by simp
le_sup_right D₁ D₂ := fun x ↦ by simp
sup_le D₁ D₂ D₃ h₁₃ h₂₃ := fun x ↦ by simp [h₁₃ x, h₂₃ x]
inf := min
inf_le_left D₁ D₂ := fun x ↦ by simp
inf_le_right D₁ D₂ := fun x ↦ by simp
le_inf D₁ D₂ D₃ h₁₃ h₂₃ := fun x ↦ by simp [h₁₃ x, h₂₃ x]
