From f1944b30c97c5eb626e498307dec8b022a05bd0a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Fri, 12 Aug 2022 09:58:10 +0000 Subject: [PATCH] =?UTF-8?q?refactor(*):=20Extend=20`=C3=97=CB=A2`=20notati?= =?UTF-8?q?on=20(#15717)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Delete `has_set_prod` in favor of a direct notation declaration. Overload that notation with the `list`, `finset`, `multiset` versions. Use the new notation and remove type ascriptions to the existing uses where possible (because Lean gets more information from the notation now). --- .../73_ascending_descending_sequences.lean | 2 +- .../81_sum_of_prime_reciprocals_diverges.lean | 2 +- src/algebra/algebra/subalgebra/basic.lean | 5 +- src/algebra/big_operators/basic.lean | 12 +-- src/algebra/big_operators/ring.lean | 2 +- src/algebra/direct_sum/internal.lean | 3 +- src/algebra/direct_sum/ring.lean | 2 +- src/algebra/indicator_function.lean | 8 +- src/algebra/monoid_algebra/basic.lean | 4 +- src/algebraic_geometry/structure_sheaf.lean | 2 +- src/analysis/calculus/cont_diff.lean | 7 +- src/analysis/convex/combination.lean | 4 +- src/analysis/normed/field/basic.lean | 2 +- src/combinatorics/additive/salem_spencer.lean | 2 +- src/combinatorics/simple_graph/density.lean | 13 ++-- src/computability/turing_machine.lean | 3 +- src/data/fin_enum.lean | 2 +- src/data/finset/functor.lean | 2 +- src/data/finset/lattice.lean | 8 +- src/data/finset/n_ary.lean | 5 +- src/data/finset/pointwise.lean | 16 ++-- src/data/finset/prod.lean | 73 ++++++++++--------- src/data/finset/sym.lean | 2 +- src/data/fintype/basic.lean | 4 +- src/data/list/defs.lean | 3 + src/data/multiset/bind.lean | 17 +++-- src/data/set/finite.lean | 2 +- src/data/set/pairwise.lean | 4 +- src/data/set/pointwise.lean | 2 +- src/data/set/prod.lean | 28 +++---- src/data/sym/sym2.lean | 4 +- src/geometry/manifold/cont_mdiff.lean | 14 ++-- src/geometry/manifold/mfderiv.lean | 4 +- src/geometry/manifold/tangent_bundle.lean | 18 ++--- src/group_theory/schreier.lean | 2 +- src/group_theory/subgroup/basic.lean | 3 +- src/group_theory/submonoid/operations.lean | 6 +- src/group_theory/subsemigroup/operations.lean | 6 +- src/linear_algebra/span.lean | 5 +- src/logic/equiv/set.lean | 2 +- src/measure_theory/group/prod.lean | 2 +- .../integral/circle_integral_transform.lean | 12 ++- src/measure_theory/measurable_space.lean | 4 +- src/measure_theory/measure/lebesgue.lean | 3 +- src/model_theory/syntax.lean | 2 +- src/number_theory/class_number/finite.lean | 6 +- src/number_theory/divisors.lean | 2 +- .../gauss_eisenstein_lemmas.lean | 19 +++-- src/order/filter/prod.lean | 2 +- src/order/locally_finite.lean | 6 +- src/order/partition/finpartition.lean | 4 +- src/order/well_founded_set.lean | 2 +- src/ring_theory/algebra_tower.lean | 15 ++-- src/ring_theory/graded_algebra/radical.lean | 2 +- src/ring_theory/integral_closure.lean | 2 +- src/ring_theory/subring/basic.lean | 6 +- src/ring_theory/subsemiring/basic.lean | 5 +- src/ring_theory/witt_vector/defs.lean | 18 ++--- src/ring_theory/witt_vector/mul_coeff.lean | 11 ++- .../witt_vector/structure_polynomial.lean | 4 +- src/topology/algebra/module/basic.lean | 15 ++-- src/topology/algebra/monoid.lean | 12 +-- src/topology/algebra/open_subgroup.lean | 2 +- src/topology/algebra/order/floor.lean | 6 +- src/topology/constructions.lean | 6 +- src/topology/fiber_bundle.lean | 39 ++++------ src/topology/sets/compacts.lean | 11 ++- .../uniform_space/compact_separated.lean | 4 +- src/topology/vector_bundle/basic.lean | 8 +- src/topology/vector_bundle/hom.lean | 2 +- src/topology/vector_bundle/prod.lean | 4 +- src/topology/vector_bundle/pullback.lean | 2 +- 72 files changed, 247 insertions(+), 296 deletions(-) diff --git a/archive/100-theorems-list/73_ascending_descending_sequences.lean b/archive/100-theorems-list/73_ascending_descending_sequences.lean index d9665dc001feb..41e92aff0d128 100644 --- a/archive/100-theorems-list/73_ascending_descending_sequences.lean +++ b/archive/100-theorems-list/73_ascending_descending_sequences.lean @@ -132,7 +132,7 @@ begin by_contra q, push_neg at q, -- Then the labels `(a_i, b_i)` all fit in the following set: `{ (x,y) | 1 ≤ x ≤ r, 1 ≤ y ≤ s }` - let ran : finset (ℕ × ℕ) := ((range r).image nat.succ).product ((range s).image nat.succ), + let ran : finset (ℕ × ℕ) := (range r).image nat.succ ×ˢ (range s).image nat.succ, -- which we prove here. have : image ab univ ⊆ ran, -- First some logical shuffling diff --git a/archive/100-theorems-list/81_sum_of_prime_reciprocals_diverges.lean b/archive/100-theorems-list/81_sum_of_prime_reciprocals_diverges.lean index 58b8eefafd121..a07a1d585cafc 100644 --- a/archive/100-theorems-list/81_sum_of_prime_reciprocals_diverges.lean +++ b/archive/100-theorems-list/81_sum_of_prime_reciprocals_diverges.lean @@ -171,7 +171,7 @@ lemma card_le_two_pow_mul_sqrt {x k : ℕ} : card (M x k) ≤ 2 ^ k * nat.sqrt x begin let M₁ := {e ∈ M x k | squarefree (e + 1)}, let M₂ := M (nat.sqrt x) k, - let K := finset.product M₁ M₂, + let K := M₁ ×ˢ M₂, let f : ℕ × ℕ → ℕ := λ mn, (mn.2 + 1) ^ 2 * (mn.1 + 1) - 1, -- Every element of `M x k` is one less than the product `(m + 1)² * (r + 1)` with `r + 1` diff --git a/src/algebra/algebra/subalgebra/basic.lean b/src/algebra/algebra/subalgebra/basic.lean index 7b5b072c843f6..7d8d4bb89d90a 100644 --- a/src/algebra/algebra/subalgebra/basic.lean +++ b/src/algebra/algebra/subalgebra/basic.lean @@ -810,12 +810,11 @@ variables (S₁ : subalgebra R B) /-- The product of two subalgebras is a subalgebra. -/ def prod : subalgebra R (A × B) := -{ carrier := (S : set A) ×ˢ (S₁ : set B), +{ carrier := S ×ˢ S₁, algebra_map_mem' := λ r, ⟨algebra_map_mem _ _, algebra_map_mem _ _⟩, .. S.to_subsemiring.prod S₁.to_subsemiring } -@[simp] lemma coe_prod : - (prod S S₁ : set (A × B)) = (S : set A) ×ˢ (S₁ : set B):= rfl +@[simp] lemma coe_prod : (prod S S₁ : set (A × B)) = S ×ˢ S₁ := rfl lemma prod_to_submodule : (S.prod S₁).to_submodule = S.to_submodule.prod S₁.to_submodule := rfl diff --git a/src/algebra/big_operators/basic.lean b/src/algebra/big_operators/basic.lean index a9565c6973c3b..84b21f722d20d 100644 --- a/src/algebra/big_operators/basic.lean +++ b/src/algebra/big_operators/basic.lean @@ -512,24 +512,24 @@ eq.trans (by rw one_mul; refl) fold_op_distrib @[to_additive] lemma prod_product {s : finset γ} {t : finset α} {f : γ×α → β} : - (∏ x in s.product t, f x) = ∏ x in s, ∏ y in t, f (x, y) := -prod_finset_product (s.product t) s (λ a, t) (λ p, mem_product) + (∏ x in s ×ˢ t, f x) = ∏ x in s, ∏ y in t, f (x, y) := +prod_finset_product (s ×ˢ t) s (λ a, t) (λ p, mem_product) /-- An uncurried version of `finset.prod_product`. -/ @[to_additive "An uncurried version of `finset.sum_product`"] lemma prod_product' {s : finset γ} {t : finset α} {f : γ → α → β} : - (∏ x in s.product t, f x.1 x.2) = ∏ x in s, ∏ y in t, f x y := + (∏ x in s ×ˢ t, f x.1 x.2) = ∏ x in s, ∏ y in t, f x y := prod_product @[to_additive] lemma prod_product_right {s : finset γ} {t : finset α} {f : γ×α → β} : - (∏ x in s.product t, f x) = ∏ y in t, ∏ x in s, f (x, y) := -prod_finset_product_right (s.product t) t (λ a, s) (λ p, mem_product.trans and.comm) + (∏ x in s ×ˢ t, f x) = ∏ y in t, ∏ x in s, f (x, y) := +prod_finset_product_right (s ×ˢ t) t (λ a, s) (λ p, mem_product.trans and.comm) /-- An uncurried version of `finset.prod_product_right`. -/ @[to_additive "An uncurried version of `finset.prod_product_right`"] lemma prod_product_right' {s : finset γ} {t : finset α} {f : γ → α → β} : - (∏ x in s.product t, f x.1 x.2) = ∏ y in t, ∏ x in s, f x y := + (∏ x in s ×ˢ t, f x.1 x.2) = ∏ y in t, ∏ x in s, f x y := prod_product_right /-- Generalization of `finset.prod_comm` to the case when the inner `finset`s depend on the outer diff --git a/src/algebra/big_operators/ring.lean b/src/algebra/big_operators/ring.lean index fb1e6504e6a79..7d5e7727e114e 100644 --- a/src/algebra/big_operators/ring.lean +++ b/src/algebra/big_operators/ring.lean @@ -52,7 +52,7 @@ add_monoid_hom.map_sum (add_monoid_hom.mul_left b) _ s lemma sum_mul_sum {ι₁ : Type*} {ι₂ : Type*} (s₁ : finset ι₁) (s₂ : finset ι₂) (f₁ : ι₁ → β) (f₂ : ι₂ → β) : - (∑ x₁ in s₁, f₁ x₁) * (∑ x₂ in s₂, f₂ x₂) = ∑ p in s₁.product s₂, f₁ p.1 * f₂ p.2 := + (∑ x₁ in s₁, f₁ x₁) * (∑ x₂ in s₂, f₂ x₂) = ∑ p in s₁ ×ˢ s₂, f₁ p.1 * f₂ p.2 := by { rw [sum_product, sum_mul, sum_congr rfl], intros, rw mul_sum } end semiring diff --git a/src/algebra/direct_sum/internal.lean b/src/algebra/direct_sum/internal.lean index 5aa5c56af42ef..87dbb2e9fb016 100644 --- a/src/algebra/direct_sum/internal.lean +++ b/src/algebra/direct_sum/internal.lean @@ -152,8 +152,7 @@ lemma direct_sum.coe_mul_apply [add_monoid ι] [semiring R] [set_like σ R] [add_submonoid_class σ R] (A : ι → σ) [set_like.graded_monoid A] [Π (i : ι) (x : A i), decidable (x ≠ 0)] (r r' : ⨁ i, A i) (i : ι) : ((r * r') i : R) = - ∑ ij in finset.filter (λ ij : ι × ι, ij.1 + ij.2 = i) (r.support.product r'.support), - r ij.1 * r' ij.2 := + ∑ ij in (r.support ×ˢ r'.support).filter (λ ij : ι × ι, ij.1 + ij.2 = i), r ij.1 * r' ij.2 := begin rw [direct_sum.mul_eq_sum_support_ghas_mul, dfinsupp.finset_sum_apply, add_submonoid_class.coe_finset_sum], diff --git a/src/algebra/direct_sum/ring.lean b/src/algebra/direct_sum/ring.lean index aae4829ac4f87..99e73c97e609f 100644 --- a/src/algebra/direct_sum/ring.lean +++ b/src/algebra/direct_sum/ring.lean @@ -269,7 +269,7 @@ open_locale big_operators lemma mul_eq_sum_support_ghas_mul [Π (i : ι) (x : A i), decidable (x ≠ 0)] (a a' : ⨁ i, A i) : a * a' = - ∑ (ij : ι × ι) in (dfinsupp.support a).product (dfinsupp.support a'), + ∑ ij in dfinsupp.support a ×ˢ dfinsupp.support a', direct_sum.of _ _ (graded_monoid.ghas_mul.mul (a ij.fst) (a' ij.snd)) := begin change direct_sum.mul_hom _ a a' = _, diff --git a/src/algebra/indicator_function.lean b/src/algebra/indicator_function.lean index 8d697ad85304f..08f80f48aabd8 100644 --- a/src/algebra/indicator_function.lean +++ b/src/algebra/indicator_function.lean @@ -457,12 +457,8 @@ lemma inter_indicator_one {s t : set α} : funext (λ _, by simpa only [← inter_indicator_mul, pi.mul_apply, pi.one_apply, one_mul]) lemma indicator_prod_one {s : set α} {t : set β} {x : α} {y : β} : - (s ×ˢ t : set _).indicator (1 : _ → M) (x, y) = s.indicator 1 x * t.indicator 1 y := -begin - letI := classical.dec_pred (∈ s), - letI := classical.dec_pred (∈ t), - simp [indicator_apply, ← ite_and], -end + (s ×ˢ t).indicator (1 : _ → M) (x, y) = s.indicator 1 x * t.indicator 1 y := +by { classical, simp [indicator_apply, ←ite_and] } variables (M) [nontrivial M] diff --git a/src/algebra/monoid_algebra/basic.lean b/src/algebra/monoid_algebra/basic.lean index 09d7c6b790759..be59f29d52cd2 100644 --- a/src/algebra/monoid_algebra/basic.lean +++ b/src/algebra/monoid_algebra/basic.lean @@ -325,8 +325,8 @@ lemma mul_apply_antidiagonal [has_mul G] (f g : monoid_algebra k G) (x : G) (s : let F : G × G → k := λ p, by classical; exact if p.1 * p.2 = x then f p.1 * g p.2 else 0 in calc (f * g) x = (∑ a₁ in f.support, ∑ a₂ in g.support, F (a₁, a₂)) : mul_apply f g x -... = ∑ p in f.support.product g.support, F p : finset.sum_product.symm -... = ∑ p in (f.support.product g.support).filter (λ p : G × G, p.1 * p.2 = x), f p.1 * g p.2 : +... = ∑ p in f.support ×ˢ g.support, F p : finset.sum_product.symm +... = ∑ p in (f.support ×ˢ g.support).filter (λ p : G × G, p.1 * p.2 = x), f p.1 * g p.2 : (finset.sum_filter _ _).symm ... = ∑ p in s.filter (λ p : G × G, p.1 ∈ f.support ∧ p.2 ∈ g.support), f p.1 * g p.2 : sum_congr (by { ext, simp only [mem_filter, mem_product, hs, and_comm] }) (λ _ _, rfl) diff --git a/src/algebraic_geometry/structure_sheaf.lean b/src/algebraic_geometry/structure_sheaf.lean index dd27bc65946b5..edae040d08332 100644 --- a/src/algebraic_geometry/structure_sheaf.lean +++ b/src/algebraic_geometry/structure_sheaf.lean @@ -688,7 +688,7 @@ begin have n_spec := λ (p : ι × ι), (exists_power p.fst p.snd).some_spec, -- We need one power `(h i * h j) ^ N` that works for *all* pairs `(i,j)` -- Since there are only finitely many indices involved, we can pick the supremum. - let N := (t.product t).sup n, + let N := (t ×ˢ t).sup n, have basic_opens_eq : ∀ i : ι, basic_open ((h i) ^ (N+1)) = basic_open (h i) := λ i, basic_open_pow _ _ (by linarith), -- Expanding the fraction `a i / h i` by the power `(h i) ^ N` gives the desired normalization diff --git a/src/analysis/calculus/cont_diff.lean b/src/analysis/calculus/cont_diff.lean index 8c244b8a7ada9..9a83247cbaeb8 100644 --- a/src/analysis/calculus/cont_diff.lean +++ b/src/analysis/calculus/cont_diff.lean @@ -1160,10 +1160,10 @@ hf.fderiv_within' (by { rw [insert_eq_of_mem hxs], exact eventually_of_mem self_ continuous. -/ lemma cont_diff_on.continuous_on_fderiv_within_apply (h : cont_diff_on 𝕜 n f s) (hs : unique_diff_on 𝕜 s) (hn : 1 ≤ n) : - continuous_on (λp : E × E, (fderiv_within 𝕜 f s p.1 : E → F) p.2) (s ×ˢ (univ : set E)) := + continuous_on (λp : E × E, (fderiv_within 𝕜 f s p.1 : E → F) p.2) (s ×ˢ univ) := begin have A : continuous (λq : (E →L[𝕜] F) × E, q.1 q.2) := is_bounded_bilinear_map_apply.continuous, - have B : continuous_on (λp : E × E, (fderiv_within 𝕜 f s p.1, p.2)) (s ×ˢ (univ : set E)), + have B : continuous_on (λp : E × E, (fderiv_within 𝕜 f s p.1, p.2)) (s ×ˢ univ), { apply continuous_on.prod _ continuous_snd.continuous_on, exact continuous_on.comp (h.continuous_on_fderiv_within hs hn) continuous_fst.continuous_on (prod_subset_preimage_fst _ _) }, @@ -2263,8 +2263,7 @@ lemma cont_diff_prod_assoc_symm : cont_diff 𝕜 ⊤ $ (equiv.prod_assoc E F G). /-- The bundled derivative of a `C^{n+1}` function is `C^n`. -/ lemma cont_diff_on_fderiv_within_apply {m n : with_top ℕ} {s : set E} {f : E → F} (hf : cont_diff_on 𝕜 n f s) (hs : unique_diff_on 𝕜 s) (hmn : m + 1 ≤ n) : - cont_diff_on 𝕜 m (λp : E × E, (fderiv_within 𝕜 f s p.1 : E →L[𝕜] F) p.2) - (s ×ˢ (univ : set E)) := + cont_diff_on 𝕜 m (λp : E × E, (fderiv_within 𝕜 f s p.1 : E →L[𝕜] F) p.2) (s ×ˢ univ) := begin have A : cont_diff 𝕜 m (λp : (E →L[𝕜] F) × E, p.1 p.2), { apply is_bounded_bilinear_map.cont_diff, diff --git a/src/analysis/convex/combination.lean b/src/analysis/convex/combination.lean index 6787f8a41fd3e..9955898d66203 100644 --- a/src/analysis/convex/combination.lean +++ b/src/analysis/convex/combination.lean @@ -352,7 +352,7 @@ begin rw convex_hull_eq at ⊢ hx hy, obtain ⟨ι, a, w, S, hw, hw', hS, hSp⟩ := hx, obtain ⟨κ, b, v, T, hv, hv', hT, hTp⟩ := hy, - have h_sum : ∑ (i : ι × κ) in a.product b, w i.fst * v i.snd = 1, + have h_sum : ∑ (i : ι × κ) in a ×ˢ b, w i.fst * v i.snd = 1, { rw [finset.sum_product, ← hw'], congr, ext i, @@ -360,7 +360,7 @@ begin { congr, ext, simp [mul_comm] }, rw [this, ← finset.sum_mul, hv'], simp }, - refine ⟨ι × κ, a.product b, λ p, (w p.1) * (v p.2), λ p, (S p.1, T p.2), + refine ⟨ι × κ, a ×ˢ b, λ p, (w p.1) * (v p.2), λ p, (S p.1, T p.2), λ p hp, _, h_sum, λ p hp, _, _⟩, { rw mem_product at hp, exact mul_nonneg (hw p.1 hp.1) (hv p.2 hp.2) }, diff --git a/src/analysis/normed/field/basic.lean b/src/analysis/normed/field/basic.lean index d556704e575e6..9df7c465f7af8 100644 --- a/src/analysis/normed/field/basic.lean +++ b/src/analysis/normed/field/basic.lean @@ -784,7 +784,7 @@ suffices this : ∀ u : finset (ι × ι'), ∑ x in u, f x.1 * g x.2 ≤ s*t, from summable_of_sum_le (λ x, mul_nonneg (hf' _) (hg' _)) this, assume u, calc ∑ x in u, f x.1 * g x.2 - ≤ ∑ x in (u.image prod.fst).product (u.image prod.snd), f x.1 * g x.2 : + ≤ ∑ x in u.image prod.fst ×ˢ u.image prod.snd, f x.1 * g x.2 : sum_mono_set_of_nonneg (λ x, mul_nonneg (hf' _) (hg' _)) subset_product ... = ∑ x in u.image prod.fst, ∑ y in u.image prod.snd, f x * g y : sum_product ... = ∑ x in u.image prod.fst, f x * ∑ y in u.image prod.snd, g y : diff --git a/src/combinatorics/additive/salem_spencer.lean b/src/combinatorics/additive/salem_spencer.lean index fd646013d86b3..9050f8ee6a0aa 100644 --- a/src/combinatorics/additive/salem_spencer.lean +++ b/src/combinatorics/additive/salem_spencer.lean @@ -345,7 +345,7 @@ calc @[to_additive] lemma le_mul_roth_number_product (s : finset α) (t : finset β) : - mul_roth_number s * mul_roth_number t ≤ mul_roth_number (s.product t) := + mul_roth_number s * mul_roth_number t ≤ mul_roth_number (s ×ˢ t) := begin obtain ⟨u, hus, hucard, hu⟩ := mul_roth_number_spec s, obtain ⟨v, hvt, hvcard, hv⟩ := mul_roth_number_spec t, diff --git a/src/combinatorics/simple_graph/density.lean b/src/combinatorics/simple_graph/density.lean index 5931847b14f16..e46e30d36ad9e 100644 --- a/src/combinatorics/simple_graph/density.lean +++ b/src/combinatorics/simple_graph/density.lean @@ -33,8 +33,7 @@ variables (r : α → β → Prop) [Π a, decidable_pred (r a)] {s s₁ s₂ : f {a : α} {b : β} {δ : ℚ} /-- Finset of edges of a relation between two finsets of vertices. -/ -def interedges (s : finset α) (t : finset β) : finset (α × β) := -(s.product t).filter $ λ e, r e.1 e.2 +def interedges (s : finset α) (t : finset β) : finset (α × β) := (s ×ˢ t).filter $ λ e, r e.1 e.2 /-- Edge density of a relation between two finsets of vertices. -/ def edge_density (s : finset α) (t : finset β) : ℚ := (interedges r s t).card / (s.card * t.card) @@ -93,7 +92,7 @@ ext $ λ a, by simp only [mem_interedges_iff, mem_bUnion, ←exists_and_distrib_ lemma interedges_bUnion (s : finset ι) (t : finset κ) (f : ι → finset α) (g : κ → finset β) : interedges r (s.bUnion f) (t.bUnion g) = - (s.product t).bUnion (λ ab, interedges r (f ab.1) (g ab.2)) := + (s ×ˢ t).bUnion (λ ab, interedges r (f ab.1) (g ab.2)) := by simp_rw [product_bUnion, interedges_bUnion_left, interedges_bUnion_right] end decidable_eq @@ -143,7 +142,7 @@ end lemma card_interedges_finpartition [decidable_eq α] [decidable_eq β] (P : finpartition s) (Q : finpartition t) : - (interedges r s t).card = ∑ ab in P.parts.product Q.parts, (interedges r ab.1 ab.2).card := + (interedges r s t).card = ∑ ab in P.parts ×ˢ Q.parts, (interedges r ab.1 ab.2).card := by simp_rw [card_interedges_finpartition_left _ P, card_interedges_finpartition_right _ _ Q, sum_product] @@ -262,7 +261,7 @@ def interedges (s t : finset α) : finset (α × α) := interedges G.adj s t def edge_density : finset α → finset α → ℚ := edge_density G.adj lemma interedges_def (s t : finset α) : - G.interedges s t = (s.product t).filter (λ e, G.adj e.1 e.2) := rfl + G.interedges s t = (s ×ˢ t).filter (λ e, G.adj e.1 e.2) := rfl lemma edge_density_def (s t : finset α) : G.edge_density s t = (G.interedges s t).card / (s.card * t.card) := rfl @@ -302,14 +301,14 @@ interedges_bUnion_right _ _ _ _ lemma interedges_bUnion (s : finset ι) (t : finset κ) (f : ι → finset α) (g : κ → finset α) : G.interedges (s.bUnion f) (t.bUnion g) = - (s.product t).bUnion (λ ab, G.interedges (f ab.1) (g ab.2)) := + (s ×ˢ t).bUnion (λ ab, G.interedges (f ab.1) (g ab.2)) := interedges_bUnion _ _ _ _ _ lemma card_interedges_add_card_interedges_compl (h : disjoint s t) : (G.interedges s t).card + (Gᶜ.interedges s t).card = s.card * t.card := begin rw [←card_product, interedges_def, interedges_def], - have : (s.product t).filter (λ e , Gᶜ.adj e.1 e.2) = (s.product t).filter (λ e , ¬ G.adj e.1 e.2), + have : (s ×ˢ t).filter (λ e , Gᶜ.adj e.1 e.2) = (s ×ˢ t).filter (λ e , ¬ G.adj e.1 e.2), { refine filter_congr (λ x hx, _), rw mem_product at hx, rw [compl_adj, and_iff_right (h.forall_ne_finset hx.1 hx.2)] }, diff --git a/src/computability/turing_machine.lean b/src/computability/turing_machine.lean index fbdc015692744..87f740cd64b8a 100644 --- a/src/computability/turing_machine.lean +++ b/src/computability/turing_machine.lean @@ -1284,8 +1284,7 @@ end variables [fintype σ] /-- Given a finite set of accessible `Λ` machine states, there is a finite set of accessible machine states in the target (even though the type `Λ'` is infinite). -/ -noncomputable def tr_stmts (S : finset Λ) : finset Λ' := -(TM1.stmts M S).product finset.univ +noncomputable def tr_stmts (S : finset Λ) : finset Λ' := TM1.stmts M S ×ˢ finset.univ open_locale classical local attribute [simp] TM1.stmts₁_self diff --git a/src/data/fin_enum.lean b/src/data/fin_enum.lean index 338b1b1bb5db0..5bb070e8df17f 100644 --- a/src/data/fin_enum.lean +++ b/src/data/fin_enum.lean @@ -86,7 +86,7 @@ instance punit : fin_enum punit := of_list [punit.star] (λ x, by cases x; simp) instance prod {β} [fin_enum α] [fin_enum β] : fin_enum (α × β) := -of_list ( (to_list α).product (to_list β) ) (λ x, by cases x; simp) +of_list (to_list α ×ˢ to_list β) (λ x, by cases x; simp) instance sum {β} [fin_enum α] [fin_enum β] : fin_enum (α ⊕ β) := of_list ( (to_list α).map sum.inl ++ (to_list β).map sum.inr ) (λ x, by cases x; simp) diff --git a/src/data/finset/functor.lean b/src/data/finset/functor.lean index d3073272295de..5cdbde7163ccb 100644 --- a/src/data/finset/functor.lean +++ b/src/data/finset/functor.lean @@ -110,7 +110,7 @@ instance : is_comm_applicative finset := { commutative_prod := λ α β s t, begin simp_rw [seq_def, fmap_def, sup_image, sup_eq_bUnion], change s.bUnion (λ a, t.image $ λ b, (a, b)) = t.bUnion (λ b, s.image $ λ a, (a, b)), - transitivity s.product t; + transitivity s ×ˢ t; [rw product_eq_bUnion, rw product_eq_bUnion_right]; congr; ext; simp_rw mem_image, end, .. finset.is_lawful_applicative } diff --git a/src/data/finset/lattice.lean b/src/data/finset/lattice.lean index a5acdb750bd9e..ad60c8a44f2a0 100644 --- a/src/data/finset/lattice.lean +++ b/src/data/finset/lattice.lean @@ -116,7 +116,7 @@ end /-- See also `finset.product_bUnion`. -/ lemma sup_product_left (s : finset β) (t : finset γ) (f : β × γ → α) : - (s.product t).sup f = s.sup (λ i, t.sup $ λ i', f ⟨i, i'⟩) := + (s ×ˢ t).sup f = s.sup (λ i, t.sup $ λ i', f ⟨i, i'⟩) := begin refine le_antisymm _ (sup_le (λ i hi, sup_le $ λ i' hi', le_sup $ mem_product.2 ⟨hi, hi'⟩)), refine sup_le _, @@ -127,7 +127,7 @@ begin end lemma sup_product_right (s : finset β) (t : finset γ) (f : β × γ → α) : - (s.product t).sup f = t.sup (λ i', s.sup $ λ i, f ⟨i, i'⟩) := + (s ×ˢ t).sup f = t.sup (λ i', s.sup $ λ i, f ⟨i, i'⟩) := by rw [sup_product_left, sup_comm] @[simp] lemma sup_erase_bot [decidable_eq α] (s : finset α) : (s.erase ⊥).sup id = s.sup id := @@ -322,11 +322,11 @@ lemma inf_comm (s : finset β) (t : finset γ) (f : β → γ → α) : @sup_comm αᵒᵈ _ _ _ _ _ _ _ lemma inf_product_left (s : finset β) (t : finset γ) (f : β × γ → α) : - (s.product t).inf f = s.inf (λ i, t.inf $ λ i', f ⟨i, i'⟩) := + (s ×ˢ t).inf f = s.inf (λ i, t.inf $ λ i', f ⟨i, i'⟩) := @sup_product_left αᵒᵈ _ _ _ _ _ _ _ lemma inf_product_right (s : finset β) (t : finset γ) (f : β × γ → α) : - (s.product t).inf f = t.inf (λ i', s.inf $ λ i, f ⟨i, i'⟩) := + (s ×ˢ t).inf f = t.inf (λ i', s.inf $ λ i, f ⟨i, i'⟩) := @sup_product_right αᵒᵈ _ _ _ _ _ _ _ @[simp] lemma inf_erase_top [decidable_eq α] (s : finset α) : (s.erase ⊤).inf id = s.inf id := diff --git a/src/data/finset/n_ary.lean b/src/data/finset/n_ary.lean index 174012d5c2e35..b28c3a645e4be 100644 --- a/src/data/finset/n_ary.lean +++ b/src/data/finset/n_ary.lean @@ -33,7 +33,7 @@ variables {α α' β β' γ γ' δ δ' ε ε' : Type*} /-- The image of a binary function `f : α → β → γ` as a function `finset α → finset β → finset γ`. Mathematically this should be thought of as the image of the corresponding function `α × β → γ`. -/ def image₂ (f : α → β → γ) (s : finset α) (t : finset β) : finset γ := -(s.product t).image $ uncurry f +(s ×ˢ t).image $ uncurry f @[simp] lemma mem_image₂ : c ∈ image₂ f s t ↔ ∃ a b, a ∈ s ∧ b ∈ t ∧ f a b = c := by simp [image₂, and_assoc] @@ -47,8 +47,7 @@ lemma card_image₂_le (f : α → β → γ) (s : finset α) (t : finset β) : card_image_le.trans_eq $ card_product _ _ lemma card_image₂_iff : - (image₂ f s t).card = s.card * t.card ↔ - ((s : set α) ×ˢ (t : set β) : set (α × β)).inj_on (λ x, f x.1 x.2) := + (image₂ f s t).card = s.card * t.card ↔ (s ×ˢ t : set (α × β)).inj_on (λ x, f x.1 x.2) := by { rw [←card_product, ←coe_product], exact card_image_iff } lemma card_image₂ (hf : injective2 f) (s : finset α) (t : finset β) : diff --git a/src/data/finset/pointwise.lean b/src/data/finset/pointwise.lean index d91bac983863e..b0ff077697f8f 100644 --- a/src/data/finset/pointwise.lean +++ b/src/data/finset/pointwise.lean @@ -151,10 +151,10 @@ protected def has_mul : has_mul (finset α) := ⟨image₂ (*)⟩ localized "attribute [instance] finset.has_mul finset.has_add" in pointwise @[to_additive] -lemma mul_def : s * t = (s.product t).image (λ p : α × α, p.1 * p.2) := rfl +lemma mul_def : s * t = (s ×ˢ t).image (λ p : α × α, p.1 * p.2) := rfl @[to_additive] -lemma image_mul_product : (s.product t).image (λ x : α × α, x.fst * x.snd) = s * t := rfl +lemma image_mul_product : (s ×ˢ t).image (λ x : α × α, x.fst * x.snd) = s * t := rfl @[to_additive] lemma mem_mul {x : α} : x ∈ s * t ↔ ∃ y z, y ∈ s ∧ z ∈ t ∧ y * z = x := mem_image₂ @@ -167,7 +167,7 @@ lemma coe_mul (s t : finset α) : (↑(s * t) : set α) = ↑s * ↑t := coe_ima @[to_additive] lemma card_mul_iff : (s * t).card = s.card * t.card ↔ - ((s : set α) ×ˢ (t : set α) : set (α × α)).inj_on (λ p, p.1 * p.2) := card_image₂_iff + (s ×ˢ t : set (α × α)).inj_on (λ p, p.1 * p.2) := card_image₂_iff @[simp, to_additive] lemma empty_mul (s : finset α) : ∅ * s = ∅ := image₂_empty_left @[simp, to_additive] lemma mul_empty (s : finset α) : s * ∅ = ∅ := image₂_empty_right @@ -231,10 +231,10 @@ protected def has_div : has_div (finset α) := ⟨image₂ (/)⟩ localized "attribute [instance] finset.has_div finset.has_sub" in pointwise @[to_additive] -lemma div_def : s / t = (s.product t).image (λ p : α × α, p.1 / p.2) := rfl +lemma div_def : s / t = (s ×ˢ t).image (λ p : α × α, p.1 / p.2) := rfl @[to_additive add_image_prod] -lemma image_div_prod : (s.product t).image (λ x : α × α, x.fst / x.snd) = s / t := rfl +lemma image_div_prod : (s ×ˢ t).image (λ x : α × α, x.fst / x.snd) = s / t := rfl @[to_additive] lemma mem_div : a ∈ s / t ↔ ∃ b c, b ∈ s ∧ c ∈ t ∧ b / c = a := mem_image₂ @@ -630,10 +630,10 @@ protected def has_smul : has_smul (finset α) (finset β) := ⟨image₂ (•) localized "attribute [instance] finset.has_smul finset.has_vadd" in pointwise -@[to_additive] lemma smul_def : s • t = (s.product t).image (λ p : α × β, p.1 • p.2) := rfl +@[to_additive] lemma smul_def : s • t = (s ×ˢ t).image (λ p : α × β, p.1 • p.2) := rfl @[to_additive] -lemma image_smul_product : (s.product t).image (λ x : α × β, x.fst • x.snd) = s • t := rfl +lemma image_smul_product : (s ×ˢ t).image (λ x : α × β, x.fst • x.snd) = s • t := rfl @[to_additive] lemma mem_smul {x : β} : x ∈ s • t ↔ ∃ y z, y ∈ s ∧ z ∈ t ∧ y • z = x := mem_image₂ @@ -902,7 +902,7 @@ section left_cancel_semigroup variables [left_cancel_semigroup α] [decidable_eq α] (s t : finset α) (a : α) @[to_additive] lemma pairwise_disjoint_smul_iff {s : set α} {t : finset α} : - s.pairwise_disjoint (• t) ↔ ((s : set α) ×ˢ (t : set α) : set (α × α)).inj_on (λ p, p.1 * p.2) := + s.pairwise_disjoint (• t) ↔ (s ×ˢ t : set (α × α)).inj_on (λ p, p.1 * p.2) := by simp_rw [←pairwise_disjoint_coe, coe_smul_finset, set.pairwise_disjoint_smul_iff] @[simp, to_additive] lemma card_singleton_mul : ({a} * t).card = t.card := diff --git a/src/data/finset/prod.lean b/src/data/finset/prod.lean index 9b4c075613496..885a9af98772b 100644 --- a/src/data/finset/prod.lean +++ b/src/data/finset/prod.lean @@ -33,55 +33,58 @@ variables {s s' : finset α} {t t' : finset β} {a : α} {b : β} /-- `product s t` is the set of pairs `(a, b)` such that `a ∈ s` and `b ∈ t`. -/ protected def product (s : finset α) (t : finset β) : finset (α × β) := ⟨_, s.nodup.product t.nodup⟩ -@[simp] lemma product_val : (s.product t).1 = s.1.product t.1 := rfl +/- This notation binds more strongly than (pre)images, unions and intersections. -/ +infixr ` ×ˢ `:82 := finset.product -@[simp] lemma mem_product {p : α × β} : p ∈ s.product t ↔ p.1 ∈ s ∧ p.2 ∈ t := mem_product +@[simp] lemma product_val : (s ×ˢ t).1 = s.1 ×ˢ t.1 := rfl -lemma mk_mem_product (ha : a ∈ s) (hb : b ∈ t) : (a, b) ∈ s.product t := mem_product.2 ⟨ha, hb⟩ +@[simp] lemma mem_product {p : α × β} : p ∈ s ×ˢ t ↔ p.1 ∈ s ∧ p.2 ∈ t := mem_product + +lemma mk_mem_product (ha : a ∈ s) (hb : b ∈ t) : (a, b) ∈ s ×ˢ t := mem_product.2 ⟨ha, hb⟩ @[simp, norm_cast] lemma coe_product (s : finset α) (t : finset β) : - (s.product t : set (α × β)) = (s : set α) ×ˢ (t : set β) := + (↑(s ×ˢ t) : set (α × β)) = s ×ˢ t := set.ext $ λ x, finset.mem_product lemma subset_product [decidable_eq α] [decidable_eq β] {s : finset (α × β)} : - s ⊆ (s.image prod.fst).product (s.image prod.snd) := + s ⊆ s.image prod.fst ×ˢ s.image prod.snd := λ p hp, mem_product.2 ⟨mem_image_of_mem _ hp, mem_image_of_mem _ hp⟩ -lemma product_subset_product (hs : s ⊆ s') (ht : t ⊆ t') : s.product t ⊆ s'.product t' := +lemma product_subset_product (hs : s ⊆ s') (ht : t ⊆ t') : s ×ˢ t ⊆ s' ×ˢ t' := λ ⟨x,y⟩ h, mem_product.2 ⟨hs (mem_product.1 h).1, ht (mem_product.1 h).2⟩ -lemma product_subset_product_left (hs : s ⊆ s') : s.product t ⊆ s'.product t := +lemma product_subset_product_left (hs : s ⊆ s') : s ×ˢ t ⊆ s' ×ˢ t := product_subset_product hs (subset.refl _) -lemma product_subset_product_right (ht : t ⊆ t') : s.product t ⊆ s.product t' := +lemma product_subset_product_right (ht : t ⊆ t') : s ×ˢ t ⊆ s ×ˢ t' := product_subset_product (subset.refl _) ht lemma product_eq_bUnion [decidable_eq α] [decidable_eq β] (s : finset α) (t : finset β) : - s.product t = s.bUnion (λa, t.image $ λb, (a, b)) := + s ×ˢ t = s.bUnion (λa, t.image $ λb, (a, b)) := ext $ λ ⟨x, y⟩, by simp only [mem_product, mem_bUnion, mem_image, exists_prop, prod.mk.inj_iff, and.left_comm, exists_and_distrib_left, exists_eq_right, exists_eq_left] lemma product_eq_bUnion_right [decidable_eq α] [decidable_eq β] (s : finset α) (t : finset β) : - s.product t = t.bUnion (λ b, s.image $ λ a, (a, b)) := + s ×ˢ t = t.bUnion (λ b, s.image $ λ a, (a, b)) := ext $ λ ⟨x, y⟩, by simp only [mem_product, mem_bUnion, mem_image, exists_prop, prod.mk.inj_iff, and.left_comm, exists_and_distrib_left, exists_eq_right, exists_eq_left] /-- See also `finset.sup_product_left`. -/ @[simp] lemma product_bUnion [decidable_eq γ] (s : finset α) (t : finset β) (f : α × β → finset γ) : - (s.product t).bUnion f = s.bUnion (λ a, t.bUnion (λ b, f (a, b))) := + (s ×ˢ t).bUnion f = s.bUnion (λ a, t.bUnion (λ b, f (a, b))) := by { classical, simp_rw [product_eq_bUnion, bUnion_bUnion, image_bUnion] } -@[simp] lemma card_product (s : finset α) (t : finset β) : card (s.product t) = card s * card t := +@[simp] lemma card_product (s : finset α) (t : finset β) : card (s ×ˢ t) = card s * card t := multiset.card_product _ _ lemma filter_product (p : α → Prop) (q : β → Prop) [decidable_pred p] [decidable_pred q] : - (s.product t).filter (λ (x : α × β), p x.1 ∧ q x.2) = (s.filter p).product (t.filter q) := + (s ×ˢ t).filter (λ (x : α × β), p x.1 ∧ q x.2) = s.filter p ×ˢ t.filter q := by { ext ⟨a, b⟩, simp only [mem_filter, mem_product], exact and_and_and_comm (a ∈ s) (b ∈ t) (p a) (q b) } lemma filter_product_card (s : finset α) (t : finset β) (p : α → Prop) (q : β → Prop) [decidable_pred p] [decidable_pred q] : - ((s.product t).filter (λ (x : α × β), p x.1 ↔ q x.2)).card = + ((s ×ˢ t).filter (λ (x : α × β), p x.1 ↔ q x.2)).card = (s.filter p).card * (t.filter q).card + (s.filter (not ∘ p)).card * (t.filter (not ∘ q)).card := begin classical, @@ -95,45 +98,45 @@ begin not_mem_empty], intros, assumption } end -lemma empty_product (t : finset β) : (∅ : finset α).product t = ∅ := rfl +lemma empty_product (t : finset β) : (∅ : finset α) ×ˢ t = ∅ := rfl -lemma product_empty (s : finset α) : s.product (∅ : finset β) = ∅ := +lemma product_empty (s : finset α) : s ×ˢ (∅ : finset β) = ∅ := eq_empty_of_forall_not_mem (λ x h, (finset.mem_product.1 h).2) -lemma nonempty.product (hs : s.nonempty) (ht : t.nonempty) : (s.product t).nonempty := +lemma nonempty.product (hs : s.nonempty) (ht : t.nonempty) : (s ×ˢ t).nonempty := let ⟨x, hx⟩ := hs, ⟨y, hy⟩ := ht in ⟨(x, y), mem_product.2 ⟨hx, hy⟩⟩ -lemma nonempty.fst (h : (s.product t).nonempty) : s.nonempty := +lemma nonempty.fst (h : (s ×ˢ t).nonempty) : s.nonempty := let ⟨xy, hxy⟩ := h in ⟨xy.1, (mem_product.1 hxy).1⟩ -lemma nonempty.snd (h : (s.product t).nonempty) : t.nonempty := +lemma nonempty.snd (h : (s ×ˢ t).nonempty) : t.nonempty := let ⟨xy, hxy⟩ := h in ⟨xy.2, (mem_product.1 hxy).2⟩ -@[simp] lemma nonempty_product : (s.product t).nonempty ↔ s.nonempty ∧ t.nonempty := +@[simp] lemma nonempty_product : (s ×ˢ t).nonempty ↔ s.nonempty ∧ t.nonempty := ⟨λ h, ⟨h.fst, h.snd⟩, λ h, h.1.product h.2⟩ -@[simp] lemma product_eq_empty {s : finset α} {t : finset β} : s.product t = ∅ ↔ s = ∅ ∨ t = ∅ := +@[simp] lemma product_eq_empty {s : finset α} {t : finset β} : s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅ := by rw [←not_nonempty_iff_eq_empty, nonempty_product, not_and_distrib, not_nonempty_iff_eq_empty, not_nonempty_iff_eq_empty] @[simp] lemma singleton_product {a : α} : - ({a} : finset α).product t = t.map ⟨prod.mk a, prod.mk.inj_left _⟩ := + ({a} : finset α) ×ˢ t = t.map ⟨prod.mk a, prod.mk.inj_left _⟩ := by { ext ⟨x, y⟩, simp [and.left_comm, eq_comm] } @[simp] lemma product_singleton {b : β} : - s.product {b} = s.map ⟨λ i, (i, b), prod.mk.inj_right _⟩ := + s ×ˢ {b} = s.map ⟨λ i, (i, b), prod.mk.inj_right _⟩ := by { ext ⟨x, y⟩, simp [and.left_comm, eq_comm] } lemma singleton_product_singleton {a : α} {b : β} : - ({a} : finset α).product ({b} : finset β) = {(a, b)} := + ({a} : finset α) ×ˢ ({b} : finset β) = {(a, b)} := by simp only [product_singleton, function.embedding.coe_fn_mk, map_singleton] @[simp] lemma union_product [decidable_eq α] [decidable_eq β] : - (s ∪ s').product t = s.product t ∪ s'.product t := + (s ∪ s') ×ˢ t = s ×ˢ t ∪ s' ×ˢ t := by { ext ⟨x, y⟩, simp only [or_and_distrib_right, mem_union, mem_product] } @[simp] lemma product_union [decidable_eq α] [decidable_eq β] : - s.product (t ∪ t') = s.product t ∪ s.product t' := + s ×ˢ (t ∪ t') = s ×ˢ t ∪ s ×ˢ t' := by { ext ⟨x, y⟩, simp only [and_or_distrib_left, mem_union, mem_product] } end prod @@ -143,11 +146,11 @@ variables (s t : finset α) [decidable_eq α] /-- Given a finite set `s`, the diagonal, `s.diag` is the set of pairs of the form `(a, a)` for `a ∈ s`. -/ -def diag := (s.product s).filter (λ (a : α × α), a.fst = a.snd) +def diag := (s ×ˢ s).filter (λ a : α × α, a.fst = a.snd) /-- Given a finite set `s`, the off-diagonal, `s.off_diag` is the set of pairs `(a, b)` with `a ≠ b` for `a, b ∈ s`. -/ -def off_diag := (s.product s).filter (λ (a : α × α), a.fst ≠ a.snd) +def off_diag := (s ×ˢ s).filter (λ (a : α × α), a.fst ≠ a.snd) @[simp] lemma mem_diag (x : α × α) : x ∈ s.diag ↔ x.1 ∈ s ∧ x.1 = x.2 := by { simp only [diag, mem_filter, mem_product], split; intros h; @@ -178,16 +181,16 @@ end @[simp] lemma off_diag_empty : (∅ : finset α).off_diag = ∅ := rfl -@[simp] lemma diag_union_off_diag : s.diag ∪ s.off_diag = s.product s := +@[simp] lemma diag_union_off_diag : s.diag ∪ s.off_diag = s ×ˢ s := filter_union_filter_neg_eq _ _ @[simp] lemma disjoint_diag_off_diag : disjoint s.diag s.off_diag := disjoint_filter_filter_neg _ _ -lemma product_sdiff_diag : s.product s \ s.diag = s.off_diag := +lemma product_sdiff_diag : s ×ˢ s \ s.diag = s.off_diag := by rw [←diag_union_off_diag, union_comm, union_sdiff_self, sdiff_eq_self_of_disjoint (disjoint_diag_off_diag _).symm] -lemma product_sdiff_off_diag : s.product s \ s.off_diag = s.diag := +lemma product_sdiff_off_diag : s ×ˢ s \ s.off_diag = s.diag := by rw [←diag_union_off_diag, union_sdiff_self, sdiff_eq_self_of_disjoint (disjoint_diag_off_diag _)] lemma diag_union : (s ∪ t).diag = s.diag ∪ t.diag := @@ -196,10 +199,10 @@ by { ext ⟨i, j⟩, simp only [mem_diag, mem_union, or_and_distrib_right] } variables {s t} lemma off_diag_union (h : disjoint s t) : - (s ∪ t).off_diag = s.off_diag ∪ t.off_diag ∪ s.product t ∪ t.product s := + (s ∪ t).off_diag = s.off_diag ∪ t.off_diag ∪ s ×ˢ t ∪ t ×ˢ s := begin - rw [off_diag, union_product, product_union, product_union, union_comm _ (t.product t), - union_assoc, union_left_comm (s.product t), ←union_assoc, filter_union, filter_union, ←off_diag, + rw [off_diag, union_product, product_union, product_union, union_comm _ (t ×ˢ t), + union_assoc, union_left_comm (s ×ˢ t), ←union_assoc, filter_union, filter_union, ←off_diag, ←off_diag, filter_true_of_mem, ←union_assoc], simp only [mem_union, mem_product, ne.def, prod.forall], rintro i j (⟨hi, hj⟩ | ⟨hi, hj⟩), @@ -219,7 +222,7 @@ lemma diag_insert : (insert a s).diag = insert (a, a) s.diag := by rw [insert_eq, insert_eq, diag_union, diag_singleton] lemma off_diag_insert (has : a ∉ s) : - (insert a s).off_diag = s.off_diag ∪ ({a} : finset α).product s ∪ s.product {a} := + (insert a s).off_diag = s.off_diag ∪ {a} ×ˢ s ∪ s ×ˢ {a} := by rw [insert_eq, union_comm, off_diag_union (disjoint_singleton_right.2 has), off_diag_singleton, union_empty, union_right_comm] diff --git a/src/data/finset/sym.lean b/src/data/finset/sym.lean index 73d53a96cc41a..83c74fe19d923 100644 --- a/src/data/finset/sym.lean +++ b/src/data/finset/sym.lean @@ -37,7 +37,7 @@ section sym2 variables {m : sym2 α} /-- Lifts a finset to `sym2 α`. `s.sym2` is the finset of all pairs with elements in `s`. -/ -protected def sym2 (s : finset α) : finset (sym2 α) := (s.product s).image quotient.mk +protected def sym2 (s : finset α) : finset (sym2 α) := (s ×ˢ s).image quotient.mk @[simp] lemma mem_sym2_iff : m ∈ s.sym2 ↔ ∀ a ∈ m, a ∈ s := begin diff --git a/src/data/fintype/basic.lean b/src/data/fintype/basic.lean index c3a8f2d4bec89..564a7e6accf02 100644 --- a/src/data/fintype/basic.lean +++ b/src/data/fintype/basic.lean @@ -907,10 +907,10 @@ instance {α : Type*} (β : α → Type*) (univ : finset α).sigma (λ a, (univ : finset (β a))) = univ := rfl instance (α β : Type*) [fintype α] [fintype β] : fintype (α × β) := -⟨univ.product univ, λ ⟨a, b⟩, by simp⟩ +⟨univ ×ˢ univ, λ ⟨a, b⟩, by simp⟩ @[simp] lemma finset.univ_product_univ {α β : Type*} [fintype α] [fintype β] : - (univ : finset α).product (univ : finset β) = univ := + (univ : finset α) ×ˢ (univ : finset β) = univ := rfl @[simp] theorem fintype.card_prod (α β : Type*) [fintype α] [fintype β] : diff --git a/src/data/list/defs.lean b/src/data/list/defs.lean index 0ace872e6c219..6c8c0a3cf96a0 100644 --- a/src/data/list/defs.lean +++ b/src/data/list/defs.lean @@ -540,6 +540,9 @@ def revzip (l : list α) : list (α × α) := zip l l.reverse def product (l₁ : list α) (l₂ : list β) : list (α × β) := l₁.bind $ λ a, l₂.map $ prod.mk a +/- This notation binds more strongly than (pre)images, unions and intersections. -/ +infixr ` ×ˢ `:82 := list.product + /-- `sigma l₁ l₂` is the list of dependent pairs `(a, b)` where `a ∈ l₁` and `b ∈ l₂ a`. sigma [1, 2] (λ_, [(5 : ℕ), 6]) = [(1, 5), (1, 6), (2, 5), (2, 6)] -/ diff --git a/src/data/multiset/bind.lean b/src/data/multiset/bind.lean index 7e04601843c55..9191a8111b743 100644 --- a/src/data/multiset/bind.lean +++ b/src/data/multiset/bind.lean @@ -146,35 +146,36 @@ end bind section product variables (a : α) (b : β) (s : multiset α) (t : multiset β) -/-- The multiplicity of `(a, b)` in `s.product t` is +/-- The multiplicity of `(a, b)` in `s ×ˢ t` is the product of the multiplicity of `a` in `s` and `b` in `t`. -/ def product (s : multiset α) (t : multiset β) : multiset (α × β) := s.bind $ λ a, t.map $ prod.mk a +/- This notation binds more strongly than (pre)images, unions and intersections. -/ +infixr ` ×ˢ `:82 := multiset.product + @[simp] lemma coe_product (l₁ : list α) (l₂ : list β) : @product α β l₁ l₂ = l₁.product l₂ := by { rw [product, list.product, ←coe_bind], simp } @[simp] lemma zero_product : @product α β 0 t = 0 := rfl --TODO: Add `product_zero` -@[simp] lemma cons_product : (a ::ₘ s).product t = map (prod.mk a) t + s.product t := +@[simp] lemma cons_product : (a ::ₘ s) ×ˢ t = map (prod.mk a) t + s ×ˢ t := by simp [product] -@[simp] lemma product_singleton : ({a} : multiset α).product ({b} : multiset β) = {(a, b)} := +@[simp] lemma product_singleton : ({a} : multiset α) ×ˢ ({b} : multiset β) = {(a, b)} := by simp only [product, bind_singleton, map_singleton] -@[simp] lemma add_product (s t : multiset α) (u : multiset β) : - (s + t).product u = s.product u + product t u := +@[simp] lemma add_product (s t : multiset α) (u : multiset β) : (s + t) ×ˢ u = s ×ˢ u + t ×ˢ u := by simp [product] -@[simp] lemma product_add (s : multiset α) : ∀ t u : multiset β, - s.product (t + u) = s.product t + s.product u := +@[simp] lemma product_add (s : multiset α) : ∀ t u : multiset β, s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u := multiset.induction_on s (λ t u, rfl) $ λ a s IH t u, by rw [cons_product, IH]; simp; cc @[simp] lemma mem_product {s t} : ∀ {p : α × β}, p ∈ @product α β s t ↔ p.1 ∈ s ∧ p.2 ∈ t | (a, b) := by simp [product, and.left_comm] -@[simp] lemma card_product : (s.product t).card = s.card * t.card := +@[simp] lemma card_product : (s ×ˢ t).card = s.card * t.card := by simp [product, repeat, (∘), mul_comm] end product diff --git a/src/data/set/finite.lean b/src/data/set/finite.lean index 07d0682c9efe6..b59a266730b64 100644 --- a/src/data/set/finite.lean +++ b/src/data/set/finite.lean @@ -307,7 +307,7 @@ set.fintype_lt_nat n instance fintype_prod (s : set α) (t : set β) [fintype s] [fintype t] : fintype (s ×ˢ t : set (α × β)) := -fintype.of_finset (s.to_finset.product t.to_finset) $ by simp +fintype.of_finset (s.to_finset ×ˢ t.to_finset) $ by simp /-- `image2 f s t` is `fintype` if `s` and `t` are. -/ instance fintype_image2 [decidable_eq γ] (f : α → β → γ) (s : set α) (t : set β) diff --git a/src/data/set/pairwise.lean b/src/data/set/pairwise.lean index db4d17d4d8ba2..e5fee97a3f25b 100644 --- a/src/data/set/pairwise.lean +++ b/src/data/set/pairwise.lean @@ -389,7 +389,7 @@ noncomputable def bUnion_eq_sigma_of_disjoint {s : set ι} {f : ι → set α} disjoint iff `f` is injective . -/ lemma pairwise_disjoint_image_right_iff {f : α → β → γ} {s : set α} {t : set β} (hf : ∀ a ∈ s, injective (f a)) : - s.pairwise_disjoint (λ a, f a '' t) ↔ (s ×ˢ t : set (α × β)).inj_on (λ p, f p.1 p.2) := + s.pairwise_disjoint (λ a, f a '' t) ↔ (s ×ˢ t).inj_on (λ p, f p.1 p.2) := begin refine ⟨λ hs x hx y hy (h : f _ _ = _), _, λ hs x hx y hy h, _⟩, { suffices : x.1 = y.1, @@ -405,7 +405,7 @@ end disjoint iff `f` is injective . -/ lemma pairwise_disjoint_image_left_iff {f : α → β → γ} {s : set α} {t : set β} (hf : ∀ b ∈ t, injective (λ a, f a b)) : - t.pairwise_disjoint (λ b, (λ a, f a b) '' s) ↔ (s ×ˢ t : set (α × β)).inj_on (λ p, f p.1 p.2) := + t.pairwise_disjoint (λ b, (λ a, f a b) '' s) ↔ (s ×ˢ t).inj_on (λ p, f p.1 p.2) := begin refine ⟨λ ht x hx y hy (h : f _ _ = _), _, λ ht x hx y hy h, _⟩, { suffices : x.2 = y.2, diff --git a/src/data/set/pointwise.lean b/src/data/set/pointwise.lean index 54aae70a1ba16..c2f070e655720 100644 --- a/src/data/set/pointwise.lean +++ b/src/data/set/pointwise.lean @@ -1268,7 +1268,7 @@ section left_cancel_semigroup variables [left_cancel_semigroup α] {s t : set α} @[to_additive] lemma pairwise_disjoint_smul_iff : - s.pairwise_disjoint (• t) ↔ (s ×ˢ t : set (α × α)).inj_on (λ p, p.1 * p.2) := + s.pairwise_disjoint (• t) ↔ (s ×ˢ t).inj_on (λ p, p.1 * p.2) := pairwise_disjoint_image_right_iff $ λ _ _, mul_right_injective _ end left_cancel_semigroup diff --git a/src/data/set/prod.lean b/src/data/set/prod.lean index aceb213dab742..9ca9fe0628b4f 100644 --- a/src/data/set/prod.lean +++ b/src/data/set/prod.lean @@ -21,13 +21,6 @@ type. open function -/-- Notation class for product of subobjects (sets, submonoids, subgroups, etc). -/ -class has_set_prod (α β : Type*) (γ : out_param Type*) := -(prod : α → β → γ) - -/- This notation binds more strongly than (pre)images, unions and intersections. -/ -infixr ` ×ˢ `:82 := has_set_prod.prod - namespace set /-! ### Cartesian binary product of sets -/ @@ -35,10 +28,11 @@ namespace set section prod variables {α β γ δ : Type*} {s s₁ s₂ : set α} {t t₁ t₂ : set β} {a : α} {b : β} -/-- The cartesian product `prod s t` is the set of `(a, b)` - such that `a ∈ s` and `b ∈ t`. -/ -instance : has_set_prod (set α) (set β) (set (α × β)) := -⟨λ s t, {p | p.1 ∈ s ∧ p.2 ∈ t}⟩ +/-- The cartesian product `prod s t` is the set of `(a, b)` such that `a ∈ s` and `b ∈ t`. -/ +def prod (s : set α) (t : set β) : set (α × β) := {p | p.1 ∈ s ∧ p.2 ∈ t} + +/- This notation binds more strongly than (pre)images, unions and intersections. -/ +infixr ` ×ˢ `:82 := set.prod lemma prod_eq (s : set α) (t : set β) : s ×ˢ t = prod.fst ⁻¹' s ∩ prod.snd ⁻¹' t := rfl @@ -177,13 +171,13 @@ lemma range_pair_subset (f : α → β) (g : α → γ) : have (λ x, (f x, g x)) = prod.map f g ∘ (λ x, (x, x)), from funext (λ x, rfl), by { rw [this, ← range_prod_map], apply range_comp_subset_range } -lemma nonempty.prod : s.nonempty → t.nonempty → (s ×ˢ t : set _).nonempty := +lemma nonempty.prod : s.nonempty → t.nonempty → (s ×ˢ t).nonempty := λ ⟨x, hx⟩ ⟨y, hy⟩, ⟨(x, y), ⟨hx, hy⟩⟩ -lemma nonempty.fst : (s ×ˢ t : set _).nonempty → s.nonempty := λ ⟨x, hx⟩, ⟨x.1, hx.1⟩ -lemma nonempty.snd : (s ×ˢ t : set _).nonempty → t.nonempty := λ ⟨x, hx⟩, ⟨x.2, hx.2⟩ +lemma nonempty.fst : (s ×ˢ t).nonempty → s.nonempty := λ ⟨x, hx⟩, ⟨x.1, hx.1⟩ +lemma nonempty.snd : (s ×ˢ t).nonempty → t.nonempty := λ ⟨x, hx⟩, ⟨x.2, hx.2⟩ -lemma prod_nonempty_iff : (s ×ˢ t : set _).nonempty ↔ s.nonempty ∧ t.nonempty := +lemma prod_nonempty_iff : (s ×ˢ t).nonempty ↔ s.nonempty ∧ t.nonempty := ⟨λ h, ⟨h.fst, h.snd⟩, λ h, h.1.prod h.2⟩ lemma prod_eq_empty_iff : s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅ := @@ -224,7 +218,7 @@ by { ext x, by_cases h₁ : x.1 ∈ s₁; by_cases h₂ : x.2 ∈ t₁; simp * } first set is empty. -/ lemma prod_subset_prod_iff : s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅ := begin - cases (s ×ˢ t : set _).eq_empty_or_nonempty with h h, + cases (s ×ˢ t).eq_empty_or_nonempty with h h, { simp [h, prod_eq_empty_iff.1 h] }, have st : s.nonempty ∧ t.nonempty, by rwa [prod_nonempty_iff] at h, refine ⟨λ H, or.inl ⟨_, _⟩, _⟩, @@ -237,7 +231,7 @@ begin exact prod_mono H.1 H.2 } end -lemma prod_eq_prod_iff_of_nonempty (h : (s ×ˢ t : set _).nonempty) : +lemma prod_eq_prod_iff_of_nonempty (h : (s ×ˢ t).nonempty) : s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁ := begin split, diff --git a/src/data/sym/sym2.lean b/src/data/sym/sym2.lean index 9ca39393f4146..d31ec392e4dc0 100644 --- a/src/data/sym/sym2.lean +++ b/src/data/sym/sym2.lean @@ -547,7 +547,7 @@ begin end lemma filter_image_quotient_mk_is_diag [decidable_eq α] (s : finset α) : - ((s.product s).image quotient.mk).filter is_diag = s.diag.image quotient.mk := + ((s ×ˢ s).image quotient.mk).filter is_diag = s.diag.image quotient.mk := begin ext z, induction z using quotient.induction_on, @@ -563,7 +563,7 @@ begin end lemma filter_image_quotient_mk_not_is_diag [decidable_eq α] (s : finset α) : - ((s.product s).image quotient.mk).filter (λ a : sym2 α, ¬a.is_diag) = + ((s ×ˢ s).image quotient.mk).filter (λ a : sym2 α, ¬a.is_diag) = s.off_diag.image quotient.mk := begin ext z, diff --git a/src/geometry/manifold/cont_mdiff.lean b/src/geometry/manifold/cont_mdiff.lean index 991e6e6fda5a8..e1d310f87da4d 100644 --- a/src/geometry/manifold/cont_mdiff.lean +++ b/src/geometry/manifold/cont_mdiff.lean @@ -1286,33 +1286,31 @@ begin { assume y hy, simpa only [unique_mdiff_on, unique_mdiff_within_at, hy.1, inter_comm] with mfld_simps using hs (I.symm y) hy.2 }, - have U : unique_diff_on 𝕜 ((range I ∩ I.symm ⁻¹' s) ×ˢ (univ : set E)) := - U'.prod unique_diff_on_univ, rw cont_mdiff_on_iff, refine ⟨hf.continuous_on_tangent_map_within_aux one_le_n hs, λp q, _⟩, - have A : range I ×ˢ (univ : set E) ∩ + have A : range I ×ˢ univ ∩ ((equiv.sigma_equiv_prod H E).symm ∘ λ (p : E × E), ((I.symm) p.fst, p.snd)) ⁻¹' (tangent_bundle.proj I H ⁻¹' s) - = (range I ∩ I.symm ⁻¹' s) ×ˢ (univ : set E), + = (range I ∩ I.symm ⁻¹' s) ×ˢ univ, by { ext ⟨x, v⟩, simp only with mfld_simps }, suffices h : cont_diff_on 𝕜 m (((λ (p : H' × E'), (I' p.fst, p.snd)) ∘ (equiv.sigma_equiv_prod H' E')) ∘ tangent_map_within I I' f s ∘ ((equiv.sigma_equiv_prod H E).symm) ∘ λ (p : E × E), (I.symm p.fst, p.snd)) - ((range ⇑I ∩ ⇑(I.symm) ⁻¹' s) ×ˢ (univ : set E)), + ((range ⇑I ∩ ⇑(I.symm) ⁻¹' s) ×ˢ univ), by simpa [A] using h, change cont_diff_on 𝕜 m (λ (p : E × E), ((I' (f (I.symm p.fst)), ((mfderiv_within I I' f s (I.symm p.fst)) : E → E') p.snd) : E' × E')) - ((range I ∩ I.symm ⁻¹' s) ×ˢ (univ : set E)), + ((range I ∩ I.symm ⁻¹' s) ×ˢ univ), -- check that all bits in this formula are `C^n` have hf' := cont_mdiff_on_iff.1 hf, have A : cont_diff_on 𝕜 m (I' ∘ f ∘ I.symm) (range I ∩ I.symm ⁻¹' s) := by simpa only with mfld_simps using (hf'.2 (I.symm 0) (I'.symm 0)).of_le m_le_n, have B : cont_diff_on 𝕜 m ((I' ∘ f ∘ I.symm) ∘ prod.fst) - ((range I ∩ I.symm ⁻¹' s) ×ˢ (univ : set E)) := + ((range I ∩ I.symm ⁻¹' s) ×ˢ univ) := A.comp (cont_diff_fst.cont_diff_on) (prod_subset_preimage_fst _ _), suffices C : cont_diff_on 𝕜 m (λ (p : E × E), ((fderiv_within 𝕜 (I' ∘ f ∘ I.symm) (I.symm ⁻¹' s ∩ range I) p.1 : _) p.2)) - ((range I ∩ I.symm ⁻¹' s) ×ˢ (univ : set E)), + ((range I ∩ I.symm ⁻¹' s) ×ˢ univ), { apply cont_diff_on.prod B _, apply C.congr (λp hp, _), simp only with mfld_simps at hp, diff --git a/src/geometry/manifold/mfderiv.lean b/src/geometry/manifold/mfderiv.lean index 86b7a82717c2b..00f5ce29857f6 100644 --- a/src/geometry/manifold/mfderiv.lean +++ b/src/geometry/manifold/mfderiv.lean @@ -1651,8 +1651,8 @@ begin -- rewrite the relevant set in the chart as a direct product have : (λ (p : E × F), (I.symm p.1, p.snd)) ⁻¹' e.target ∩ (λ (p : E × F), (I.symm p.1, p.snd)) ⁻¹' (e.symm ⁻¹' (sigma.fst ⁻¹' s)) ∩ - (range I ×ˢ (univ : set F)) - = (I.symm ⁻¹' (e₀.target ∩ e₀.symm⁻¹' s) ∩ range I) ×ˢ (univ : set F), + (range I ×ˢ univ) + = (I.symm ⁻¹' (e₀.target ∩ e₀.symm⁻¹' s) ∩ range I) ×ˢ univ, by mfld_set_tac, assume q hq, replace hq : q.1 ∈ (chart_at H p.1).target ∧ ((chart_at H p.1).symm : H → M) q.1 ∈ s, diff --git a/src/geometry/manifold/tangent_bundle.lean b/src/geometry/manifold/tangent_bundle.lean index ce6b2c87fb5e4..88b4ba20ef87a 100644 --- a/src/geometry/manifold/tangent_bundle.lean +++ b/src/geometry/manifold/tangent_bundle.lean @@ -134,13 +134,13 @@ end lemma coord_change_smooth (i j : atlas H M) : cont_diff_on 𝕜 ∞ (λ p : E × F, Z.coord_change i j (I.symm p.1) p.2) - ((I '' (i.1.symm.trans j.1).source) ×ˢ (univ : set F)) := + ((I '' (i.1.symm.trans j.1).source) ×ˢ univ) := begin have A : cont_diff 𝕜 ∞ (λ p : (F →L[𝕜] F) × F, p.1 p.2), { apply is_bounded_bilinear_map.cont_diff, exact is_bounded_bilinear_map_apply }, have B : cont_diff_on 𝕜 ∞ (λ (p : E × F), (Z.coord_change i j (I.symm p.1), p.snd)) - ((I '' (i.1.symm.trans j.1).source) ×ˢ (univ : set F)), + ((I '' (i.1.symm.trans j.1).source) ×ˢ univ), { apply cont_diff_on.prod _ _, { exact (Z.coord_change_smooth_clm i j).comp cont_diff_fst.cont_diff_on (prod_subset_preimage_fst _ _) }, @@ -174,7 +174,7 @@ def to_topological_vector_bundle_core : topological_vector_bundle_core 𝕜 M F (Z.to_topological_vector_bundle_core.local_triv i).base_set = i.1.source := rfl @[simp, mfld_simps] lemma target (i : atlas H M) : - (Z.to_topological_vector_bundle_core.local_triv i).target = i.1.source ×ˢ (univ : set F) := rfl + (Z.to_topological_vector_bundle_core.local_triv i).target = i.1.source ×ˢ univ := rfl /-- Local chart for the total space of a basic smooth bundle -/ def chart {e : local_homeomorph M H} (he : e ∈ atlas H M) : @@ -187,7 +187,7 @@ def chart {e : local_homeomorph M H} (he : e ∈ atlas H M) : by { simp only [chart, mem_prod], mfld_set_tac } @[simp, mfld_simps] lemma chart_target (e : local_homeomorph M H) (he : e ∈ atlas H M) : - (Z.chart he).target = e.target ×ˢ (univ : set F) := + (Z.chart he).target = e.target ×ˢ univ := by { simp only [chart], mfld_set_tac } /-- The total space of a basic smooth bundle is endowed with a charted space structure, where the @@ -240,20 +240,20 @@ begin (J.symm ⁻¹' ((Z.chart he).symm.trans (Z.chart he')).source ∩ range J), { assume e e' he he', have : J.symm ⁻¹' ((chart Z he).symm.trans (chart Z he')).source ∩ range J = - (I.symm ⁻¹' (e.symm.trans e').source ∩ range I) ×ˢ (univ : set F), + (I.symm ⁻¹' (e.symm.trans e').source ∩ range I) ×ˢ univ, by { simp only [J, chart, model_with_corners.prod], mfld_set_tac }, rw this, -- check separately that the two components of the coordinate change are smooth apply cont_diff_on.prod, show cont_diff_on 𝕜 ∞ (λ (p : E × F), (I ∘ e' ∘ e.symm ∘ I.symm) p.1) - ((I.symm ⁻¹' (e.symm.trans e').source ∩ range I) ×ˢ (univ : set F)), + ((I.symm ⁻¹' (e.symm.trans e').source ∩ range I) ×ˢ univ), { -- the coordinate change on the base is just a coordinate change for `M`, smooth since -- `M` is smooth have A : cont_diff_on 𝕜 ∞ (I ∘ (e.symm.trans e') ∘ I.symm) (I.symm ⁻¹' (e.symm.trans e').source ∩ range I) := (has_groupoid.compatible (cont_diff_groupoid ∞ I) he he').1, have B : cont_diff_on 𝕜 ∞ (λ p : E × F, p.1) - ((I.symm ⁻¹' (e.symm.trans e').source ∩ range I) ×ˢ (univ : set F)) := + ((I.symm ⁻¹' (e.symm.trans e').source ∩ range I) ×ˢ univ) := cont_diff_fst.cont_diff_on, exact cont_diff_on.comp A B (prod_subset_preimage_fst _ _) }, show cont_diff_on 𝕜 ∞ (λ (p : E × F), @@ -261,7 +261,7 @@ begin ((chart_at H (e.symm (I.symm p.1)) : M → H) (e.symm (I.symm p.1))) (Z.coord_change ⟨e, he⟩ ⟨chart_at H (e.symm (I.symm p.1)), _⟩ (e (e.symm (I.symm p.1))) p.2)) - ((I.symm ⁻¹' (e.symm.trans e').source ∩ range I) ×ˢ (univ : set F)), + ((I.symm ⁻¹' (e.symm.trans e').source ∩ range I) ×ˢ univ), { /- The coordinate change in the fiber is more complicated as its definition involves the reference chart chosen at each point. However, it appears with its inverse, so using the cocycle property one can get rid of it, and then conclude using the smoothness of the @@ -311,7 +311,7 @@ fiber corresponds to the derivative of the coordinate change in `M`. -/ have C : cont_diff_on 𝕜 ∞ (λ (p : E × E), (fderiv_within 𝕜 (I ∘ j.1 ∘ i.1.symm ∘ I.symm) (I.symm ⁻¹' (i.1.symm.trans j.1).source ∩ range I) p.1 : E → E) p.2) - ((I.symm ⁻¹' (i.1.symm.trans j.1).source ∩ range I) ×ˢ (univ : set E)) := + ((I.symm ⁻¹' (i.1.symm.trans j.1).source ∩ range I) ×ˢ univ) := cont_diff_on_fderiv_within_apply A B le_top, have D : ∀ x ∈ (I.symm ⁻¹' (i.1.symm.trans j.1).source ∩ range I), fderiv_within 𝕜 (I ∘ j.1 ∘ i.1.symm ∘ I.symm) diff --git a/src/group_theory/schreier.lean b/src/group_theory/schreier.lean index f55c3633a087b..c787ff596e72f 100644 --- a/src/group_theory/schreier.lean +++ b/src/group_theory/schreier.lean @@ -115,7 +115,7 @@ begin replace hR1 : (1 : G) ∈ R := by rwa set.mem_to_finset, refine ⟨_, _, closure_mul_image_eq_top' hR hR1 hS⟩, calc _ ≤ (R * S).card : finset.card_image_le - ... ≤ (R.product S).card : finset.card_image_le + ... ≤ (R ×ˢ S).card : finset.card_image_le ... = R.card * S.card : R.card_product S ... = H.index * S.card : congr_arg (* S.card) _, calc R.card = fintype.card R : (fintype.card_coe R).symm diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean index fa30d218469e8..97174d54c780b 100644 --- a/src/group_theory/subgroup/basic.lean +++ b/src/group_theory/subgroup/basic.lean @@ -1312,8 +1312,7 @@ def prod (H : subgroup G) (K : subgroup N) : subgroup (G × N) := .. submonoid.prod H.to_submonoid K.to_submonoid} @[to_additive coe_prod] -lemma coe_prod (H : subgroup G) (K : subgroup N) : - (H.prod K : set (G × N)) = (H : set G) ×ˢ (K : set N) := rfl +lemma coe_prod (H : subgroup G) (K : subgroup N) : (H.prod K : set (G × N)) = H ×ˢ K := rfl @[to_additive mem_prod] lemma mem_prod {H : subgroup G} {K : subgroup N} {p : G × N} : diff --git a/src/group_theory/submonoid/operations.lean b/src/group_theory/submonoid/operations.lean index 6516c99252025..e0d307a9f5b89 100644 --- a/src/group_theory/submonoid/operations.lean +++ b/src/group_theory/submonoid/operations.lean @@ -621,14 +621,12 @@ of `M × N`. -/ @[to_additive prod "Given `add_submonoid`s `s`, `t` of `add_monoid`s `A`, `B` respectively, `s × t` as an `add_submonoid` of `A × B`."] def prod (s : submonoid M) (t : submonoid N) : submonoid (M × N) := -{ carrier := (s : set M) ×ˢ (t : set N), +{ carrier := s ×ˢ t, one_mem' := ⟨s.one_mem, t.one_mem⟩, mul_mem' := λ p q hp hq, ⟨s.mul_mem hp.1 hq.1, t.mul_mem hp.2 hq.2⟩ } @[to_additive coe_prod] -lemma coe_prod (s : submonoid M) (t : submonoid N) : - (s.prod t : set (M × N)) = (s : set M) ×ˢ (t : set N) := -rfl +lemma coe_prod (s : submonoid M) (t : submonoid N) : (s.prod t : set (M × N)) = s ×ˢ t := rfl @[to_additive mem_prod] lemma mem_prod {s : submonoid M} {t : submonoid N} {p : M × N} : diff --git a/src/group_theory/subsemigroup/operations.lean b/src/group_theory/subsemigroup/operations.lean index c975e1cb6002f..f7d869856605f 100644 --- a/src/group_theory/subsemigroup/operations.lean +++ b/src/group_theory/subsemigroup/operations.lean @@ -470,13 +470,11 @@ of `M × N`. -/ @[to_additive prod "Given `add_subsemigroup`s `s`, `t` of `add_semigroup`s `A`, `B` respectively, `s × t` as an `add_subsemigroup` of `A × B`."] def prod (s : subsemigroup M) (t : subsemigroup N) : subsemigroup (M × N) := -{ carrier := (s : set M) ×ˢ (t : set N), +{ carrier := s ×ˢ t, mul_mem' := λ p q hp hq, ⟨s.mul_mem hp.1 hq.1, t.mul_mem hp.2 hq.2⟩ } @[to_additive coe_prod] -lemma coe_prod (s : subsemigroup M) (t : subsemigroup N) : - (s.prod t : set (M × N)) = (s : set M) ×ˢ (t : set N) := -rfl +lemma coe_prod (s : subsemigroup M) (t : subsemigroup N) : (s.prod t : set (M × N)) = s ×ˢ t := rfl @[to_additive mem_prod] lemma mem_prod {s : subsemigroup M} {t : subsemigroup N} {p : M × N} : diff --git a/src/linear_algebra/span.lean b/src/linear_algebra/span.lean index cea3bd449d52c..740ade5b903ca 100644 --- a/src/linear_algebra/span.lean +++ b/src/linear_algebra/span.lean @@ -668,12 +668,11 @@ variables {M' : Type*} [add_comm_monoid M'] [module R M'] (q₁ q₁' : submodul /-- The product of two submodules is a submodule. -/ def prod : submodule R (M × M') := -{ carrier := (p : set M) ×ˢ (q₁ : set M'), +{ carrier := p ×ˢ q₁, smul_mem' := by rintro a ⟨x, y⟩ ⟨hx, hy⟩; exact ⟨smul_mem _ a hx, smul_mem _ a hy⟩, .. p.to_add_submonoid.prod q₁.to_add_submonoid } -@[simp] lemma prod_coe : - (prod p q₁ : set (M × M')) = (p : set M) ×ˢ (q₁ : set M') := rfl +@[simp] lemma prod_coe : (prod p q₁ : set (M × M')) = p ×ˢ q₁ := rfl @[simp] lemma mem_prod {p : submodule R M} {q : submodule R M'} {x : M × M'} : x ∈ prod p q ↔ x.1 ∈ p ∧ x.2 ∈ q := set.mem_prod diff --git a/src/logic/equiv/set.lean b/src/logic/equiv/set.lean index 2ae28c23b6f05..4d6c03580206a 100644 --- a/src/logic/equiv/set.lean +++ b/src/logic/equiv/set.lean @@ -503,7 +503,7 @@ e.injective.preimage_surjective.forall lemma preimage_pi_equiv_pi_subtype_prod_symm_pi {α : Type*} {β : α → Type*} (p : α → Prop) [decidable_pred p] (s : Π i, set (β i)) : (pi_equiv_pi_subtype_prod p β).symm ⁻¹' pi univ s = - (pi univ (λ i : {i // p i}, s i)) ×ˢ (pi univ (λ i : {i // ¬p i}, s i)) := + (pi univ (λ i : {i // p i}, s i)) ×ˢ pi univ (λ i : {i // ¬p i}, s i) := begin ext ⟨f, g⟩, simp only [mem_preimage, mem_univ_pi, prod_mk_mem_set_prod_eq, subtype.forall, diff --git a/src/measure_theory/group/prod.lean b/src/measure_theory/group/prod.lean index 9e84e468f01ff..296ab73148c1a 100644 --- a/src/measure_theory/group/prod.lean +++ b/src/measure_theory/group/prod.lean @@ -79,7 +79,7 @@ lemma measurable_measure_mul_right (hE : measurable_set E) : measurable (λ x, μ ((λ y, y * x) ⁻¹' E)) := begin suffices : measurable (λ y, - μ ((λ x, (x, y)) ⁻¹' ((λ z : G × G, ((1 : G), z.1 * z.2)) ⁻¹' ((univ : set G) ×ˢ E)))), + μ ((λ x, (x, y)) ⁻¹' ((λ z : G × G, ((1 : G), z.1 * z.2)) ⁻¹' (univ ×ˢ E)))), { convert this, ext1 x, congr' 1 with y : 1, simp }, apply measurable_measure_prod_mk_right, exact measurable_const.prod_mk (measurable_fst.mul measurable_snd) (measurable_set.univ.prod hE) diff --git a/src/measure_theory/integral/circle_integral_transform.lean b/src/measure_theory/integral/circle_integral_transform.lean index 81ce0c737c03b..36b42bcf906b1 100644 --- a/src/measure_theory/integral/circle_integral_transform.lean +++ b/src/measure_theory/integral/circle_integral_transform.lean @@ -97,8 +97,7 @@ def circle_transform_bounding_function (R : ℝ) (z : ℂ) (w : ℂ × ℝ) : circle_transform_deriv R z w.1 (λ x, 1) w.2 lemma continuous_on_prod_circle_transform_function {R r : ℝ} (hr : r < R) {z : ℂ} : - continuous_on (λ (w : ℂ × ℝ), ((circle_map z R w.snd - w.fst)⁻¹) ^ 2) - ((closed_ball z r) ×ˢ (⊤ : set ℝ)) := + continuous_on (λ w : ℂ × ℝ, ((circle_map z R w.snd - w.fst)⁻¹) ^ 2) (closed_ball z r ×ˢ univ) := begin simp_rw ←one_div, apply_rules [continuous_on.pow, continuous_on.div, continuous_on_const], @@ -111,8 +110,7 @@ begin end lemma continuous_on_abs_circle_transform_bounding_function {R r : ℝ} (hr : r < R) (z : ℂ) : - continuous_on (abs ∘ (λ t, circle_transform_bounding_function R z t)) - ((closed_ball z r) ×ˢ (⊤ : set ℝ) : set $ ℂ × ℝ) := + continuous_on (abs ∘ (λ t, circle_transform_bounding_function R z t)) (closed_ball z r ×ˢ univ) := begin have : continuous_on (circle_transform_bounding_function R z) (closed_ball z r ×ˢ (⊤ : set ℝ)), { apply_rules [continuous_on.smul, continuous_on_const], @@ -127,12 +125,12 @@ begin end lemma abs_circle_transform_bounding_function_le {R r : ℝ} (hr : r < R) (hr' : 0 ≤ r) (z : ℂ) : - ∃ (x : ((closed_ball z r) ×ˢ [0, 2 * π] : set $ ℂ × ℝ)), - ∀ (y : ((closed_ball z r) ×ˢ [0, 2 * π] : set $ ℂ × ℝ)), + ∃ x : closed_ball z r ×ˢ [0, 2 * π], + ∀ y : closed_ball z r ×ˢ [0, 2 * π], abs (circle_transform_bounding_function R z y) ≤ abs (circle_transform_bounding_function R z x) := begin have cts := continuous_on_abs_circle_transform_bounding_function hr z, - have comp : is_compact (((closed_ball z r) ×ˢ [0, 2 * π]) : set (ℂ × ℝ)), + have comp : is_compact (closed_ball z r ×ˢ [0, 2 * π]), { apply_rules [is_compact.prod, proper_space.is_compact_closed_ball z r, is_compact_interval], }, have none := (nonempty_closed_ball.2 hr').prod nonempty_interval, simpa using is_compact.exists_forall_ge comp none (cts.mono (by { intro z, simp, tauto })), diff --git a/src/measure_theory/measurable_space.lean b/src/measure_theory/measurable_space.lean index 214a70853781f..386c3000b628f 100644 --- a/src/measure_theory/measurable_space.lean +++ b/src/measure_theory/measurable_space.lean @@ -552,7 +552,7 @@ lemma measurable_set.prod {s : set α} {t : set β} (hs : measurable_set s) (ht measurable_set (s ×ˢ t) := measurable_set.inter (measurable_fst hs) (measurable_snd ht) -lemma measurable_set_prod_of_nonempty {s : set α} {t : set β} (h : (s ×ˢ t : set _).nonempty) : +lemma measurable_set_prod_of_nonempty {s : set α} {t : set β} (h : (s ×ˢ t).nonempty) : measurable_set (s ×ˢ t) ↔ measurable_set s ∧ measurable_set t := begin rcases h with ⟨⟨x, y⟩, hx, hy⟩, @@ -565,7 +565,7 @@ end lemma measurable_set_prod {s : set α} {t : set β} : measurable_set (s ×ˢ t) ↔ (measurable_set s ∧ measurable_set t) ∨ s = ∅ ∨ t = ∅ := begin - cases (s ×ˢ t : set _).eq_empty_or_nonempty with h h, + cases (s ×ˢ t).eq_empty_or_nonempty with h h, { simp [h, prod_eq_empty_iff.mp h] }, { simp [←not_nonempty_iff_eq_empty, prod_nonempty_iff.mp h, measurable_set_prod_of_nonempty h] } end diff --git a/src/measure_theory/measure/lebesgue.lean b/src/measure_theory/measure/lebesgue.lean index bb2065e5b5fdd..0249bbb9a3c6c 100644 --- a/src/measure_theory/measure/lebesgue.lean +++ b/src/measure_theory/measure/lebesgue.lean @@ -396,8 +396,7 @@ variable {α : Type*} def region_between (f g : α → ℝ) (s : set α) : set (α × ℝ) := {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Ioo (f p.1) (g p.1)} -lemma region_between_subset (f g : α → ℝ) (s : set α) : - region_between f g s ⊆ s ×ˢ (univ : set ℝ) := +lemma region_between_subset (f g : α → ℝ) (s : set α) : region_between f g s ⊆ s ×ˢ univ := by simpa only [prod_univ, region_between, set.preimage, set_of_subset_set_of] using λ a, and.left variables [measurable_space α] {μ : measure α} {f g : α → ℝ} {s : set α} diff --git a/src/model_theory/syntax.lean b/src/model_theory/syntax.lean index 7d7c4c35869aa..18c853e3eaab4 100644 --- a/src/model_theory/syntax.lean +++ b/src/model_theory/syntax.lean @@ -864,7 +864,7 @@ def nonempty_theory : L.Theory := {sentence.card_ge L 1} /-- A theory indicating that each of a set of constants is distinct. -/ def distinct_constants_theory (s : set α) : L[[α]].Theory := -(λ ab : α × α, (((L.con ab.1).term.equal (L.con ab.2).term).not)) '' ((s ×ˢ s) ∩ (set.diagonal α)ᶜ) +(λ ab : α × α, (((L.con ab.1).term.equal (L.con ab.2).term).not)) '' (s ×ˢ s ∩ (set.diagonal α)ᶜ) variables {L} {α} diff --git a/src/number_theory/class_number/finite.lean b/src/number_theory/class_number/finite.lean index c201beff98c05..c1014c786715d 100644 --- a/src/number_theory/class_number/finite.lean +++ b/src/number_theory/class_number/finite.lean @@ -165,9 +165,7 @@ variables [decidable_eq R] /-- `finset_approx` is a finite set such that each fractional ideal in the integral closure contains an element close to `finset_approx`. -/ noncomputable def finset_approx : finset R := -((finset.univ.product finset.univ) - .image (λ (xy : _ × _), distinct_elems bS adm xy.1 - distinct_elems bS adm xy.2)) - .erase 0 +(finset.univ.image $ λ xy : _ × _, distinct_elems bS adm xy.1 - distinct_elems bS adm xy.2).erase 0 lemma finset_approx.zero_not_mem : (0 : R) ∉ finset_approx bS adm := finset.not_mem_erase _ _ @@ -183,7 +181,7 @@ begin rintro rfl, simpa using hx }, { rintros ⟨i, j, hij, rfl⟩, - refine ⟨_, ⟨i, j⟩, finset.mem_product.mpr ⟨finset.mem_univ _, finset.mem_univ _⟩, rfl⟩, + refine ⟨_, ⟨i, j⟩, finset.mem_univ _, rfl⟩, rw [ne.def, sub_eq_zero], exact λ h, hij ((distinct_elems bS adm).injective h) } end diff --git a/src/number_theory/divisors.lean b/src/number_theory/divisors.lean index edfb0e5ced1eb..22fc2c46c48fd 100644 --- a/src/number_theory/divisors.lean +++ b/src/number_theory/divisors.lean @@ -45,7 +45,7 @@ def proper_divisors : finset ℕ := finset.filter (λ x : ℕ, x ∣ n) (finset. /-- `divisors_antidiagonal n` is the `finset` of pairs `(x,y)` such that `x * y = n`. As a special case, `divisors_antidiagonal 0 = ∅`. -/ def divisors_antidiagonal : finset (ℕ × ℕ) := -((finset.Ico 1 (n + 1)).product (finset.Ico 1 (n + 1))).filter (λ x, x.fst * x.snd = n) +(Ico 1 (n + 1) ×ˢ Ico 1 (n + 1)).filter (λ x, x.fst * x.snd = n) variable {n} diff --git a/src/number_theory/legendre_symbol/gauss_eisenstein_lemmas.lean b/src/number_theory/legendre_symbol/gauss_eisenstein_lemmas.lean index bd60ea818edcf..7bb9f0735124f 100644 --- a/src/number_theory/legendre_symbol/gauss_eisenstein_lemmas.lean +++ b/src/number_theory/legendre_symbol/gauss_eisenstein_lemmas.lean @@ -206,9 +206,8 @@ calc a / b = (Ico 1 (a / b).succ).card : by simp /-- The given sum is the number of integer points in the triangle formed by the diagonal of the rectangle `(0, p/2) × (0, q/2)` -/ private lemma sum_Ico_eq_card_lt {p q : ℕ} : - ∑ a in Ico 1 (p / 2).succ, (a * q) / p = - (((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter - (λ x : ℕ × ℕ, x.2 * p ≤ x.1 * q)).card := + ∑ a in Ico 1 (p / 2).succ, (a * q) / p = ((Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ).filter $ + λ x : ℕ × ℕ, x.2 * p ≤ x.1 * q).card := if hp0 : p = 0 then by simp [hp0, finset.ext_iff] else calc ∑ a in Ico 1 (p / 2).succ, (a * q) / p = @@ -240,9 +239,9 @@ lemma sum_mul_div_add_sum_mul_div_eq_mul (p q : ℕ) [hp : fact p.prime] ∑ a in Ico 1 (q / 2).succ, (a * p) / q = (p / 2) * (q / 2) := begin - have hswap : (((Ico 1 (q / 2).succ).product (Ico 1 (p / 2).succ)).filter + have hswap : ((Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ).filter (λ x : ℕ × ℕ, x.2 * q ≤ x.1 * p)).card = - (((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter + ((Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ).filter (λ x : ℕ × ℕ, x.1 * q ≤ x.2 * p)).card := card_congr (λ x _, prod.swap x) (λ ⟨_, _⟩, by simp only [mem_filter, and_self, prod.swap_prod_mk, forall_true_iff, mem_product] @@ -252,9 +251,9 @@ begin (λ ⟨x₁, x₂⟩ h, ⟨⟨x₂, x₁⟩, by revert h; simp only [mem_filter, eq_self_iff_true, and_self, exists_prop_of_true, prod.swap_prod_mk, forall_true_iff, mem_product] {contextual := tt}⟩), have hdisj : disjoint - (((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter + ((Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ).filter (λ x : ℕ × ℕ, x.2 * p ≤ x.1 * q)) - (((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter + ((Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ).filter (λ x : ℕ × ℕ, x.1 * q ≤ x.2 * p)), { apply disjoint_filter.2 (λ x hx hpq hqp, _), have hxp : x.1 < p, from lt_of_le_of_lt @@ -265,11 +264,11 @@ begin apply_fun zmod.val at this, rw [val_cast_of_lt hxp, val_zero] at this, simpa only [this, nonpos_iff_eq_zero, mem_Ico, one_ne_zero, false_and, mem_product] using hx }, - have hunion : ((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter + have hunion : (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ).filter (λ x : ℕ × ℕ, x.2 * p ≤ x.1 * q) ∪ - ((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter + (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ).filter (λ x : ℕ × ℕ, x.1 * q ≤ x.2 * p) = - ((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)), + (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ), from finset.ext (λ x, by have := le_total (x.2 * p) (x.1 * q); simp only [mem_union, mem_filter, mem_Ico, mem_product]; tauto), rw [sum_Ico_eq_card_lt, sum_Ico_eq_card_lt, hswap, ← card_disjoint_union hdisj, hunion, diff --git a/src/order/filter/prod.lean b/src/order/filter/prod.lean index e7d13906d8bcb..7c93895fa46c3 100644 --- a/src/order/filter/prod.lean +++ b/src/order/filter/prod.lean @@ -386,7 +386,7 @@ Together with the next lemma, `map_prod_map_const_id_principal_coprod_principal` example showing that the inequality in the lemma `map_prod_map_coprod_le` can be strict. -/ lemma map_const_principal_coprod_map_id_principal {α β ι : Type*} (a : α) (b : β) (i : ι) : (map (λ _ : α, b) (𝓟 {a})).coprod (map id (𝓟 {i})) - = 𝓟 (({b} : set β) ×ˢ (univ : set ι) ∪ (univ : set β) ×ˢ ({i} : set ι)) := + = 𝓟 (({b} : set β) ×ˢ univ ∪ univ ×ˢ ({i} : set ι)) := by simp only [map_principal, filter.coprod, comap_principal, sup_principal, image_singleton, image_id, prod_univ, univ_prod] diff --git a/src/order/locally_finite.lean b/src/order/locally_finite.lean index 2cdd96d39832b..a7d3bcd28f630 100644 --- a/src/order/locally_finite.lean +++ b/src/order/locally_finite.lean @@ -660,20 +660,20 @@ instance [locally_finite_order α] [locally_finite_order β] [decidable_rel ((≤) : α × β → α × β → Prop)] : locally_finite_order (α × β) := locally_finite_order.of_Icc' (α × β) - (λ a b, (Icc a.fst b.fst).product (Icc a.snd b.snd)) + (λ a b, Icc a.fst b.fst ×ˢ Icc a.snd b.snd) (λ a b x, by { rw [mem_product, mem_Icc, mem_Icc, and_and_and_comm], refl }) instance [locally_finite_order_top α] [locally_finite_order_top β] [decidable_rel ((≤) : α × β → α × β → Prop)] : locally_finite_order_top (α × β) := locally_finite_order_top.of_Ici' (α × β) - (λ a, (Ici a.fst).product (Ici a.snd)) (λ a x, by { rw [mem_product, mem_Ici, mem_Ici], refl }) + (λ a, Ici a.fst ×ˢ Ici a.snd) (λ a x, by { rw [mem_product, mem_Ici, mem_Ici], refl }) instance [locally_finite_order_bot α] [locally_finite_order_bot β] [decidable_rel ((≤) : α × β → α × β → Prop)] : locally_finite_order_bot (α × β) := locally_finite_order_bot.of_Iic' (α × β) - (λ a, (Iic a.fst).product (Iic a.snd)) (λ a x, by { rw [mem_product, mem_Iic, mem_Iic], refl }) + (λ a, Iic a.fst ×ˢ Iic a.snd) (λ a x, by { rw [mem_product, mem_Iic, mem_Iic], refl }) end preorder diff --git a/src/order/partition/finpartition.lean b/src/order/partition/finpartition.lean index af8bf00615867..3d351d98f15ba 100644 --- a/src/order/partition/finpartition.lean +++ b/src/order/partition/finpartition.lean @@ -229,7 +229,7 @@ section inf variables [decidable_eq α] {a b c : α} instance : has_inf (finpartition a) := -⟨λ P Q, of_erase ((P.parts.product Q.parts).image $ λ bc, bc.1 ⊓ bc.2) +⟨λ P Q, of_erase ((P.parts ×ˢ Q.parts).image $ λ bc, bc.1 ⊓ bc.2) begin rw sup_indep_iff_disjoint_erase, simp only [mem_image, and_imp, exists_prop, forall_exists_index, id.def, prod.exists, @@ -250,7 +250,7 @@ instance : has_inf (finpartition a) := end⟩ @[simp] lemma parts_inf (P Q : finpartition a) : - (P ⊓ Q).parts = ((P.parts.product Q.parts).image $ λ bc : α × α, bc.1 ⊓ bc.2).erase ⊥ := rfl + (P ⊓ Q).parts = ((P.parts ×ˢ Q.parts).image $ λ bc : α × α, bc.1 ⊓ bc.2).erase ⊥ := rfl instance : semilattice_inf (finpartition a) := { inf_le_left := λ P Q b hb, begin diff --git a/src/order/well_founded_set.lean b/src/order/well_founded_set.lean index eb1ef542aca4d..ccf5bec5dbd20 100644 --- a/src/order/well_founded_set.lean +++ b/src/order/well_founded_set.lean @@ -337,7 +337,7 @@ partially_well_ordered_on_iff_exists_monotone_subseq lemma is_pwo.prod (hs : s.is_pwo) (ht : t.is_pwo) : - (s ×ˢ t : set _).is_pwo := + (s ×ˢ t).is_pwo := begin classical, rw is_pwo_iff_exists_monotone_subseq at *, diff --git a/src/ring_theory/algebra_tower.lean b/src/ring_theory/algebra_tower.lean index 9417f333be828..99878f3a6a48c 100644 --- a/src/ring_theory/algebra_tower.lean +++ b/src/ring_theory/algebra_tower.lean @@ -150,7 +150,7 @@ theorem linear_independent_smul {ι : Type v₁} {b : ι → S} {ι' : Type w₁ begin rw linear_independent_iff' at hb hc, rw linear_independent_iff'', rintros s g hg hsg ⟨i, k⟩, by_cases hik : (i, k) ∈ s, - { have h1 : ∑ i in (s.image prod.fst).product (s.image prod.snd), g i • b i.1 • c i.2 = 0, + { have h1 : ∑ i in s.image prod.fst ×ˢ s.image prod.snd, g i • b i.1 • c i.2 = 0, { rw ← hsg, exact (finset.sum_subset finset.subset_product $ λ p _ hp, show g p • b p.1 • c p.2 = 0, by rw [hg p hp, zero_smul]).symm }, rw finset.sum_product_right at h1, @@ -226,18 +226,12 @@ begin cases hAC with x hx, cases hBC with y hy, have := hy, simp_rw [eq_top_iff', mem_span_finset] at this, choose f hf, - let s : finset B := (finset.product (x ∪ (y * y)) y).image (function.uncurry f), - have hsx : ∀ (xi ∈ x) (yj ∈ y), f xi yj ∈ s := λ xi hxi yj hyj, - show function.uncurry f (xi, yj) ∈ s, - from mem_image_of_mem _ $ mem_product.2 ⟨mem_union_left _ hxi, hyj⟩, - have hsy : ∀ (yi yj yk ∈ y), f (yi * yj) yk ∈ s := λ yi hyi yj hyj yk hyk, - show function.uncurry f (yi * yj, yk) ∈ s, - from mem_image_of_mem _ $ mem_product.2 ⟨mem_union_right _ $ finset.mul_mem_mul hyi hyj, hyk⟩, + let s : finset B := finset.image₂ f (x ∪ (y * y)) y, have hxy : ∀ xi ∈ x, xi ∈ span (algebra.adjoin A (↑s : set B)) (↑(insert 1 y : finset C) : set C) := λ xi hxi, hf xi ▸ sum_mem (λ yj hyj, smul_mem (span (algebra.adjoin A (↑s : set B)) (↑(insert 1 y : finset C) : set C)) - ⟨f xi yj, algebra.subset_adjoin $ hsx xi hxi yj hyj⟩ + ⟨f xi yj, algebra.subset_adjoin $ mem_image₂_of_mem (mem_union_left _ hxi) hyj⟩ (subset_span $ mem_insert_of_mem hyj)), have hyy : span (algebra.adjoin A (↑s : set B)) (↑(insert 1 y : finset C) : set C) * span (algebra.adjoin A (↑s : set B)) (↑(insert 1 y : finset C) : set C) ≤ @@ -248,7 +242,8 @@ begin { rw mul_one, exact subset_span (set.mem_insert_of_mem _ hyi) }, { rw ← hf (yi * yj), exact set_like.mem_coe.2 (sum_mem $ λ yk hyk, smul_mem (span (algebra.adjoin A (↑s : set B)) (insert 1 ↑y : set C)) - ⟨f (yi * yj) yk, algebra.subset_adjoin $ hsy yi hyi yj hyj yk hyk⟩ + ⟨f (yi * yj) yk, algebra.subset_adjoin $ mem_image₂_of_mem (mem_union_right _ $ + mul_mem_mul hyi hyj) hyk⟩ (subset_span $ set.mem_insert_of_mem _ hyk : yk ∈ _)) } }, refine ⟨algebra.adjoin A (↑s : set B), subalgebra.fg_adjoin_finset _, insert 1 y, _⟩, refine restrict_scalars_injective A _ _ _, diff --git a/src/ring_theory/graded_algebra/radical.lean b/src/ring_theory/graded_algebra/radical.lean index f8935fb7c04cc..a4953692a153b 100644 --- a/src/ring_theory/graded_algebra/radical.lean +++ b/src/ring_theory/graded_algebra/radical.lean @@ -85,7 +85,7 @@ lemma ideal.is_homogeneous.is_prime_of_homogeneous_mem_or_mem have mem_I : proj 𝒜 max₁ x * proj 𝒜 max₂ y ∈ I, { set antidiag := - ((decompose 𝒜 x).support.product (decompose 𝒜 y).support) + ((decompose 𝒜 x).support ×ˢ (decompose 𝒜 y).support) .filter (λ z : ι × ι, z.1 + z.2 = max₁ + max₂) with ha, have mem_antidiag : (max₁, max₂) ∈ antidiag, { simp only [add_sum_erase, mem_filter, mem_product], diff --git a/src/ring_theory/integral_closure.lean b/src/ring_theory/integral_closure.lean index 2969c7751705c..013dc970075cf 100644 --- a/src/ring_theory/integral_closure.lean +++ b/src/ring_theory/integral_closure.lean @@ -219,7 +219,7 @@ begin have hyS : ∀ {p}, p ∈ y → p ∈ S := λ p hp, show p ∈ S.to_submodule, by { rw ← hy, exact subset_span hp }, -- Now `S` is a subalgebra so the product of two elements of `y` is also in `S`. - have : ∀ (jk : (↑(y.product y) : set (A × A))), jk.1.1 * jk.1.2 ∈ S.to_submodule := + have : ∀ (jk : (↑(y ×ˢ y) : set (A × A))), jk.1.1 * jk.1.2 ∈ S.to_submodule := λ jk, S.mul_mem (hyS (finset.mem_product.1 jk.2).1) (hyS (finset.mem_product.1 jk.2).2), rw [← hy, ← set.image_id ↑y] at this, simp only [finsupp.mem_span_image_iff_total] at this, -- Say `yᵢyⱼ = ∑rᵢⱼₖ yₖ` diff --git a/src/ring_theory/subring/basic.lean b/src/ring_theory/subring/basic.lean index 5de9780f72b5f..865b537154118 100644 --- a/src/ring_theory/subring/basic.lean +++ b/src/ring_theory/subring/basic.lean @@ -816,13 +816,11 @@ lemma comap_infi {ι : Sort*} (f : R →+* S) (s : ι → subring S) : /-- Given `subring`s `s`, `t` of rings `R`, `S` respectively, `s.prod t` is `s ×̂ t` as a subring of `R × S`. -/ def prod (s : subring R) (t : subring S) : subring (R × S) := -{ carrier := (s : set R) ×ˢ (t : set S), +{ carrier := s ×ˢ t, .. s.to_submonoid.prod t.to_submonoid, .. s.to_add_subgroup.prod t.to_add_subgroup} @[norm_cast] -lemma coe_prod (s : subring R) (t : subring S) : - (s.prod t : set (R × S)) = (s : set R) ×ˢ (t : set S) := -rfl +lemma coe_prod (s : subring R) (t : subring S) : (s.prod t : set (R × S)) = s ×ˢ t := rfl lemma mem_prod {s : subring R} {t : subring S} {p : R × S} : p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t := iff.rfl diff --git a/src/ring_theory/subsemiring/basic.lean b/src/ring_theory/subsemiring/basic.lean index b39772122725f..e693a75715df0 100644 --- a/src/ring_theory/subsemiring/basic.lean +++ b/src/ring_theory/subsemiring/basic.lean @@ -760,12 +760,11 @@ lemma comap_infi {ι : Sort*} (f : R →+* S) (s : ι → subsemiring S) : /-- Given `subsemiring`s `s`, `t` of semirings `R`, `S` respectively, `s.prod t` is `s × t` as a subsemiring of `R × S`. -/ def prod (s : subsemiring R) (t : subsemiring S) : subsemiring (R × S) := -{ carrier := (s : set R) ×ˢ (t : set S), +{ carrier := s ×ˢ t, .. s.to_submonoid.prod t.to_submonoid, .. s.to_add_submonoid.prod t.to_add_submonoid} @[norm_cast] -lemma coe_prod (s : subsemiring R) (t : subsemiring S) : - (s.prod t : set (R × S)) = (s : set R) ×ˢ (t : set S) := +lemma coe_prod (s : subsemiring R) (t : subsemiring S) : (s.prod t : set (R × S)) = s ×ˢ t := rfl lemma mem_prod {s : subsemiring R} {t : subsemiring S} {p : R × S} : diff --git a/src/ring_theory/witt_vector/defs.lean b/src/ring_theory/witt_vector/defs.lean index 61a2f2b150848..07648860fc301 100644 --- a/src/ring_theory/witt_vector/defs.lean +++ b/src/ring_theory/witt_vector/defs.lean @@ -369,32 +369,28 @@ by simp [mul_coeff, peval] end coeff -lemma witt_add_vars (n : ℕ) : - (witt_add p n).vars ⊆ finset.univ.product (finset.range (n + 1)) := +lemma witt_add_vars (n : ℕ) : (witt_add p n).vars ⊆ finset.univ ×ˢ finset.range (n + 1) := witt_structure_int_vars _ _ _ -lemma witt_sub_vars (n : ℕ) : - (witt_sub p n).vars ⊆ finset.univ.product (finset.range (n + 1)) := +lemma witt_sub_vars (n : ℕ) : (witt_sub p n).vars ⊆ finset.univ ×ˢ finset.range (n + 1) := witt_structure_int_vars _ _ _ -lemma witt_mul_vars (n : ℕ) : - (witt_mul p n).vars ⊆ finset.univ.product (finset.range (n + 1)) := +lemma witt_mul_vars (n : ℕ) : (witt_mul p n).vars ⊆ finset.univ ×ˢ finset.range (n + 1) := witt_structure_int_vars _ _ _ -lemma witt_neg_vars (n : ℕ) : - (witt_neg p n).vars ⊆ finset.univ.product (finset.range (n + 1)) := +lemma witt_neg_vars (n : ℕ) : (witt_neg p n).vars ⊆ finset.univ ×ˢ finset.range (n + 1) := witt_structure_int_vars _ _ _ lemma witt_nsmul_vars (m : ℕ) (n : ℕ) : - (witt_nsmul p m n).vars ⊆ finset.univ.product (finset.range (n + 1)) := + (witt_nsmul p m n).vars ⊆ finset.univ ×ˢ finset.range (n + 1) := witt_structure_int_vars _ _ _ lemma witt_zsmul_vars (m : ℤ) (n : ℕ) : - (witt_zsmul p m n).vars ⊆ finset.univ.product (finset.range (n + 1)) := + (witt_zsmul p m n).vars ⊆ finset.univ ×ˢ finset.range (n + 1) := witt_structure_int_vars _ _ _ lemma witt_pow_vars (m : ℕ) (n : ℕ) : - (witt_pow p m n).vars ⊆ finset.univ.product (finset.range (n + 1)) := + (witt_pow p m n).vars ⊆ finset.univ ×ˢ finset.range (n + 1) := witt_structure_int_vars _ _ _ end witt_vector diff --git a/src/ring_theory/witt_vector/mul_coeff.lean b/src/ring_theory/witt_vector/mul_coeff.lean index 274b845d5b2ca..5a2bed5e2b75c 100644 --- a/src/ring_theory/witt_vector/mul_coeff.lean +++ b/src/ring_theory/witt_vector/mul_coeff.lean @@ -48,8 +48,7 @@ rename (prod.mk (0 : fin 2)) (witt_polynomial p ℤ n) * include hp -lemma witt_poly_prod_vars (n : ℕ) : - (witt_poly_prod p n).vars ⊆ finset.univ.product (finset.range (n + 1)) := +lemma witt_poly_prod_vars (n : ℕ) : (witt_poly_prod p n).vars ⊆ univ ×ˢ range (n + 1) := begin rw [witt_poly_prod], apply subset.trans (vars_mul _ _), @@ -63,7 +62,7 @@ def witt_poly_prod_remainder (n : ℕ) : mv_polynomial (fin 2 × ℕ) ℤ := ∑ i in range n, p^i * (witt_mul p i)^(p^(n-i)) lemma witt_poly_prod_remainder_vars (n : ℕ) : - (witt_poly_prod_remainder p n).vars ⊆ finset.univ.product (finset.range n) := + (witt_poly_prod_remainder p n).vars ⊆ univ ×ˢ range n := begin rw [witt_poly_prod_remainder], apply subset.trans (vars_sum_subset _ _), @@ -100,7 +99,7 @@ def remainder (n : ℕ) : mv_polynomial (fin 2 × ℕ) ℤ := include hp -lemma remainder_vars (n : ℕ) : (remainder p n).vars ⊆ univ.product (range (n+1)) := +lemma remainder_vars (n : ℕ) : (remainder p n).vars ⊆ univ ×ˢ range (n + 1) := begin rw [remainder], apply subset.trans (vars_mul _ _), @@ -205,7 +204,7 @@ end lemma mul_poly_of_interest_vars (n : ℕ) : ((p ^ (n + 1) : mv_polynomial (fin 2 × ℕ) ℤ) * poly_of_interest p n).vars ⊆ - univ.product (range (n+1)) := + univ ×ˢ range (n + 1) := begin rw mul_poly_of_interest_aux5, apply subset.trans (vars_sub_subset _ _), @@ -228,7 +227,7 @@ begin exact_mod_cast hp.out.ne_zero end -lemma poly_of_interest_vars (n : ℕ) : (poly_of_interest p n).vars ⊆ univ.product (range (n+1)) := +lemma poly_of_interest_vars (n : ℕ) : (poly_of_interest p n).vars ⊆ univ ×ˢ (range (n+1)) := by rw poly_of_interest_vars_eq; apply mul_poly_of_interest_vars lemma peval_poly_of_interest (n : ℕ) (x y : 𝕎 k) : diff --git a/src/ring_theory/witt_vector/structure_polynomial.lean b/src/ring_theory/witt_vector/structure_polynomial.lean index c4e1630ad99a9..94f53c9710b23 100644 --- a/src/ring_theory/witt_vector/structure_polynomial.lean +++ b/src/ring_theory/witt_vector/structure_polynomial.lean @@ -382,7 +382,7 @@ variable (R) -- we could relax the fintype on `idx`, but then we need to cast from finset to set. -- for our applications `idx` is always finite. lemma witt_structure_rat_vars [fintype idx] (Φ : mv_polynomial idx ℚ) (n : ℕ) : - (witt_structure_rat p Φ n).vars ⊆ finset.univ.product (finset.range (n + 1)) := + (witt_structure_rat p Φ n).vars ⊆ finset.univ ×ˢ finset.range (n + 1) := begin rw witt_structure_rat, intros x hx, @@ -399,7 +399,7 @@ end -- we could relax the fintype on `idx`, but then we need to cast from finset to set. -- for our applications `idx` is always finite. lemma witt_structure_int_vars [fintype idx] (Φ : mv_polynomial idx ℤ) (n : ℕ) : - (witt_structure_int p Φ n).vars ⊆ finset.univ.product (finset.range (n + 1)) := + (witt_structure_int p Φ n).vars ⊆ finset.univ ×ˢ finset.range (n + 1) := begin have : function.injective (int.cast_ring_hom ℚ) := int.cast_injective, rw [← vars_map_of_injective _ this, map_witt_structure_int], diff --git a/src/topology/algebra/module/basic.lean b/src/topology/algebra/module/basic.lean index af6d8d860d239..dd51e5e7a73db 100644 --- a/src/topology/algebra/module/basic.lean +++ b/src/topology/algebra/module/basic.lean @@ -173,13 +173,12 @@ variables {R : Type u} {M : Type v} [module R M] [has_continuous_smul R M] lemma submodule.closure_smul_self_subset (s : submodule R M) : - (λ p : R × M, p.1 • p.2) '' ((set.univ : set R) ×ˢ closure (s : set M)) - ⊆ closure (s : set M) := + (λ p : R × M, p.1 • p.2) '' (set.univ ×ˢ closure s) ⊆ closure s := calc -(λ p : R × M, p.1 • p.2) '' ((set.univ : set R) ×ˢ closure (s : set M)) - = (λ p : R × M, p.1 • p.2) '' (closure ((set.univ : set R) ×ˢ (s : set M))) : +(λ p : R × M, p.1 • p.2) '' (set.univ ×ˢ closure s) + = (λ p : R × M, p.1 • p.2) '' closure (set.univ ×ˢ s) : by simp [closure_prod_eq] -... ⊆ closure ((λ p : R × M, p.1 • p.2) '' ((set.univ : set R) ×ˢ (s : set M))) : +... ⊆ closure ((λ p : R × M, p.1 • p.2) '' (set.univ ×ˢ s)) : image_closure_subset_closure_image continuous_smul ... = closure s : begin congr, @@ -190,10 +189,8 @@ calc end lemma submodule.closure_smul_self_eq (s : submodule R M) : - (λ p : R × M, p.1 • p.2) '' ((set.univ : set R) ×ˢ closure (s : set M)) - = closure (s : set M) := -set.subset.antisymm s.closure_smul_self_subset - (λ x hx, ⟨⟨1, x⟩, ⟨set.mem_univ _, hx⟩, one_smul R _⟩) + (λ p : R × M, p.1 • p.2) '' (set.univ ×ˢ closure s) = closure s := +s.closure_smul_self_subset.antisymm $ λ x hx, ⟨⟨1, x⟩, ⟨set.mem_univ _, hx⟩, one_smul R _⟩ variables [has_continuous_add M] diff --git a/src/topology/algebra/monoid.lean b/src/topology/algebra/monoid.lean index a837c435086de..8a0f6eb83a0d9 100644 --- a/src/topology/algebra/monoid.lean +++ b/src/topology/algebra/monoid.lean @@ -249,17 +249,17 @@ variables [topological_space M] [monoid M] [has_continuous_mul M] @[to_additive] lemma submonoid.top_closure_mul_self_subset (s : submonoid M) : - (closure (s : set M)) * closure (s : set M) ⊆ closure (s : set M) := + closure (s : set M) * closure s ⊆ closure s := calc -(closure (s : set M)) * closure (s : set M) - = (λ p : M × M, p.1 * p.2) '' (closure ((s : set M) ×ˢ (s : set M))) : by simp [closure_prod_eq] -... ⊆ closure ((λ p : M × M, p.1 * p.2) '' ((s : set M) ×ˢ (s : set M))) : +closure (s : set M) * closure s + = (λ p : M × M, p.1 * p.2) '' closure (s ×ˢ s) : by simp [closure_prod_eq] +... ⊆ closure ((λ p : M × M, p.1 * p.2) '' s ×ˢ s) : image_closure_subset_closure_image continuous_mul ... = closure s : by simp [s.coe_mul_self_eq] @[to_additive] lemma submonoid.top_closure_mul_self_eq (s : submonoid M) : - (closure (s : set M)) * closure (s : set M) = closure (s : set M) := + closure (s : set M) * closure s = closure s := subset.antisymm s.top_closure_mul_self_subset (λ x hx, ⟨x, 1, hx, subset_closure s.one_mem, mul_one _⟩) @@ -300,7 +300,7 @@ def submonoid.comm_monoid_topological_closure [t2_space M] (s : submonoid M) have h₁ : (s.topological_closure : set M) = closure s := rfl, let f₁ := λ (x : M × M), x.1 * x.2, let f₂ := λ (x : M × M), x.2 * x.1, - let S : set (M × M) := (s : set M) ×ˢ (s : set M), + let S : set (M × M) := s ×ˢ s, have h₃ : set.eq_on f₁ f₂ (closure S), { refine set.eq_on.closure _ continuous_mul (by continuity), intros x hx, diff --git a/src/topology/algebra/open_subgroup.lean b/src/topology/algebra/open_subgroup.lean index 145f6a278c965..61c5049e76d7a 100644 --- a/src/topology/algebra/open_subgroup.lean +++ b/src/topology/algebra/open_subgroup.lean @@ -124,7 +124,7 @@ variables {H : Type*} [group H] [topological_space H] /-- The product of two open subgroups as an open subgroup of the product group. -/ @[to_additive "The product of two open subgroups as an open subgroup of the product group."] def prod (U : open_subgroup G) (V : open_subgroup H) : open_subgroup (G × H) := -{ carrier := (U : set G) ×ˢ (V : set H), +{ carrier := U ×ˢ V, is_open' := U.is_open.prod V.is_open, .. (U : subgroup G).prod (V : subgroup H) } diff --git a/src/topology/algebra/order/floor.lean b/src/topology/algebra/order/floor.lean index 837b14a8f1423..26adfe819ab00 100644 --- a/src/topology/algebra/order/floor.lean +++ b/src/topology/algebra/order/floor.lean @@ -158,7 +158,7 @@ variables [order_topology α] [topological_add_group α] [topological_space β] /-- Do not use this, use `continuous_on.comp_fract` instead. -/ lemma continuous_on.comp_fract' {f : β → α → γ} - (h : continuous_on (uncurry f) $ (univ : set β) ×ˢ I) (hf : ∀ s, f s 0 = f s 1) : + (h : continuous_on (uncurry f) $ univ ×ˢ I) (hf : ∀ s, f s 0 = f s 1) : continuous (λ st : β × α, f st.1 $ fract st.2) := begin change continuous ((uncurry f) ∘ (prod.map id (fract))), @@ -167,7 +167,7 @@ begin by_cases ht : t = floor t, { rw ht, rw ← continuous_within_at_univ, - have : (univ : set (β × α)) ⊆ ((univ : set β) ×ˢ Iio ↑⌊t⌋) ∪ ((univ : set β) ×ˢ Ici ↑⌊t⌋), + have : (univ : set (β × α)) ⊆ (univ ×ˢ Iio ↑⌊t⌋) ∪ (univ ×ˢ Ici ↑⌊t⌋), { rintros p -, rw ← prod_union, exact ⟨trivial, lt_or_le p.2 _⟩ }, @@ -203,7 +203,7 @@ end lemma continuous_on.comp_fract {s : β → α} {f : β → α → γ} - (h : continuous_on (uncurry f) $ (univ : set β) ×ˢ (Icc 0 1 : set α)) + (h : continuous_on (uncurry f) $ univ ×ˢ Icc 0 1) (hs : continuous s) (hf : ∀ s, f s 0 = f s 1) : continuous (λ x : β, f x $ int.fract (s x)) := diff --git a/src/topology/constructions.lean b/src/topology/constructions.lean index 6afc7b4585541..3b991418d8de0 100644 --- a/src/topology/constructions.lean +++ b/src/topology/constructions.lean @@ -598,7 +598,7 @@ empty -/ lemma is_open_prod_iff' {s : set α} {t : set β} : is_open (s ×ˢ t) ↔ (is_open s ∧ is_open t) ∨ (s = ∅) ∨ (t = ∅) := begin - cases (s ×ˢ t : set _).eq_empty_or_nonempty with h h, + cases (s ×ˢ t).eq_empty_or_nonempty with h h, { simp [h, prod_eq_empty_iff.1 h] }, { have st : s.nonempty ∧ t.nonempty, from prod_nonempty_iff.1 h, split, @@ -631,11 +631,11 @@ lemma frontier_prod_eq (s : set α) (t : set β) : by simp only [frontier, closure_prod_eq, interior_prod_eq, prod_diff_prod] @[simp] lemma frontier_prod_univ_eq (s : set α) : - frontier (s ×ˢ (univ : set β)) = frontier s ×ˢ (univ : set β) := + frontier (s ×ˢ (univ : set β)) = frontier s ×ˢ univ := by simp [frontier_prod_eq] @[simp] lemma frontier_univ_prod_eq (s : set β) : - frontier ((univ : set α) ×ˢ s) = (univ : set α) ×ˢ (frontier s) := + frontier ((univ : set α) ×ˢ s) = univ ×ˢ frontier s := by simp [frontier_prod_eq] lemma map_mem_closure2 {s : set α} {t : set β} {u : set γ} {f : α → β → γ} {a : α} {b : β} diff --git a/src/topology/fiber_bundle.lean b/src/topology/fiber_bundle.lean index b9d5ac358a962..821fc8a1f5b7b 100644 --- a/src/topology/fiber_bundle.lean +++ b/src/topology/fiber_bundle.lean @@ -170,7 +170,7 @@ structure topological_fiber_bundle.pretrivialization (proj : Z → B) extends lo (base_set : set B) (open_base_set : is_open base_set) (source_eq : source = proj ⁻¹' base_set) -(target_eq : target = base_set ×ˢ (univ : set F)) +(target_eq : target = base_set ×ˢ univ) (proj_to_fun : ∀ p ∈ source, (to_fun p).1 = proj p) open topological_fiber_bundle @@ -233,8 +233,7 @@ begin end @[simp, mfld_simps] lemma preimage_symm_proj_inter (s : set B) : - (e.to_local_equiv.symm ⁻¹' (proj ⁻¹' s)) ∩ e.base_set ×ˢ (univ : set F) = - (s ∩ e.base_set) ×ˢ (univ : set F) := + (e.to_local_equiv.symm ⁻¹' (proj ⁻¹' s)) ∩ e.base_set ×ˢ univ = (s ∩ e.base_set) ×ˢ univ := begin ext ⟨x, y⟩, suffices : x ∈ e.base_set → (proj (e.to_local_equiv.symm (x, y)) ∈ s ↔ x ∈ s), @@ -244,13 +243,11 @@ begin end lemma target_inter_preimage_symm_source_eq (e f : pretrivialization F proj) : - f.target ∩ (f.to_local_equiv.symm) ⁻¹' e.source - = (e.base_set ∩ f.base_set) ×ˢ (univ : set F) := + f.target ∩ (f.to_local_equiv.symm) ⁻¹' e.source = (e.base_set ∩ f.base_set) ×ˢ univ := by rw [inter_comm, f.target_eq, e.source_eq, f.preimage_symm_proj_inter] lemma trans_source (e f : pretrivialization F proj) : - (f.to_local_equiv.symm.trans e.to_local_equiv).source - = (e.base_set ∩ f.base_set) ×ˢ (univ : set F) := + (f.to_local_equiv.symm.trans e.to_local_equiv).source = (e.base_set ∩ f.base_set) ×ˢ univ := by rw [local_equiv.trans_source, local_equiv.symm_source, e.target_inter_preimage_symm_source_eq] lemma symm_trans_symm (e e' : pretrivialization F proj) : @@ -259,14 +256,12 @@ lemma symm_trans_symm (e e' : pretrivialization F proj) : by rw [local_equiv.trans_symm_eq_symm_trans_symm, local_equiv.symm_symm] lemma symm_trans_source_eq (e e' : pretrivialization F proj) : - (e.to_local_equiv.symm.trans e'.to_local_equiv).source = - (e.base_set ∩ e'.base_set) ×ˢ (univ : set F) := + (e.to_local_equiv.symm.trans e'.to_local_equiv).source = (e.base_set ∩ e'.base_set) ×ˢ univ := by rw [local_equiv.trans_source, e'.source_eq, local_equiv.symm_source, e.target_eq, inter_comm, e.preimage_symm_proj_inter, inter_comm] lemma symm_trans_target_eq (e e' : pretrivialization F proj) : - (e.to_local_equiv.symm.trans e'.to_local_equiv).target = - (e.base_set ∩ e'.base_set) ×ˢ (univ : set F) := + (e.to_local_equiv.symm.trans e'.to_local_equiv).target = (e.base_set ∩ e'.base_set) ×ˢ univ := by rw [← local_equiv.symm_source, symm_trans_symm, symm_trans_source_eq, inter_comm] end topological_fiber_bundle.pretrivialization @@ -284,7 +279,7 @@ structure topological_fiber_bundle.trivialization (proj : Z → B) (base_set : set B) (open_base_set : is_open base_set) (source_eq : source = proj ⁻¹' base_set) -(target_eq : target = base_set ×ˢ (univ : set F)) +(target_eq : target = base_set ×ˢ univ) (proj_to_fun : ∀ p ∈ source, (to_local_homeomorph p).1 = proj p) open topological_fiber_bundle @@ -349,13 +344,11 @@ e.to_pretrivialization.apply_symm_apply' hx e.to_pretrivialization.symm_apply_mk_proj ex lemma symm_trans_source_eq (e e' : trivialization F proj) : - (e.to_local_equiv.symm.trans e'.to_local_equiv).source - = (e.base_set ∩ e'.base_set) ×ˢ (univ : set F) := + (e.to_local_equiv.symm.trans e'.to_local_equiv).source = (e.base_set ∩ e'.base_set) ×ˢ univ := pretrivialization.symm_trans_source_eq e.to_pretrivialization e' lemma symm_trans_target_eq (e e' : trivialization F proj) : - (e.to_local_equiv.symm.trans e'.to_local_equiv).target - = (e.base_set ∩ e'.base_set) ×ˢ (univ : set F) := + (e.to_local_equiv.symm.trans e'.to_local_equiv).target = (e.base_set ∩ e'.base_set) ×ˢ univ := pretrivialization.symm_trans_target_eq e.to_pretrivialization e' lemma coe_fst_eventually_eq_proj (ex : x ∈ e.source) : prod.fst ∘ e =ᶠ[𝓝 x] proj := @@ -644,7 +637,7 @@ end comap namespace topological_fiber_bundle.trivialization lemma is_image_preimage_prod (e : trivialization F proj) (s : set B) : - e.to_local_homeomorph.is_image (proj ⁻¹' s) (s ×ˢ (univ : set F)) := + e.to_local_homeomorph.is_image (proj ⁻¹' s) (s ×ˢ univ) := λ x hx, by simp [e.coe_fst', hx] /-- Restrict a `trivialization` to an open set in the base. `-/ @@ -675,7 +668,7 @@ noncomputable def piecewise (e e' : trivialization F proj) (s : set B) (Heq : eq_on e e' $ proj ⁻¹' (e.base_set ∩ frontier s)) : trivialization F proj := { to_local_homeomorph := e.to_local_homeomorph.piecewise e'.to_local_homeomorph - (proj ⁻¹' s) (s ×ˢ (univ : set F)) (e.is_image_preimage_prod s) (e'.is_image_preimage_prod s) + (proj ⁻¹' s) (s ×ˢ univ) (e.is_image_preimage_prod s) (e'.is_image_preimage_prod s) (by rw [e.frontier_preimage, e'.frontier_preimage, Hs]) (by rwa e.frontier_preimage), base_set := s.ite e.base_set e'.base_set, @@ -843,7 +836,7 @@ structure topological_fiber_bundle_core (ι : Type*) (B : Type*) [topological_sp (coord_change : ι → ι → B → F → F) (coord_change_self : ∀ i, ∀ x ∈ base_set i, ∀ v, coord_change i i x v = v) (coord_change_continuous : ∀ i j, continuous_on (λp : B × F, coord_change i j p.1 p.2) - (((base_set i) ∩ (base_set j)) ×ˢ (univ : set F))) + (((base_set i) ∩ (base_set j)) ×ˢ univ)) (coord_change_comp : ∀ i j k, ∀ x ∈ (base_set i) ∩ (base_set j) ∩ (base_set k), ∀ v, (coord_change j k x) (coord_change i j x v) = coord_change i k x v) @@ -884,8 +877,8 @@ def total_space := bundle.total_space Z.fiber /-- Local homeomorphism version of the trivialization change. -/ def triv_change (i j : ι) : local_homeomorph (B × F) (B × F) := -{ source := (Z.base_set i ∩ Z.base_set j) ×ˢ (univ : set F), - target := (Z.base_set i ∩ Z.base_set j) ×ˢ (univ : set F), +{ source := (Z.base_set i ∩ Z.base_set j) ×ˢ univ, + target := (Z.base_set i ∩ Z.base_set j) ×ˢ univ, to_fun := λp, ⟨p.1, Z.coord_change i j p.1 p.2⟩, inv_fun := λp, ⟨p.1, Z.coord_change j i p.1 p.2⟩, map_source' := λp hp, by simpa using hp, @@ -927,7 +920,7 @@ and use `Z.local_triv` instead. -/ def local_triv_as_local_equiv (i : ι) : local_equiv Z.total_space (B × F) := { source := Z.proj ⁻¹' (Z.base_set i), - target := Z.base_set i ×ˢ (univ : set F), + target := Z.base_set i ×ˢ univ, inv_fun := λp, ⟨p.1, Z.coord_change i (Z.index_at p.1) p.1 p.2⟩, to_fun := λp, ⟨p.1, Z.coord_change (Z.index_at p.1) i p.1 p.2⟩, map_source' := λp hp, @@ -992,7 +985,7 @@ lemma open_source' (i : ι) : is_open (Z.local_triv_as_local_equiv i).source := begin apply topological_space.generate_open.basic, simp only [exists_prop, mem_Union, mem_singleton_iff], - refine ⟨i, Z.base_set i ×ˢ (univ : set F), (Z.is_open_base_set i).prod is_open_univ, _⟩, + refine ⟨i, Z.base_set i ×ˢ univ, (Z.is_open_base_set i).prod is_open_univ, _⟩, ext p, simp only [local_triv_as_local_equiv_apply, prod_mk_mem_set_prod_eq, mem_inter_eq, and_self, mem_local_triv_as_local_equiv_source, and_true, mem_univ, mem_preimage], diff --git a/src/topology/sets/compacts.lean b/src/topology/sets/compacts.lean index cf0a8b8e63cef..606e7844bb914 100644 --- a/src/topology/sets/compacts.lean +++ b/src/topology/sets/compacts.lean @@ -108,11 +108,10 @@ congr_fun (image_eq_preimage_of_inverse f.left_inv f.right_inv) K.1 /-- The product of two `compacts`, as a `compacts` in the product space. -/ protected def prod (K : compacts α) (L : compacts β) : compacts (α × β) := -{ carrier := (K : set α) ×ˢ (L : set β), +{ carrier := K ×ˢ L, compact' := is_compact.prod K.2 L.2 } -@[simp] lemma coe_prod (K : compacts α) (L : compacts β) : - (K.prod L : set (α × β)) = (K : set α) ×ˢ (L : set β) := rfl +@[simp] lemma coe_prod (K : compacts α) (L : compacts β) : (K.prod L : set (α × β)) = K ×ˢ L := rfl end compacts @@ -172,7 +171,7 @@ protected def prod (K : nonempty_compacts α) (L : nonempty_compacts β) : .. K.to_compacts.prod L.to_compacts } @[simp] lemma coe_prod (K : nonempty_compacts α) (L : nonempty_compacts β) : - (K.prod L : set (α × β)) = (K : set α) ×ˢ (L : set β) := rfl + (K.prod L : set (α × β)) = K ×ˢ L := rfl end nonempty_compacts @@ -245,7 +244,7 @@ protected def prod (K : positive_compacts α) (L : positive_compacts β) : .. K.to_compacts.prod L.to_compacts } @[simp] lemma coe_prod (K : positive_compacts α) (L : positive_compacts β) : - (K.prod L : set (α × β)) = (K : set α) ×ˢ (L : set β) := rfl + (K.prod L : set (α × β)) = K ×ˢ L := rfl end positive_compacts @@ -326,7 +325,7 @@ protected def prod (K : compact_opens α) (L : compact_opens β) : .. K.to_compacts.prod L.to_compacts } @[simp] lemma coe_prod (K : compact_opens α) (L : compact_opens β) : - (K.prod L : set (α × β)) = (K : set α) ×ˢ (L : set β) := rfl + (K.prod L : set (α × β)) = K ×ˢ L := rfl end compact_opens end topological_space diff --git a/src/topology/uniform_space/compact_separated.lean b/src/topology/uniform_space/compact_separated.lean index e0d5d3d3836a5..e226a3b7e569e 100644 --- a/src/topology/uniform_space/compact_separated.lean +++ b/src/topology/uniform_space/compact_separated.lean @@ -221,11 +221,11 @@ hs.uniform_continuous_on_of_continuous' (is_separated_of_separated_space s) hf neighborhood `U` of `x`. -/ lemma continuous_on.tendsto_uniformly [locally_compact_space α] [compact_space β] [separated_space β] [uniform_space γ] {f : α → β → γ} {x : α} {U : set α} - (hxU : U ∈ 𝓝 x) (hU : is_separated U) (h : continuous_on ↿f (U ×ˢ (univ : set β))) : + (hxU : U ∈ 𝓝 x) (hU : is_separated U) (h : continuous_on ↿f (U ×ˢ univ)) : tendsto_uniformly f (f x) (𝓝 x) := begin rcases locally_compact_space.local_compact_nhds _ _ hxU with ⟨K, hxK, hKU, hK⟩, - have : uniform_continuous_on ↿f (K ×ˢ (univ : set β)), + have : uniform_continuous_on ↿f (K ×ˢ univ), { refine is_compact.uniform_continuous_on_of_continuous' (hK.prod compact_univ) _ (h.mono $ prod_mono hKU subset.rfl), exact (hU.mono hKU).prod (is_separated_of_separated_space _) }, diff --git a/src/topology/vector_bundle/basic.lean b/src/topology/vector_bundle/basic.lean index 371393ce6255c..a5152e0f1972f 100644 --- a/src/topology/vector_bundle/basic.lean +++ b/src/topology/vector_bundle/basic.lean @@ -351,8 +351,7 @@ lemma apply_mk_symm (e : trivialization R F E) {b : B} (hb : b ∈ e.base_set) ( e.to_pretrivialization.apply_mk_symm hb y lemma continuous_on_symm (e : trivialization R F E) : - continuous_on (λ z : B × F, total_space_mk z.1 (e.symm z.1 z.2)) - (e.base_set ×ˢ (univ : set F)) := + continuous_on (λ z : B × F, total_space_mk z.1 (e.symm z.1 z.2)) (e.base_set ×ˢ univ) := begin have : ∀ (z : B × F) (hz : z ∈ e.base_set ×ˢ (univ : set F)), total_space_mk z.1 (e.symm z.1 z.2) = e.to_local_homeomorph.symm z, @@ -490,7 +489,7 @@ target both `s ×ˢ univ`, which on this set is of the form `λ (b, v), (b, ε b map `ε` from `s` to `F ≃L[R] F`. Here continuity is with respect to the operator norm on `F →L[R] F`. -/ def continuous_transitions (e : local_equiv (B × F) (B × F)) : Prop := -∃ s : set B, e.source = s ×ˢ (univ : set F) ∧ e.target = s ×ˢ (univ : set F) +∃ s : set B, e.source = s ×ˢ univ ∧ e.target = s ×ˢ univ ∧ ∃ ε : B → (F ≃L[R] F), continuous_on (λ b, (ε b : F →L[R] F)) s ∧ ∀ b ∈ s, ∀ v : F, e (b, v) = (b, ε b v) @@ -992,8 +991,7 @@ def to_topological_fiber_prebundle (a : topological_vector_prebundle R F E) : ((a.continuous_on_coord_change he' he).prod_map continuous_on_id), have H : e'.to_fiber_bundle_pretrivialization.to_local_equiv.target ∩ e'.to_fiber_bundle_pretrivialization.to_local_equiv.symm ⁻¹' - e.to_fiber_bundle_pretrivialization.to_local_equiv.source = - (e'.base_set ∩ e.base_set) ×ˢ (univ : set F), + e.to_fiber_bundle_pretrivialization.to_local_equiv.source =(e'.base_set ∩ e.base_set) ×ˢ univ, { rw [e'.target_eq, e.source_eq], ext ⟨b, f⟩, simp only [-total_space.proj, and.congr_right_iff, e'.proj_symm_apply', iff_self, diff --git a/src/topology/vector_bundle/hom.lean b/src/topology/vector_bundle/hom.lean index d9a29f2ce10ac..a21c54f6ffe81 100644 --- a/src/topology/vector_bundle/hom.lean +++ b/src/topology/vector_bundle/hom.lean @@ -134,7 +134,7 @@ def continuous_linear_map : { to_fun := λ p, ⟨p.1, (e₂.continuous_linear_map_at p.1).comp $ p.2.comp $ e₁.symmL p.1⟩, inv_fun := λ p, ⟨p.1, (e₂.symmL p.1).comp $ p.2.comp $ e₁.continuous_linear_map_at p.1⟩, source := (bundle.total_space.proj) ⁻¹' (e₁.base_set ∩ e₂.base_set), - target := (e₁.base_set ∩ e₂.base_set) ×ˢ (set.univ : set (F₁ →SL[σ] F₂)), + target := (e₁.base_set ∩ e₂.base_set) ×ˢ set.univ, map_source' := λ ⟨x, L⟩ h, ⟨h, set.mem_univ _⟩, map_target' := λ ⟨x, f⟩ h, h.1, left_inv' := λ ⟨x, L⟩ ⟨h₁, h₂⟩, diff --git a/src/topology/vector_bundle/prod.lean b/src/topology/vector_bundle/prod.lean index 43ced74eaa23e..a7486d3642dc5 100644 --- a/src/topology/vector_bundle/prod.lean +++ b/src/topology/vector_bundle/prod.lean @@ -130,7 +130,7 @@ begin end lemma prod.continuous_inv_fun : - continuous_on (prod.inv_fun' e₁ e₂) ((e₁.base_set ∩ e₂.base_set) ×ˢ (univ : set (F₁ × F₂))) := + continuous_on (prod.inv_fun' e₁ e₂) ((e₁.base_set ∩ e₂.base_set) ×ˢ univ) := begin rw (prod.inducing_diag E₁ E₂).continuous_on_iff, have H₁ : continuous (λ p : B × F₁ × F₂, ((p.1, p.2.1), (p.1, p.2.2))) := @@ -151,7 +151,7 @@ def prod : trivialization R (F₁ × F₂) (E₁ ×ᵇ E₂) := { to_fun := prod.to_fun' e₁ e₂, inv_fun := prod.inv_fun' e₁ e₂, source := (@total_space.proj B (E₁ ×ᵇ E₂)) ⁻¹' (e₁.base_set ∩ e₂.base_set), - target := (e₁.base_set ∩ e₂.base_set) ×ˢ (set.univ : set (F₁ × F₂)), + target := (e₁.base_set ∩ e₂.base_set) ×ˢ set.univ, map_source' := λ x h, ⟨h, set.mem_univ _⟩, map_target' := λ x h, h.1, left_inv' := λ x, prod.left_inv, diff --git a/src/topology/vector_bundle/pullback.lean b/src/topology/vector_bundle/pullback.lean index 8074fd62b983c..68abd45793834 100644 --- a/src/topology/vector_bundle/pullback.lean +++ b/src/topology/vector_bundle/pullback.lean @@ -88,7 +88,7 @@ def topological_vector_bundle.trivialization.pullback (e : trivialization 𝕜 F inv_fun := λ y, @total_space_mk _ (f *ᵖ E) y.1 (e.symm (f y.1) y.2), source := pullback.lift f ⁻¹' e.source, base_set := f ⁻¹' e.base_set, - target := (f ⁻¹' e.base_set) ×ˢ (univ : set F), + target := (f ⁻¹' e.base_set) ×ˢ univ, map_source' := λ x h, by { simp_rw [e.source_eq, mem_preimage, pullback.proj_lift] at h, simp_rw [prod_mk_mem_set_prod_eq, mem_univ, and_true, mem_preimage, h] }, map_target' := λ y h, by { rw [mem_prod, mem_preimage] at h,