instLocallyFiniteOrderTop — Mathlib

English

The product α×β has a LocallyFiniteOrderTop structure defined coordinatewise by Ici x1 ×ˢ Ici x2.

Русский

Произведение α×β приобретает структуру LocallyFiniteOrderTop по координатам как Ici x1 ×ˢ Ici x2.

LaTeX

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

Lean4

instance instLocallyFiniteOrderTop : LocallyFiniteOrderTop (α × β) :=
  LocallyFiniteOrderTop.ofIci' (α × β) (fun x => Ici x.1 ×ˢ Ici x.2) fun a x => by
    rw [mem_product, mem_Ici, mem_Ici, le_def]

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