instLocallyFiniteOrderBotSubtypeLtOfDecidableLTOfLocallyFiniteOrder

English

The subtype { y < x } carries a LocallyFiniteOrderBot structure, with finsetIio and finsetIic given by Ioo(y,x) and Ioc(y,x) respectively.

Русский

Подтип { y < x } имеет структуру LocallyFiniteOrderBot; finsetIio и finsetIic задаются как Ioo(y,x) и Ioc(y,x).

LaTeX

$$$\\text{LocallyFiniteOrderBot}\\;\\{ x \\in \\alpha \\mid y < x \\}$ with finsetIio(a) = \\mathrm{Ioo}(y,a),\\; finsetIic(a) = \\mathrm{Ioc}(y,a)$$$

Lean4

instance (priority := low) [Preorder α] [DecidableLT α] [LocallyFiniteOrder α] :
    LocallyFiniteOrderBot { x : α // y < x }
    where
  finsetIio a := (Finset.Ioo y ↑a).subtype _
  finsetIic a := (Finset.Ioc y ↑a).subtype _
  finset_mem_Iic a
    b := by
    simp only [Finset.mem_subtype, Finset.mem_Ioc, Subtype.coe_le_coe, and_iff_right_iff_imp]
    exact fun _ => b.property
  finset_mem_Iio a
    b := by
    simp only [Finset.mem_subtype, Finset.mem_Ioo, Subtype.coe_lt_coe, and_iff_right_iff_imp]
    exact fun _ => b.property

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