Zulip Chat Archive

Stream: new members

Topic: forall commutes with or


Raphael Appenzeller (Jul 29 2022 at 14:47):

I would like to use the following statement in a proof. I would have expected this to be in the library somewhere but library_search was not successful. Is there a different version that I could use, or should this be added to the library?

lemma logic_helper (α β : Type*) (A : α  Prop ) (B : β  Prop): ( u : α ,  v : β , A u  B v )
                                                           ( u : α, A u)  ( v : β , B v ) :=
begin
  sorry,
end

Ruben Van de Velde (Jul 29 2022 at 14:53):

lemma logic_helper (α β : Type*) (A : α  Prop ) (B : β  Prop): ( u : α ,  v : β , A u  B v )
                                                           ( u : α, A u)  ( v : β , B v ) :=
begin
  simp_rw [forall_or_distrib_right, forall_or_distrib_left],
end

Last updated: Dec 20 2023 at 11:08 UTC