instSubsingletonLocallyFiniteOrderTop

English

The class LocallyFiniteOrderTop α is a Subsingleton; any two such top-structured orders coincide.

Русский

Класс LocallyFiniteOrderTop α является Subsingleton; любые две такие структуры совпадают.

LaTeX

$$$\operatorname{Subsingleton}(\mathrm{LocallyFiniteOrderTop}(\alpha))$$$

Lean4

instance : Subsingleton (LocallyFiniteOrderTop α) :=
  Subsingleton.intro fun h₀ h₁ =>
    by
    obtain ⟨h₀_finset_Ioi, h₀_finset_Ici, h₀_finset_mem_Ici, h₀_finset_mem_Ioi⟩ := h₀
    obtain ⟨h₁_finset_Ioi, h₁_finset_Ici, h₁_finset_mem_Ici, h₁_finset_mem_Ioi⟩ := h₁
    have hIci : h₀_finset_Ici = h₁_finset_Ici := by
      ext a b
      rw [h₀_finset_mem_Ici, h₁_finset_mem_Ici]
    have hIoi : h₀_finset_Ioi = h₁_finset_Ioi := by
      ext a b
      rw [h₀_finset_mem_Ioi, h₁_finset_mem_Ioi]
    simp_rw [hIci, hIoi]

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