fst and snd for zfc

Stream: new members

[Victor Porton]

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

[Patrick Johnson]

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]

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

[Mario Carneiro]

set_theory.zfc is part of lean 3 mathlib

[Patrick Johnson]

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]

Can elan install both Lean4 and Lean3?

[Mario Carneiro]

yes

[Victor Porton]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Patrick Johnson]

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