## Stream: general

### Topic: find supr

#### Johan Commelin (Nov 09 2018 at 12:33):

I have found

@[simp] lemma supr_pos {p : Prop} {f : p → α} (hp : p) : (⨆ h : p, f h) = f hp :=
le_antisymm (supr_le \$ assume h, le_refl _) (le_supr _ _)


in the library. I would like to have

lemma supr_xyzzy {p : Prop} {f : p → α} (hp : p) : (⨆ h : p, f h) ≤ f hp := sorry


I have never succesfully used find. Somehow it just doesn't give me any results. What should I type into VScode to find this lemma? (Assuming it is there...)

#### Johan Commelin (Nov 09 2018 at 13:45):

Ok, I've figured out that I should just use supr_le for this one.

#### Johan Commelin (Nov 09 2018 at 13:46):

Here is another one. Should there be a lemma called mem_of_mem_supr?
It would state that if x ∈ ⊔s ∈ S, s then there is an s ∈ S such that x ∈ s.

Last updated: May 14 2021 at 04:22 UTC