Zulip Chat Archive

Stream: new members

Topic: Partition lemma without LEM


view this post on Zulip Brandon Brown (Jul 09 2020 at 02:02):

Is it possible to prove this set partition lemma without using the law of excluded middle?

lemma partition_els_eq_if_share_el
{F : set (set X)}
{disjoint :  A B  F, A  B  A  B = }
{cover :  x : X,  A  F, x  A}
{nonempty :  A  F, A  }
{A B : set X}
{h0 : A  F} {h1 : B  F}
(h2 :  x : X, x  A  x  B) : A = B :=
begin
cases h2,
cases h2_h,
by_contra,
have z : A  B = ,
apply disjoint,
repeat {tauto},
have z2 : h2_w  A  B,
apply mem_inter,
repeat {tauto},
rw z at z2,
tauto,
end

view this post on Zulip Mario Carneiro (Jul 09 2020 at 02:03):

not with that statement

view this post on Zulip Mario Carneiro (Jul 09 2020 at 02:04):

if you rewrite disjoint to disjoint : ∀ A B ∈ F, A = B ∨ A ∩ B = ∅ then it can be done

view this post on Zulip Mario Carneiro (Jul 09 2020 at 02:09):

lemma partition_els_eq_if_share_el {X}
  {F : set (set X)}
  (disjoint :  A B  F, A = B  A  B = )
  {A B : set X}
  (h0 : A  F) (h1 : B  F)
  (h2 :  x : X, x  A  x  B) : A = B :=
(disjoint _ _ h0 h1).resolve_right $ λ h,
let x, hx := h2 in
show x  ( : set X), from h  hx

#print axioms partition_els_eq_if_share_el
-- no axioms

view this post on Zulip Brandon Brown (Jul 09 2020 at 02:35):

Thanks for the confirmation and reformulation!


Last updated: May 10 2021 at 00:31 UTC