toFinset_empty — Mathlib

English

The Finset of the empty set is empty.

Русский

Пустое множество имеет пустой Finset.

LaTeX

$$$(\emptyset : Set\ α).toFinset = \emptyset$$$

Lean4

@[simp]
theorem toFinset_empty [Fintype (∅ : Set α)] : (∅ : Set α).toFinset = ∅ :=
  by
  ext
  simp
    /- TODO Without the coercion arrow (`↥`) there is an elaboration bug in the following two;
    it essentially infers `Fintype.{v} (Set.univ.{u} : Set α)` with `v` and `u` distinct.
    Reported in https://github.com/leanprover-community/lean/issues/672 -/

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