instLocallyFiniteOrderTopSubtypeLtOfDecidableLTOfLocallyFiniteOrder

English

The subtype { x ≤ y } carries a LocallyFiniteOrderTop structure with finsetIoi as Ioc(a,y) and finsetIci as Icc(a,y).

Русский

Подтип { x ≤ y } имеет структуру LocallyFiniteOrderTop; finsetIoi задаётся как Ioc(a,y), finsetIci как Icc(a,y).

LaTeX

$$$\\text{LocallyFiniteOrderTop}\\;\\{ x \\in \\alpha \\mid x \\le y \\}$ with finsetIoi(a) = \\mathrm{Ioc}(a,y),\\; finsetIci(a) = \\mathrm{Icc}(a,y)$$$

Lean4

instance (priority := low) [Preorder α] [DecidableLT α] [LocallyFiniteOrder α] :
    LocallyFiniteOrderTop { x : α // x < y }
    where
  finsetIoi a := (Finset.Ioo (↑a) y).subtype _
  finsetIci a := (Finset.Ico (↑a) y).subtype _
  finset_mem_Ici a
    b := by
    simp only [Finset.mem_subtype, Finset.mem_Ico, Subtype.coe_le_coe, and_iff_left_iff_imp]
    exact fun _ => b.property
  finset_mem_Ioi a
    b := by
    simp only [Finset.mem_subtype, Finset.mem_Ioo, Subtype.coe_lt_coe, and_iff_left_iff_imp]
    exact fun _ => b.property

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