English
The type LocallyFiniteOrder α is a Subsingleton, i.e., any two LocallyFiniteOrder structures on α are equal.
Русский
Тип LocallyFiniteOrder α является Subsingleton, то есть любые две структуры локально-конечного порядка на α равны друг другу.
LaTeX
$$$\operatorname{Subsingleton}(\mathrm{LocallyFiniteOrder}(\alpha))$$$
Lean4
/-- A fintype is a locally finite order.
This is not an instance as it would not be defeq to better instances such as
`Fin.locallyFiniteOrder`.
-/
abbrev toLocallyFiniteOrder [Fintype α] [DecidableLT α] [DecidableLE α] : LocallyFiniteOrder α
where
finsetIcc a b := (Set.Icc a b).toFinset
finsetIco a b := (Set.Ico a b).toFinset
finsetIoc a b := (Set.Ioc a b).toFinset
finsetIoo a b := (Set.Ioo a b).toFinset
finset_mem_Icc a b x := by simp only [Set.mem_toFinset, Set.mem_Icc]
finset_mem_Ico a b x := by simp only [Set.mem_toFinset, Set.mem_Ico]
finset_mem_Ioc a b x := by simp only [Set.mem_toFinset, Set.mem_Ioc]
finset_mem_Ioo a b x := by simp only [Set.mem_toFinset, Set.mem_Ioo]
