Zulip Chat Archive

Stream: new members

Topic: reverse orders in finset filter


Emma R. Hasson (Jul 19 2022 at 19:45):

Can anyone help with this? We seem to need to break it into sums and then use sum_comm, but feel there should be a more direct route.

example (P :     Prop) (s t : finset ) :
 (a:×) in finset.filter (λ (x : ×), P x.1  x.2) (s.product t), 1  =
 (a:×) in finset.filter (λ (x : ×), P x.2  x.1) (t.product s), 1 :=
begin
 sorry,
end

Kenny Lau (Jul 19 2022 at 19:45):

you could observe that this equality is induced by a bijection of the domain

Yakov Pechersky (Jul 19 2022 at 20:18):

import algebra.big_operators.basic

open_locale big_operators
open finset


example (P :     Prop) [ x y, decidable (P x y)] (s t : finset ) :
   (a:×) in filter (λ (x : ×), P x.1  x.2) (s.product t), 1  =
   (a:×) in filter (λ (x : ×), P x.2  x.1) (t.product s), 1 :=
begin
  refine sum_bij (λ a _, a.swap) _ (λ _ _, rfl) (λ _ _ _ _, prod.swap_inj.mp) _,
  { rintro ⟨⟩,
    simp {contextual := tt} },
  { rintro x, y h,
    refine ⟨(y, x), _, rfl⟩,
    simpa [and.comm] using h }
end

Eric Wieser (Jul 19 2022 at 22:46):

Sounds like we're missing the lemma that says (s.product t).map equiv.prod_comm.to_embedding = t.product s

Yaël Dillies (Jul 19 2022 at 23:13):

docs#set.image_swap_prod for the set version.


Last updated: Dec 20 2023 at 11:08 UTC