Zulip Chat Archive

Stream: maths

Topic: multilple "and elimination"

Filippo A. E. Nuccio (Oct 17 2020 at 16:19):

I have a hypothesis h : p_1 and p_2 and p_3 and p_4 and I would like to use p_4. Is there a nicer way than writing .right four times?

Heather Macbeth (Oct 17 2020 at 16:20):

You can write .2 four (three?) times, not sure if it's nicer!

Filippo A. E. Nuccio (Oct 17 2020 at 16:21):

Heather Macbeth said:

You can write .2 four (three?) times, not sure if it's nicer!

Well, it uses less ink...

Heather Macbeth (Oct 17 2020 at 16:23):

Or, will want to use the other pieces later as well? Then you can split h up using something like 

obtain ⟨p1, p2, p3, p4⟩ := h,

Filippo A. E. Nuccio (Oct 17 2020 at 16:24):

Well no, actually p1 to p3 are useless for me; but if I understand your hint, this would pout p1 to p4 in the list of hypothesis?

Floris van Doorn (Oct 17 2020 at 17:13):

I believe obtain ⟨-, -, -, p4⟩ := h, also works, and throws away all hypotheses other than p4.

Filippo A. E. Nuccio (Oct 17 2020 at 17:14):

Thanks! Let me check

Floris van Doorn (Oct 17 2020 at 17:14):

Or you can do have p4 := h.2.2.2 (this will not remove h from the list of hypotheses)

Filippo A. E. Nuccio (Oct 17 2020 at 17:15):

Oh yes, the first works - thanks!

Last updated: Dec 20 2023 at 11:08 UTC