instFintypeOfDecidableLT — Mathlib

English

Let α be a finite preorder with a decidable linear order; the LTSeries construction on α yields a finite type.

Русский

Пусть α — конечное упорядоченное множество с предикатом строгого порядка; конструкция LTSeries над α образует конечный тип.

LaTeX

$$$|\\mathrm{LTSeries}(\\alpha)| < \\infty$$$

Lean4

instance [DecidableLT α] : Fintype (LTSeries α)
    where
  elems := Finset.univ.map (injStrictMono (Fintype.card α))
  complete
    s := by
    have bl := s.length_lt_card
    obtain ⟨l, f, mf⟩ := s
    simp_rw [Finset.mem_map, Finset.mem_univ, true_and, Subtype.exists]
    use ⟨⟨l, bl⟩, f⟩, Fin.strictMono_iff_lt_succ.mpr mf; rfl

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