instLocallyFiniteOrderBot — Mathlib

English

If α and β have LocallyFiniteOrderBot structures, the product α × β also carries a LocallyFiniteOrderBot structure, with lower sets given by Iic(a) × Iic(b).

Русский

Если у α и β есть структуры LocallyFiniteOrderBot, то произведение α × β также имеет такую структуру, и нижние множества задаются как Iic(a) × Iic(b).

LaTeX

$$$ \text{LocallyFiniteOrderBot}(\alpha \times \beta) \;\text{with} \; Iic(a,b) = Iic(a) \times Iic(b) $$$

Lean4

instance instLocallyFiniteOrderBot : LocallyFiniteOrderBot (α × β) :=
  LocallyFiniteOrderBot.ofIic' (α × β) (fun x ↦ Iic x.1 ×ˢ Iic x.2) fun a x ↦ by
    rw [mem_product, mem_Iic, mem_Iic, le_def]

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