Zulip Chat Archive

Stream: new members

Topic: fst and snd for zfc


Victor Porton (Apr 22 2022 at 02:44):

I need analogs of fst and snd for Set.pair of zfc module. Please help.

Patrick Johnson (Apr 22 2022 at 03:01):

Not sure what the recommended way is, but you can easily implement fst and snd using choice:

import set_theory.zfc

noncomputable theory
open_locale classical

def Set.fst (p : Set) : Set :=
if h :  (a b : Set), p = a.pair b then h.some else 

def Set.snd (p : Set) : Set :=
if h :  (a b : Set), p = a.pair b then h.some_spec.some else 

lemma Set.fst_eq {a b : Set} : (a.pair b).fst = a :=
begin
  rw Set.fst,
  split_ifs,
  { exact (Set.pair_inj h.some_spec.some_spec).1.symm },
  { cases h _, _, rfl },
end

lemma Set.snd_eq {a b : Set} : (a.pair b).snd = b :=
begin
  rw Set.snd,
  split_ifs,
  { exact (Set.pair_inj h.some_spec.some_spec).2.symm },
  { cases h _, _, rfl },
end

Victor Porton (Apr 22 2022 at 03:06):

@Patrick Johnson It is which version of Lean? My Lean 4 does not accept your code.

Mario Carneiro (Apr 22 2022 at 03:06):

set_theory.zfc is part of lean 3 mathlib

Patrick Johnson (Apr 22 2022 at 03:09):

Victor Porton said:

It is which version of Lean? My Lean 4 does not accept your code.

It's Lean 3. You should have mentioned in your question which version of Lean you are using. Note that there is also lean4 stream.

Victor Porton (Apr 22 2022 at 03:10):

Can elan install both Lean4 and Lean3?

Mario Carneiro (Apr 22 2022 at 03:14):

yes

Victor Porton (Apr 23 2022 at 10:25):

It does not compile with invalid field notation, 'some' is not a valid "field" because environment does not contain 'Exists.some'. It does not work even if I add import logic.basic. Why?

Victor Porton (Apr 23 2022 at 10:30):

@Patrick Johnson I indeed use Lean3, but it still does not compile (see above).

Eric Wieser (Apr 23 2022 at 15:28):

docs#Exists.some suggests that import logic.basic is enough in lean 3

Eric Wieser (Apr 23 2022 at 15:32):

docs4#Exists.some tells you it does not exist in lean 4

Patrick Johnson (Apr 23 2022 at 15:57):

It works in the online editor. The error is probably related to your Lean 3 installation. Note that logic.basic is indirectly imported by set_theory.zfc


Last updated: Dec 20 2023 at 11:08 UTC