Zulip Chat Archive

Stream: Is there code for X?

Topic: cardinal.pos_of_one_le


view this post on Zulip Adam Topaz (Jan 22 2021 at 16:32):

I'm having a hard time finding something that proves the following simple thing:

import set_theory.cardinal

example (x : cardinal) (h : 1  x) : 0 < x := sorry

view this post on Zulip Eric Wieser (Jan 22 2021 at 16:33):

What import do I need for docs#cardinal?

view this post on Zulip Eric Wieser (Jan 22 2021 at 16:33):

Ah, set_theory.cardinal

view this post on Zulip Adam Topaz (Jan 22 2021 at 16:35):

Oh yeah, sorry :)

view this post on Zulip Eric Wieser (Jan 22 2021 at 16:39):

cardinal.zero_lt_one.trans_le h

view this post on Zulip Adam Topaz (Jan 22 2021 at 16:41):

Oh sorry, I had the wrong way around :) I really need

import set_theory.cardinal

example (x : cardinal) (h : 0 < x) : 1  x := sorry

view this post on Zulip Adam Topaz (Jan 22 2021 at 16:41):

Which seems a bit harder since you need to know there is nothing between 00 and 11.

view this post on Zulip Eric Wieser (Jan 22 2021 at 16:48):

docs#cardinal.one_le_iff_pos

view this post on Zulip Eric Wieser (Jan 22 2021 at 16:48):

Or by library_search ;)

view this post on Zulip Adam Topaz (Jan 22 2021 at 16:49):

Library search didn't find it for me... strange :)


Last updated: May 17 2021 at 15:13 UTC