Stream: new members

Topic: nonempty and set.nonempty

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


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


Adam Topaz (Dec 14 2020 at 21:15):

So at least it's true :)

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


Much better!

Yakov Pechersky (Dec 14 2020 at 21:17):

Found by two suggests

Yakov Pechersky (Dec 14 2020 at 21:19):

Golfed:

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


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?

Heather Macbeth (Dec 14 2020 at 21:25):

Also, this seems to work:

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


Heather Macbeth (Dec 14 2020 at 21:28):

So maybe no need for a PR :)

Yakov Pechersky (Dec 14 2020 at 21:29):

#5373 too late =)

Last updated: May 18 2021 at 15:14 UTC