## Stream: general

### Topic: le_supr

#### 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


#### 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


#### Adam Topaz (Feb 16 2021 at 20:16):

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

#### 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

#### Adam Topaz (Feb 16 2021 at 20:18):

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


#### 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.

#### Rémy Degenne (Feb 16 2021 at 20:20):

well your solution looks simple :)

#### Adam Topaz (Feb 16 2021 at 20:20):

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

#### 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

#### Eric Wieser (Feb 16 2021 at 20:43):

Which is why le_supr doesn't match

#### 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.

#### 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?

#### Adam Topaz (Feb 16 2021 at 21:20):

b = binders or something?

#### 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

#### Adam Topaz (Feb 16 2021 at 21:22):

but Sup is also for many...

#### 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)

#### Adam Topaz (Feb 16 2021 at 21:25):

Or yeah, rmust be for range

#### Adam Topaz (Feb 16 2021 at 21:25):

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

#### Eric Wieser (Feb 16 2021 at 21:26):

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

#### 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

#### Mario Carneiro (Feb 16 2021 at 21:28):

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

#### Mario Carneiro (Feb 16 2021 at 21:29):

ah, eric said this

#### 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