Zulip Chat Archive

Stream: general

Topic: find supr


view this post on Zulip 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...)

view this post on Zulip Johan Commelin (Nov 09 2018 at 13:45):

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

view this post on Zulip 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