instLocallyFiniteOrderBotSubtypeLeOfDecidableLEOfLocallyFiniteOrder

English

The subtype { x ≤ y } also forms a LocallyFiniteOrderTop when DecidableLE is assumed, with the same finset prescriptions as above.

Русский

Подтип { x ≤ y } образует LocallyFiniteOrderTop при предполагаемом DecidableLE, с теми же правилами для конечных множеств.

LaTeX

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

Lean4

instance (priority := low) [Preorder α] [DecidableLE α] [LocallyFiniteOrder α] :
    LocallyFiniteOrderBot { x : α // y ≤ x }
    where
  finsetIio a := Finset.Ico ⟨y, by rfl⟩ a
  finsetIic a := Finset.Icc ⟨y, by rfl⟩ a
  finset_mem_Iic a
    b := by
    simp only [Finset.mem_Icc, and_iff_right_iff_imp]
    exact fun _ => b.property
  finset_mem_Iio a
    b := by
    simp only [Finset.mem_Ico, and_iff_right_iff_imp]
    exact fun _ => b.property

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