find supr

Stream: general

[Johan Commelin]

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]

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

[Johan Commelin]

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.