Commit 2023-12-29 06:46 8f17470f

View on Github →

refactor(*): change definition of Set.image2 etc (#9275)

  • Redefine Set.image2 to use ∃ a ∈ s, ∃ b ∈ t, f a b = c instead of ∃ a b, a ∈ s ∧ b ∈ t ∧ f a b = c.
  • Redefine Set.seq as Set.image2. The new definition is equal to the old one but rw [Set.seq] gives a different result.
  • Redefine Filter.map₂ to use ∃ u ∈ f, ∃ v ∈ g, image2 m u v ⊆ s instead of ∃ u v, u ∈ f ∧ v ∈ g ∧ ...
  • Update lemmas like Set.mem_image2, Finset.mem_image₂, Set.mem_mul, Finset.mem_div etc The two reasons to make the change are:
  • ∃ a ∈ s, ∃ b ∈ t, _ is a simp-normal form, and
  • it looks a bit nicer.

Estimated changes

modified theorem Language.mem_mul
modified theorem Finset.mem_image₂
modified theorem Finset.mem_div
modified theorem Finset.mem_mul
modified theorem Finset.mem_smul
modified theorem Finset.mem_vsub
modified def Set.seq
modified theorem Set.seq_eq_image2
modified theorem Set.seq_singleton
modified theorem Set.singleton_seq
modified theorem Set.image2_mk_eq_prod
modified theorem Set.mem_image2
modified theorem Set.mem_div
modified theorem Set.mem_mul
modified theorem Set.mem_smul
modified theorem Set.mem_vsub
added theorem Doset.doset_eq_image2
modified theorem Doset.mem_doset
modified theorem SubMulAction.mem_mul
modified theorem Filter.mem_map₂_iff
modified theorem Filter.mem_div
modified theorem Filter.mem_mul
modified theorem Filter.mem_smul
modified theorem Filter.mem_vsub