Zulip Chat Archive

Stream: Is there code for X?

Topic: subsingleton_of_card_eq_one

Kevin Buzzard (Jul 30 2023 at 20:31):

Do we not have this? I'm surprised.

lemma subsingleton_of_card_eq_one {X : Type _} [Fintype X] (h : Fintype.card X = 1) :
    Subsingleton X := by
  rw [Fintype.card_eq_one_iff_nonempty_unique] at h
  cases h
  infer_instance

Should I dump it in Data.Fintype.Card?

Oliver Nash (Jul 30 2023 at 20:50):

~~The conclusion could be the stronger Unique X, right?~~ On second thought, I'm not sure I prefer this.

Kyle Miller (Jul 30 2023 at 20:54):

docs#Fintype.card_le_one_iff_subsingleton is pretty much that

Kyle Miller (Jul 30 2023 at 20:55):

Untested: Fintype.card_le_one_iff_subsingleton.mp h.le

Kevin Buzzard (Jul 30 2023 at 21:03):

Yeah that'll do fine. Thanks!

Kevin Buzzard (Jul 30 2023 at 21:04):

The thing about docs#Unique is that it's data so I usually try to avoid it.

Kevin Buzzard (Jul 30 2023 at 21:06):

turns out it's h.ge BTW :-) Thanks both!

Yury G. Kudryashov (Jul 31 2023 at 17:53):

Why is it h.ge?

Ruben Van de Velde (Jul 31 2023 at 18:20):

Yury G. Kudryashov said:

Why is it h.ge?

Because it's h.symm.le = h.ge rather than h.le

Yury G. Kudryashov (Jul 31 2023 at 18:23):

If h : card X = 1, then h.le is card X ≤ 1, see docs#Eq.le

Yury G. Kudryashov (Jul 31 2023 at 18:24):

And that's exactly what we need. Possibly, @Kevin Buzzard had h : 1 = card X, not h : card X = 1.

Kevin Buzzard (Jul 31 2023 at 21:39):

Yes you're absolutely right, sorry for the noise! I actually have 1 = card X in my application.

Last updated: Dec 20 2023 at 11:08 UTC