English
The structure LocallyFiniteOrder α is uniquely determined; i.e., there is at most one such structure on α.
Русский
Структура LocallyFiniteOrder α определена однозначно; т.е. существует не более одной такой структуры на α.
LaTeX
$$$\operatorname{Subsingleton}(\mathrm{LocallyFiniteOrder}(\alpha))$$$
Lean4
instance : Subsingleton (LocallyFiniteOrder α) :=
Subsingleton.intro fun h₀ h₁ =>
by
obtain
⟨h₀_finset_Icc, h₀_finset_Ico, h₀_finset_Ioc, h₀_finset_Ioo, h₀_finset_mem_Icc, h₀_finset_mem_Ico,
h₀_finset_mem_Ioc, h₀_finset_mem_Ioo⟩ :=
h₀
obtain
⟨h₁_finset_Icc, h₁_finset_Ico, h₁_finset_Ioc, h₁_finset_Ioo, h₁_finset_mem_Icc, h₁_finset_mem_Ico,
h₁_finset_mem_Ioc, h₁_finset_mem_Ioo⟩ :=
h₁
have hIcc : h₀_finset_Icc = h₁_finset_Icc := by
ext a b x
rw [h₀_finset_mem_Icc, h₁_finset_mem_Icc]
have hIco : h₀_finset_Ico = h₁_finset_Ico := by
ext a b x
rw [h₀_finset_mem_Ico, h₁_finset_mem_Ico]
have hIoc : h₀_finset_Ioc = h₁_finset_Ioc := by
ext a b x
rw [h₀_finset_mem_Ioc, h₁_finset_mem_Ioc]
have hIoo : h₀_finset_Ioo = h₁_finset_Ioo := by
ext a b x
rw [h₀_finset_mem_Ioo, h₁_finset_mem_Ioo]
simp_rw [hIcc, hIco, hIoc, hIoo]
