Zulip Chat Archive

Stream: Is there code for X?

Topic: fintype_of_univ_finite


view this post on Zulip Johan Commelin (Feb 10 2021 at 15:24):

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

view this post on Zulip Johan Commelin (Feb 10 2021 at 21:36):

PRd in #6164


Last updated: May 07 2021 at 23:11 UTC