instLattice — Mathlib

English

The Lp-space is a lattice under the pointwise order; sup and inf are given by the pointwise sup and inf of representatives, and remain in Lp.

Русский

Пространство Lp является решёткой по точечному порядку; верхняя и нижняя границы задаются точечными максимумами и минимумами и остаются в Lp.

LaTeX

$$$\text{Lp}(E,p,\mu)$ is a lattice with $(f\vee g),(f\wedge g)\in \text{Lp}(E,p,\mu)$ for all $f,g$.$$

Lean4

instance instLattice : Lattice (Lp E p μ) :=
  Subtype.lattice
    (fun f g hf hg => by
      rw [mem_Lp_iff_memLp] at *
      exact (memLp_congr_ae (AEEqFun.coeFn_sup _ _)).mpr (hf.sup hg))
    fun f g hf hg => by
    rw [mem_Lp_iff_memLp] at *
    exact (memLp_congr_ae (AEEqFun.coeFn_inf _ _)).mpr (hf.inf hg)

Похожие утверждения