instFintype — Mathlib

English

If α is finite, then Sym2 α is finite, given by elems := univ.sym2 with a complete map.

Русский

Если α конечна, то Sym2 α конечна, задана через элементы univ.sym2 и полноту отображения.

LaTeX

$$If $Fintype(\alpha)$ then $Fintype(Sym2(\alpha))$ with $elems := Finset.univ.sym2$ and $complete$ as in the definition.$$

Lean4

instance _root_.Sym2.instFintype [Fintype α] : Fintype (Sym2 α)
    where
  elems := Finset.univ.sym2
  complete := fun x ↦ by rw [mem_sym2_iff];
    exact
      (fun a _ ↦ mem_univ a)
        -- Note(kmill): Using a default argument to make this simp lemma more general.

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