## Stream: new members

### Topic: Partition lemma without LEM

#### 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


#### Mario Carneiro (Jul 09 2020 at 02:03):

not with that statement

#### 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

#### 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


#### Brandon Brown (Jul 09 2020 at 02:35):

Thanks for the confirmation and reformulation!

Last updated: May 10 2021 at 00:31 UTC