instLocallyFiniteOrder — Mathlib

English

The product of locally finite ordered sets α and β carries a LocallyFiniteOrder structure given coordinatewise by Icc sets.

Русский

Произведение локально конечных упорядоченных множеств α и β наделено структурой LocallyFiniteOrder, где интервалы координатно определяются через Icc.

LaTeX

$$$ \operatorname{LocallyFiniteOrder}(\alpha \times \beta) $$$

Lean4

instance instLocallyFiniteOrder : LocallyFiniteOrder (α × β) :=
  LocallyFiniteOrder.ofIcc' (α × β) (fun x y ↦ Icc x.1 y.1 ×ˢ Icc x.2 y.2) fun a b x => by
    rw [mem_product, mem_Icc, mem_Icc, and_and_and_comm, le_def, le_def]

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