instLocallyFiniteOrderTopSubtypeLeOfDecidableLEOfLocallyFiniteOrder

English

The subset { x ∈ α | x ≤ y } inherits a LocallyFiniteOrderTop structure from α, with finsetIoi and finsetIci given by Ioc and Icc with top y, respectively.

Русский

Подпоследовательность { x ∈ α | x ≤ y } наследует структуру LocallyFiniteOrderTop от α, причём finsetIoi и finsetIci задаются как Ioc и Icc с верхней границей 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 α] [DecidableLE α] [LocallyFiniteOrder α] :
    LocallyFiniteOrderTop { x : α // x ≤ y }
    where
  finsetIoi a := Finset.Ioc a ⟨y, by rfl⟩
  finsetIci a := Finset.Icc a ⟨y, by rfl⟩
  finset_mem_Ici a
    b := by
    simp only [Finset.mem_Icc, and_iff_left_iff_imp]
    exact fun _ => b.property
  finset_mem_Ioi a
    b := by
    simp only [Finset.mem_Ioc, and_iff_left_iff_imp]
    exact fun _ => b.property

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