le_supr

Stream: general

[Adam Topaz]

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]

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]

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

[Rémy Degenne]

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

[Adam Topaz]

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

[Rémy Degenne]

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]

well your solution looks simple :)

[Adam Topaz]

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

[Eric Wieser]

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]

Which is why le_supr doesn't match

[Kevin Buzzard]

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]

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

[Adam Topaz]

b = binders or something?

[Rémy Degenne]

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]

but Sup is also for many...

[Rémy Degenne]

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]

Or yeah, rmust be for range

[Adam Topaz]

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

[Eric Wieser]

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

[Rémy Degenne]

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]

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

[Mario Carneiro]

ah, eric said this

[Kevin Buzzard]

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/