Zulip Chat Archive

Stream: Is there code for X?

Topic: subsingleton from card = 1


view this post on Zulip Eric Wieser (Mar 16 2021 at 16:03):

I can't seem to find these:

import data.fintype.basic

variables {n : Type*} [fintype n] (h : fintype.card n = 1)

example : unique n := by library_search
example : subsingleton n := by library_search

view this post on Zulip Gabriel Ebner (Mar 16 2021 at 16:08):

docs#fintype.card_le_one_iff_subsingleton

view this post on Zulip Eric Wieser (Mar 16 2021 at 16:11):

Thanks, that beats my

  obtain k, heq := fintype.card_eq_one_iff.mp h,
  exact subsingleton_of_forall_eq k heq,

by a line


Last updated: May 07 2021 at 18:19 UTC