Zulip Chat Archive

Stream: new members

Topic: nonempty and set.nonempty


view this post on Zulip Heather Macbeth (Dec 14 2020 at 21:11):

Am I supposed to be able to get set.nonempty from a set whose subtype is nonempty, without using classical (for classical.inhabited_of_nonempty or similar)? Please tell me how, if so!

import data.set.basic

example {α : Type*} {s : set α} (hs : s.nonempty) : nonempty s := set.nonempty.to_subtype hs

example {α : Type*} (s : set α) [inhabited s] : s.nonempty := ⟨(default s).1, (default s).2

-- is this true?
example {α : Type*} (s : set α) [nonempty s] : s.nonempty := sorry

view this post on Zulip Adam Topaz (Dec 14 2020 at 21:14):

Here's a bad and non-golfed proof:

import data.set.basic

example {α : Type*} {s : set α} (hs : s.nonempty) : nonempty s := set.nonempty.to_subtype hs

example {α : Type*} (s : set α) [inhabited s] : s.nonempty := ⟨(default s).1, (default s).2

-- is this true?
example {α : Type*} (s : set α) (I : nonempty s) : s.nonempty :=
begin
  tactic.unfreeze_local_instances,
  induction I,
  use I,
  exact I.2
end

view this post on Zulip Adam Topaz (Dec 14 2020 at 21:15):

So at least it's true :)

view this post on Zulip Yakov Pechersky (Dec 14 2020 at 21:17):

example {α : Type*} (s : set α) [nonempty s] : s.nonempty :=
begin
  rw set.nonempty_def,
  rw nonempty_subtype,
  assumption
end

view this post on Zulip Adam Topaz (Dec 14 2020 at 21:17):

Much better!

view this post on Zulip Yakov Pechersky (Dec 14 2020 at 21:17):

Found by two suggests

view this post on Zulip Yakov Pechersky (Dec 14 2020 at 21:19):

Golfed:

example {α : Type*} (s : set α) [nonempty s] : s.nonempty :=
set.nonempty_def.mpr (nonempty_subtype.mp _›)

view this post on Zulip Heather Macbeth (Dec 14 2020 at 21:20):

Can you PR it? :). At least I assume it should be PR'd, it's so fundamental that perhaps it's been omitted for some good reason?

view this post on Zulip Heather Macbeth (Dec 14 2020 at 21:25):

Also, this seems to work:

example {α : Type*} (s : set α) [nonempty s] : s.nonempty := nonempty_subtype.mp _

view this post on Zulip Heather Macbeth (Dec 14 2020 at 21:28):

So maybe no need for a PR :)

view this post on Zulip Yakov Pechersky (Dec 14 2020 at 21:29):

#5373 too late =)


Last updated: May 18 2021 at 15:14 UTC