Zulip Chat Archive

Stream: general

Topic: le_supr


view this post on Zulip Adam Topaz (Feb 16 2021 at 20:12):

Can someone come up with a simple proof of this using le_supr or something? Am I just being stupid?

import linear_algebra

variables {K V : Type*} [field K] [add_comm_group V] [vector_space K V]
variables (Hs : set (subspace K V))

example {H : subspace K V} (h : H  Hs) : H   (M  Hs), M :=
begin
  sorry,
end

view this post on Zulip Rémy Degenne (Feb 16 2021 at 20:15):

example {H : subspace K V} (h : H  Hs) : H   (M  Hs), M :=
begin
  refine le_trans _ (le_bsupr _ h),
  exact le_rfl,
end

view this post on Zulip Adam Topaz (Feb 16 2021 at 20:16):

Ah, it's le_bsupr that I needed! Thanks :)

view this post on Zulip Rémy Degenne (Feb 16 2021 at 20:16):

And I don't know how to write it on one line only. I always get errors with le_bsupr

view this post on Zulip Adam Topaz (Feb 16 2021 at 20:18):

example {H : subspace K V} (h : H  Hs) : H   (M  Hs), M := le_bsupr H h

view this post on Zulip Rémy Degenne (Feb 16 2021 at 20:19):

I basically always need to write le_trans _ (le_bsupr _ h) to get what I want when I think that le_bsupr would be enough. I don't get that lemma.

view this post on Zulip Rémy Degenne (Feb 16 2021 at 20:20):

well your solution looks simple :)

view this post on Zulip Adam Topaz (Feb 16 2021 at 20:20):

Yeah, I agree it's annoying, same goes for le_supr

view this post on Zulip Eric Wieser (Feb 16 2021 at 20:43):

Note that when you do \Sup (x \in s), you're actually taking the supremum over x of the supremum over proofs of x \in s

view this post on Zulip Eric Wieser (Feb 16 2021 at 20:43):

Which is why le_supr doesn't match

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 21:12):

The b lemmas are sometimes just the same as two applications of the un-b lemmas, one on a type and one on a proof.

view this post on Zulip Adam Topaz (Feb 16 2021 at 21:20):

what does b stand for? what does r stand for in supr? How am I supposed to remember these names?

view this post on Zulip Adam Topaz (Feb 16 2021 at 21:20):

b = binders or something?

view this post on Zulip Rémy Degenne (Feb 16 2021 at 21:21):

sup is for two things, supr is for many. I think that b is for bounded, but I don't understand the reason behind that name

view this post on Zulip Adam Topaz (Feb 16 2021 at 21:22):

but Sup is also for many...

view this post on Zulip Rémy Degenne (Feb 16 2021 at 21:24):

oh yes, indeed. supr is Sup of a Range ? I guess you can remember it that way, since supr s = Sup (set.range s)

view this post on Zulip Adam Topaz (Feb 16 2021 at 21:25):

Or yeah, rmust be for range

view this post on Zulip Adam Topaz (Feb 16 2021 at 21:25):

And b must be for baah! I forgot to add the b.

view this post on Zulip Eric Wieser (Feb 16 2021 at 21:26):

b is for "bounded" as in "one of the binders is x \in y"

view this post on Zulip Rémy Degenne (Feb 16 2021 at 21:26):

I am not sure r really is for range. It does not explain infi :) . I think it is just another variation on supremum, because several different ones were needed

view this post on Zulip Mario Carneiro (Feb 16 2021 at 21:28):

the b stands for "bounded", as in bounded quantification

view this post on Zulip Mario Carneiro (Feb 16 2021 at 21:29):

ah, eric said this

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 21:29):

I wrote something about Union, sUnion and bUnion for my course notes last week: https://xenaproject.wordpress.com/2021/02/10/formalising-mathematics-workshop-4/


Last updated: May 11 2021 at 12:15 UTC