instLatticeOfTopologicalLattice — Mathlib

English

If β is a lattice and a TopologicalLattice, then C(α, β) has a lattice structure with pointwise sup and inf.

Русский

Если β — решётка и TopologicalLattice, то на C(α, β) задана решётка с точечными максимумом и минимумом.

LaTeX

$$\$Lattice\\, C(α, β)\$ under pointwise operations.$$

Lean4

instance [Lattice β] [TopologicalLattice β] : Lattice C(α, β) :=
  DFunLike.coe_injective.lattice _ (fun _ _ ↦ rfl) fun _ _ ↦ rfl

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