fintype_of_univ_finite

Stream: Is there code for X?

[Johan Commelin]

I couldn't find this in mathlib, which seems surprising

/-- If `(set.univ : set X)` is finite then `X` is a finite type. -/
noncomputable
def fintype_of_univ_finite {X : Type*} (H : set.finite (set.univ : set X)) :
  fintype X :=
begin
  choose t ht using H.exists_finset,
  refine ⟨t, _⟩,
  simpa only [set.mem_univ, iff_true] using ht
end

[Johan Commelin]

PRd in #6164