diff --git a/Mathlib.lean b/Mathlib.lean index 896c561fa97d3c..ed5cd718e178b1 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5117,6 +5117,7 @@ public import Mathlib.Logic.Function.Defs public import Mathlib.Logic.Function.DependsOn public import Mathlib.Logic.Function.FiberPartition public import Mathlib.Logic.Function.FromTypes +public import Mathlib.Logic.Function.Init public import Mathlib.Logic.Function.Iterate public import Mathlib.Logic.Function.OfArity public import Mathlib.Logic.Function.ULift diff --git a/Mathlib/Algebra/Algebra/NonUnitalHom.lean b/Mathlib/Algebra/Algebra/NonUnitalHom.lean index d3986be73bd13b..dd399313c609d0 100644 --- a/Mathlib/Algebra/Algebra/NonUnitalHom.lean +++ b/Mathlib/Algebra/Algebra/NonUnitalHom.lean @@ -371,11 +371,11 @@ variable [DistribMulAction R C] /-- The prod of two morphisms is a morphism. -/ @[simps] def prod (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : A →ₙₐ[R] B × C where - toFun := Pi.prod f g - map_zero' := by simp only [Pi.prod, Prod.mk_zero_zero, map_zero] - map_add' x y := by simp only [Pi.prod, Prod.mk_add_mk, map_add] - map_mul' x y := by simp only [Pi.prod, Prod.mk_mul_mk, map_mul] - map_smul' c x := by simp only [Pi.prod, map_smul, MonoidHom.id_apply, Prod.smul_mk] + toFun := Function.prod f g + map_zero' := by simp only [Function.prod, Prod.mk_zero_zero, map_zero] + map_add' x y := by simp only [Function.prod, Prod.mk_add_mk, map_add] + map_mul' x y := by simp only [Function.prod, Prod.mk_mul_mk, map_mul] + map_smul' c x := by simp only [Function.prod, map_smul, MonoidHom.id_apply, Prod.smul_mk] theorem coe_prod (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : ⇑(f.prod g) = Pi.prod f g := rfl diff --git a/Mathlib/Algebra/Algebra/Prod.lean b/Mathlib/Algebra/Algebra/Prod.lean index 46058dff5af82d..66cd3bf80c06aa 100644 --- a/Mathlib/Algebra/Algebra/Prod.lean +++ b/Mathlib/Algebra/Algebra/Prod.lean @@ -77,7 +77,7 @@ theorem snd_apply (a) : snd R A B a = a.2 := rfl variable {R} -/-- The `Pi.prod` of two morphisms is a morphism. -/ +/-- The `Function.prod` of two morphisms is a morphism. -/ @[simps!] def prod (f : A →ₐ[R] B) (g : A →ₐ[R] C) : A →ₐ[R] B × C := { f.toRingHom.prod g.toRingHom with @@ -85,7 +85,7 @@ def prod (f : A →ₐ[R] B) (g : A →ₐ[R] C) : A →ₐ[R] B × C := simp only [toRingHom_eq_coe, RingHom.toFun_eq_coe, RingHom.prod_apply, coe_toRingHom, commutes, Prod.algebraMap_apply] } -theorem coe_prod (f : A →ₐ[R] B) (g : A →ₐ[R] C) : ⇑(f.prod g) = Pi.prod f g := +theorem coe_prod (f : A →ₐ[R] B) (g : A →ₐ[R] C) : ⇑(f.prod g) = Function.prod f g := rfl @[simp] diff --git a/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean b/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean index 28bdc737819ec3..135b227cef3ad7 100644 --- a/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean +++ b/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean @@ -283,8 +283,8 @@ end bij @[to_additive (attr := simp)] lemma prod_diag (s : Finset ι) (f : ι × ι → M) : - ∏ i ∈ s.diag, f i = ∏ i ∈ s, f (i, i) := by - simp [diag] + ∏ i ∈ s.diag, f i = ∏ i ∈ s, (f ∘ Function.diag) i := by + simp [diag, Function.diag_apply] @[to_additive] theorem prod_image' [DecidableEq ι] {s : Finset κ} {g : κ → ι} (h : κ → M) diff --git a/Mathlib/Algebra/FiniteSupport/Basic.lean b/Mathlib/Algebra/FiniteSupport/Basic.lean index 66b51c3f410ed6..79ba79f7524426 100644 --- a/Mathlib/Algebra/FiniteSupport/Basic.lean +++ b/Mathlib/Algebra/FiniteSupport/Basic.lean @@ -55,7 +55,7 @@ lemma HasFiniteMulSupport.snd {M' : Type*} [One M'] {f : α → M × M'} (hf : H @[to_additive (attr := fun_prop)] lemma HasFiniteMulSupport.prodMk {M' : Type*} [One M'] {f : α → M} {g : α → M'} (hf : HasFiniteMulSupport f) (hg : HasFiniteMulSupport g) : - HasFiniteMulSupport fun a ↦ (f a, g a) := by + HasFiniteMulSupport (Function.prod f g) := by simp only [HasFiniteMulSupport] at hf hg ⊢ rw [mulSupport_prodMk f g] exact hf.union hg diff --git a/Mathlib/Algebra/Group/Prod.lean b/Mathlib/Algebra/Group/Prod.lean index 7b6de8812c6ba1..2b516ede3c9d4d 100644 --- a/Mathlib/Algebra/Group/Prod.lean +++ b/Mathlib/Algebra/Group/Prod.lean @@ -221,11 +221,11 @@ theorem coe_snd : ⇑(snd M N) = Prod.snd := `f.prod g : AddHom M (N × P)` given by `(f.prod g) x = (f x, g x)` -/] protected def prod (f : M →ₙ* N) (g : M →ₙ* P) : M →ₙ* N × P where - toFun := Pi.prod f g + toFun := Function.prod f g map_mul' x y := Prod.ext (f.map_mul x y) (g.map_mul x y) @[to_additive coe_prod] -theorem coe_prod (f : M →ₙ* N) (g : M →ₙ* P) : ⇑(f.prod g) = Pi.prod f g := +theorem coe_prod (f : M →ₙ* N) (g : M →ₙ* P) : ⇑(f.prod g) = Function.prod f g := rfl @[to_additive (attr := simp) prod_apply] @@ -387,12 +387,12 @@ given by `(f.prod g) x = (f x, g x)`. -/ `f.prod g : M →+ N × P` given by `(f.prod g) x = (f x, g x)` -/] protected def prod (f : M →* N) (g : M →* P) : M →* N × P where - toFun := Pi.prod f g + toFun := Function.prod f g map_one' := Prod.ext f.map_one g.map_one map_mul' x y := Prod.ext (f.map_mul x y) (g.map_mul x y) @[to_additive coe_prod] -theorem coe_prod (f : M →* N) (g : M →* P) : ⇑(f.prod g) = Pi.prod f g := +theorem coe_prod (f : M →* N) (g : M →* P) : ⇑(f.prod g) = Function.prod f g := rfl @[to_additive (attr := simp) prod_apply] diff --git a/Mathlib/Algebra/Lie/Prod.lean b/Mathlib/Algebra/Lie/Prod.lean index be9596c35560c2..b3e21f22fee50d 100644 --- a/Mathlib/Algebra/Lie/Prod.lean +++ b/Mathlib/Algebra/Lie/Prod.lean @@ -99,7 +99,7 @@ def prod (f : L →ₗ⁅R⁆ L₁) (g : L →ₗ⁅R⁆ L₂) : L →ₗ⁅R⁆ toLinearMap := LinearMap.prod f g map_lie' := by simp -theorem coe_prod (f : L →ₗ⁅R⁆ L₁) (g : L →ₗ⁅R⁆ L₂) : ⇑(f.prod g) = Pi.prod f g := +theorem coe_prod (f : L →ₗ⁅R⁆ L₁) (g : L →ₗ⁅R⁆ L₂) : ⇑(f.prod g) = Function.prod f g := rfl @[simp] diff --git a/Mathlib/Algebra/Notation/Pi/Defs.lean b/Mathlib/Algebra/Notation/Pi/Defs.lean index 56fb6e87726968..68580139f65f3e 100644 --- a/Mathlib/Algebra/Notation/Pi/Defs.lean +++ b/Mathlib/Algebra/Notation/Pi/Defs.lean @@ -26,14 +26,6 @@ variable {ι α β : Type*} {G M R : ι → Type*} namespace Pi --- TODO: Do we really need this definition? If so, where to put it? -/-- The mapping into a product type built from maps into each component. -/ -@[simp] -protected def prod {α β : ι → Type*} (f : ∀ i, α i) (g : ∀ i, β i) (i : ι) : α i × β i := (f i, g i) - -lemma prod_fst_snd : Pi.prod (Prod.fst : α × β → α) (Prod.snd : α × β → β) = id := rfl -lemma prod_snd_fst : Pi.prod (Prod.snd : α × β → β) (Prod.fst : α × β → α) = .swap := rfl - /-! `1`, `0`, `+`, `*`, `+ᵥ`, `•`, `^`, `-`, `⁻¹`, and `/` are defined pointwise. -/ section One diff --git a/Mathlib/Algebra/Notation/Support.lean b/Mathlib/Algebra/Notation/Support.lean index 976c3d00f51a6e..8c1e3eaa1e17d6 100644 --- a/Mathlib/Algebra/Notation/Support.lean +++ b/Mathlib/Algebra/Notation/Support.lean @@ -173,14 +173,13 @@ lemma mulSupport_comp_eq_preimage (g : κ → M) (f : ι → κ) : @[to_additive support_prodMk] lemma mulSupport_prodMk (f : ι → M) (g : ι → N) : - mulSupport (fun x ↦ (f x, g x)) = mulSupport f ∪ mulSupport g := - Set.ext fun x ↦ by - simp only [mulSupport, not_and_or, mem_union, mem_setOf_eq, Prod.mk_eq_one, Ne] + mulSupport (f ⇊ g) = mulSupport f ∪ mulSupport g := + Set.ext fun x ↦ by simp [mulSupport, Prod.ext_iff, imp_iff_not_or] @[to_additive support_prodMk'] lemma mulSupport_prodMk' (f : ι → M × N) : - mulSupport f = (mulSupport fun x ↦ (f x).1) ∪ mulSupport fun x ↦ (f x).2 := by - simp only [← mulSupport_prodMk] + mulSupport f = (mulSupport (Prod.fst ∘ f)) ∪ mulSupport (Prod.snd ∘ f) := by + simp [← mulSupport_prodMk] @[to_additive] lemma mulSupport_along_fiber_subset (f : ι × κ → M) (i : ι) : diff --git a/Mathlib/Algebra/Order/Antidiag/Pi.lean b/Mathlib/Algebra/Order/Antidiag/Pi.lean index 7f601cde03e8fe..65f3e2ae7590c3 100644 --- a/Mathlib/Algebra/Order/Antidiag/Pi.lean +++ b/Mathlib/Algebra/Order/Antidiag/Pi.lean @@ -149,10 +149,7 @@ lemma piAntidiag_empty (n : μ) : piAntidiag (∅ : Finset ι) n = if n = 0 then lemma finsetCongr_piAntidiag_eq_antidiag (n : μ) : Equiv.finsetCongr (Equiv.boolArrowEquivProd _) (piAntidiag univ n) = antidiagonal n := by - ext ⟨x₁, x₂⟩ - simp_rw [Equiv.finsetCongr_apply, mem_map, Equiv.toEmbedding, Function.Embedding.coeFn_mk, - ← Equiv.eq_symm_apply] - simp [add_comm] + simp [Finset.ext_iff, flip, add_comm] end AddCommMonoid diff --git a/Mathlib/Algebra/Ring/Prod.lean b/Mathlib/Algebra/Ring/Prod.lean index 94357bd286e99c..bf32efe783fc61 100644 --- a/Mathlib/Algebra/Ring/Prod.lean +++ b/Mathlib/Algebra/Ring/Prod.lean @@ -132,7 +132,7 @@ variable [NonUnitalNonAssocSemiring T] (f : R →ₙ+* S) (g : R →ₙ+* T) `f.prod g : R →ₙ+* S × T` given by `(f.prod g) x = (f x, g x)` -/ protected def prod (f : R →ₙ+* S) (g : R →ₙ+* T) : R →ₙ+* S × T := { MulHom.prod (f : MulHom R S) (g : MulHom R T), AddMonoidHom.prod (f : R →+ S) (g : R →+ T) with - toFun := fun x => (f x, g x) } + toFun := Function.prod f g } @[simp] theorem prod_apply (x) : f.prod g x = (f x, g x) := @@ -208,7 +208,7 @@ variable [NonAssocSemiring T] (f : R →+* S) (g : R →+* T) given by `(f.prod g) x = (f x, g x)` -/ protected def prod (f : R →+* S) (g : R →+* T) : R →+* S × T := { MonoidHom.prod (f : R →* S) (g : R →* T), AddMonoidHom.prod (f : R →+ S) (g : R →+ T) with - toFun := fun x => (f x, g x) } + toFun := Function.prod f g } @[simp] theorem prod_apply (x) : f.prod g x = (f x, g x) := diff --git a/Mathlib/Algebra/Star/StarAlgHom.lean b/Mathlib/Algebra/Star/StarAlgHom.lean index 2ef669e39999ad..311ce0599e6097 100644 --- a/Mathlib/Algebra/Star/StarAlgHom.lean +++ b/Mathlib/Algebra/Star/StarAlgHom.lean @@ -485,13 +485,13 @@ def snd : A × B →⋆ₙₐ[R] B := variable {R A B C} -/-- The `Pi.prod` of two morphisms is a morphism. -/ +/-- The `Function.prod` of two morphisms is a morphism. -/ @[simps!] def prod (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) : A →⋆ₙₐ[R] B × C := { f.toNonUnitalAlgHom.prod g.toNonUnitalAlgHom with map_star' := fun x => by simp [map_star, Prod.star_def] } -theorem coe_prod (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) : ⇑(f.prod g) = Pi.prod f g := +theorem coe_prod (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) : ⇑(f.prod g) = Function.prod f g := rfl @[simp] @@ -504,7 +504,7 @@ theorem snd_prod (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) : (snd R B @[simp] theorem prod_fst_snd : prod (fst R A B) (snd R A B) = 1 := - DFunLike.coe_injective Pi.prod_fst_snd + DFunLike.coe_injective Function.prod_fst_snd /-- Taking the product of two maps with the same domain is equivalent to taking the product of their codomains. -/ @@ -590,12 +590,12 @@ def snd : A × B →⋆ₐ[R] B := variable {R A B C} -/-- The `Pi.prod` of two morphisms is a morphism. -/ +/-- The `Function.prod` of two morphisms is a morphism. -/ @[simps!] def prod (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) : A →⋆ₐ[R] B × C := - { f.toAlgHom.prod g.toAlgHom with map_star' := fun x => by simp [Prod.star_def, map_star] } + { f.toAlgHom.prod g.toAlgHom with map_star' := by simp [Prod.star_def, map_star, Prod.ext_iff] } -theorem coe_prod (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) : ⇑(f.prod g) = Pi.prod f g := +theorem coe_prod (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) : ⇑(f.prod g) = Function.prod f g := rfl @[simp] @@ -608,7 +608,7 @@ theorem snd_prod (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) : (snd R B C).com @[simp] theorem prod_fst_snd : prod (fst R A B) (snd R A B) = 1 := - DFunLike.coe_injective Pi.prod_fst_snd + DFunLike.coe_injective Function.prod_fst_snd /-- Taking the product of two maps with the same domain is equivalent to taking the product of their codomains. -/ diff --git a/Mathlib/Analysis/Analytic/Constructions.lean b/Mathlib/Analysis/Analytic/Constructions.lean index 8e4a7cb6769404..68bf87c40ed249 100644 --- a/Mathlib/Analysis/Analytic/Constructions.lean +++ b/Mathlib/Analysis/Analytic/Constructions.lean @@ -290,7 +290,7 @@ lemma FormalMultilinearSeries.radius_prod_eq_min lemma HasFPowerSeriesWithinOnBall.prod {e : E} {f : E → F} {g : E → G} {r s : ℝ≥0∞} {t : Set E} {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G} (hf : HasFPowerSeriesWithinOnBall f p t e r) (hg : HasFPowerSeriesWithinOnBall g q t e s) : - HasFPowerSeriesWithinOnBall (fun x ↦ (f x, g x)) (p.prod q) t e (min r s) where + HasFPowerSeriesWithinOnBall (f ⇊ g) (p.prod q) t e (min r s) where r_le := by rw [p.radius_prod_eq_min] exact min_le_min hf.r_le hg.r_le @@ -305,14 +305,14 @@ lemma HasFPowerSeriesWithinOnBall.prod {e : E} {f : E → F} {g : E → G} {r s lemma HasFPowerSeriesOnBall.prod {e : E} {f : E → F} {g : E → G} {r s : ℝ≥0∞} {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G} (hf : HasFPowerSeriesOnBall f p e r) (hg : HasFPowerSeriesOnBall g q e s) : - HasFPowerSeriesOnBall (fun x ↦ (f x, g x)) (p.prod q) e (min r s) := by + HasFPowerSeriesOnBall (f ⇊ g) (p.prod q) e (min r s) := by rw [← hasFPowerSeriesWithinOnBall_univ] at hf hg ⊢ exact hf.prod hg lemma HasFPowerSeriesWithinAt.prod {e : E} {f : E → F} {g : E → G} {s : Set E} {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G} (hf : HasFPowerSeriesWithinAt f p s e) (hg : HasFPowerSeriesWithinAt g q s e) : - HasFPowerSeriesWithinAt (fun x ↦ (f x, g x)) (p.prod q) s e := by + HasFPowerSeriesWithinAt (f ⇊ g) (p.prod q) s e := by rcases hf with ⟨_, hf⟩ rcases hg with ⟨_, hg⟩ exact ⟨_, hf.prod hg⟩ @@ -320,7 +320,7 @@ lemma HasFPowerSeriesWithinAt.prod {e : E} {f : E → F} {g : E → G} {s : Set lemma HasFPowerSeriesAt.prod {e : E} {f : E → F} {g : E → G} {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G} (hf : HasFPowerSeriesAt f p e) (hg : HasFPowerSeriesAt g q e) : - HasFPowerSeriesAt (fun x ↦ (f x, g x)) (p.prod q) e := by + HasFPowerSeriesAt (f ⇊ g) (p.prod q) e := by rcases hf with ⟨_, hf⟩ rcases hg with ⟨_, hg⟩ exact ⟨_, hf.prod hg⟩ @@ -328,7 +328,7 @@ lemma HasFPowerSeriesAt.prod {e : E} {f : E → F} {g : E → G} /-- The Cartesian product of analytic functions is analytic. -/ lemma AnalyticWithinAt.prod {e : E} {f : E → F} {g : E → G} {s : Set E} (hf : AnalyticWithinAt 𝕜 f s e) (hg : AnalyticWithinAt 𝕜 g s e) : - AnalyticWithinAt 𝕜 (fun x ↦ (f x, g x)) s e := by + AnalyticWithinAt 𝕜 (f ⇊ g) s e := by rcases hf with ⟨_, hf⟩ rcases hg with ⟨_, hg⟩ exact ⟨_, hf.prod hg⟩ @@ -337,7 +337,7 @@ lemma AnalyticWithinAt.prod {e : E} {f : E → F} {g : E → G} {s : Set E} @[fun_prop] lemma AnalyticAt.prod {e : E} {f : E → F} {g : E → G} (hf : AnalyticAt 𝕜 f e) (hg : AnalyticAt 𝕜 g e) : - AnalyticAt 𝕜 (fun x ↦ (f x, g x)) e := by + AnalyticAt 𝕜 (f ⇊ g) e := by rcases hf with ⟨_, hf⟩ rcases hg with ⟨_, hg⟩ exact ⟨_, hf.prod hg⟩ @@ -345,13 +345,13 @@ lemma AnalyticAt.prod {e : E} {f : E → F} {g : E → G} /-- The Cartesian product of analytic functions within a set is analytic. -/ lemma AnalyticOn.prod {f : E → F} {g : E → G} {s : Set E} (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) : - AnalyticOn 𝕜 (fun x ↦ (f x, g x)) s := + AnalyticOn 𝕜 (f ⇊ g) s := fun x hx ↦ (hf x hx).prod (hg x hx) /-- The Cartesian product of analytic functions is analytic. -/ lemma AnalyticOnNhd.prod {f : E → F} {g : E → G} {s : Set E} (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOnNhd 𝕜 g s) : - AnalyticOnNhd 𝕜 (fun x ↦ (f x, g x)) s := + AnalyticOnNhd 𝕜 (f ⇊ g) s := fun x hx ↦ (hf x hx).prod (hg x hx) /-- `AnalyticAt.comp` for functions on product spaces -/ diff --git a/Mathlib/Analysis/Asymptotics/TVS.lean b/Mathlib/Analysis/Asymptotics/TVS.lean index 50c5e8a599a193..79ef727ffdc35e 100644 --- a/Mathlib/Analysis/Asymptotics/TVS.lean +++ b/Mathlib/Analysis/Asymptotics/TVS.lean @@ -464,7 +464,7 @@ lemma IsLittleOTVS.bot : f =o[𝕜; ⊥] g := ⟨fun u hU ↦ ⟨univ, by simp [EventuallyLE]⟩⟩ theorem IsLittleOTVS.prodMk [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 F] {k : α → G} - (hf : f =o[𝕜; l] k) (hg : g =o[𝕜; l] k) : (fun x ↦ (f x, g x)) =o[𝕜; l] k := by + (hf : f =o[𝕜; l] k) (hg : g =o[𝕜; l] k) : (f ⇊ g) =o[𝕜; l] k := by rw [((nhds_basis_balanced 𝕜 E).prod_nhds (nhds_basis_balanced 𝕜 F)).isLittleOTVS_iff (basis_sets _)] rintro ⟨U, V⟩ ⟨⟨hU, hUb⟩, hV, hVb⟩ @@ -484,11 +484,11 @@ protected theorem IsLittleOTVS.snd {f : α → E × F} {g : α → G} (h : f =o[ @[simp] theorem isLittleOTVS_prodMk_left [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 F] {k : α → G} : - (fun x ↦ (f x, g x)) =o[𝕜; l] k ↔ f =o[𝕜; l] k ∧ g =o[𝕜; l] k := + (f ⇊ g) =o[𝕜; l] k ↔ f =o[𝕜; l] k ∧ g =o[𝕜; l] k := ⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.elim .prodMk⟩ theorem IsBigOTVS.prodMk [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 F] {k : α → G} - (hf : f =O[𝕜; l] k) (hg : g =O[𝕜; l] k) : (fun x ↦ (f x, g x)) =O[𝕜; l] k := by + (hf : f =O[𝕜; l] k) (hg : g =O[𝕜; l] k) : (f ⇊ g) =O[𝕜; l] k := by rw [((nhds_basis_balanced 𝕜 E).prod_nhds (nhds_basis_balanced 𝕜 F)).isBigOTVS_iff (basis_sets _)] rintro ⟨U, V⟩ ⟨⟨hU, hUb⟩, hV, hVb⟩ rcases ((hf.eventually_smallSets U hU).and (hg.eventually_smallSets V hV)).exists_mem_of_smallSets @@ -507,7 +507,7 @@ protected theorem IsBigOTVS.snd {f : α → E × F} {g : α → G} (h : f =O[ @[simp] theorem isBigOTVS_prodMk_left [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 F] {k : α → G} : - (fun x ↦ (f x, g x)) =O[𝕜; l] k ↔ f =O[𝕜; l] k ∧ g =O[𝕜; l] k := + (f ⇊ g) =O[𝕜; l] k ↔ f =O[𝕜; l] k ∧ g =O[𝕜; l] k := ⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.elim .prodMk⟩ @[to_fun] diff --git a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean index e0ad3b97537a73..3a54ae4ceeea09 100644 --- a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean +++ b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean @@ -588,7 +588,7 @@ theorem ContDiff.prodMk {f : E → F} {g : E → G} (hf : ContDiff 𝕜 n f) (hg theorem iteratedFDerivWithin_prodMk {f : E → F} {g : E → G} (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) (hs : UniqueDiffOn 𝕜 s) (ha : x ∈ s) {i : ℕ} (hi : i ≤ n) : - iteratedFDerivWithin 𝕜 i (fun x ↦ (f x, g x)) s x = + iteratedFDerivWithin 𝕜 i (f ⇊ g) s x = (iteratedFDerivWithin 𝕜 i f s x).prod (iteratedFDerivWithin 𝕜 i g s x) := by ext <;> · rw [← ContinuousLinearMap.iteratedFDerivWithin_comp_left _ (hf.prodMk hg) hs ha hi] @@ -596,7 +596,7 @@ theorem iteratedFDerivWithin_prodMk {f : E → F} {g : E → G} (hf : ContDiffWi theorem iteratedFDeriv_prodMk {f : E → F} {g : E → G} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) {i : ℕ} (hi : i ≤ n) : - iteratedFDeriv 𝕜 i (fun x ↦ (f x, g x)) x = + iteratedFDeriv 𝕜 i (f ⇊ g) x = (iteratedFDeriv 𝕜 i f x).prod (iteratedFDeriv 𝕜 i g x) := by simp only [← iteratedFDerivWithin_univ] exact iteratedFDerivWithin_prodMk hf.contDiffWithinAt hg.contDiffWithinAt uniqueDiffOn_univ diff --git a/Mathlib/Analysis/Calculus/ContDiffHolder/Pointwise.lean b/Mathlib/Analysis/Calculus/ContDiffHolder/Pointwise.lean index 0a34d6f0757294..0844dfb7611b8f 100644 --- a/Mathlib/Analysis/Calculus/ContDiffHolder/Pointwise.lean +++ b/Mathlib/Analysis/Calculus/ContDiffHolder/Pointwise.lean @@ -134,7 +134,7 @@ theorem snd {a : E × F} : ContDiffPointwiseHolderAt k α Prod.snd a := theorem prodMk {g : E → G} (hf : ContDiffPointwiseHolderAt k α f a) (hg : ContDiffPointwiseHolderAt k α g a) : - ContDiffPointwiseHolderAt k α (fun x ↦ (f x, g x)) a where + ContDiffPointwiseHolderAt k α (f ⇊ g) a where contDiffAt := hf.contDiffAt.prodMk hg.contDiffAt isBigO := calc _ =ᶠ[𝓝 a] (fun x ↦ (iteratedFDeriv ℝ k f x - iteratedFDeriv ℝ k f a).prod diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean index 9aa96ec2855caf..06d82e198fdba0 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean @@ -85,7 +85,7 @@ theorem HasStrictFDerivAt.const_cpow (hf : HasStrictFDerivAt f f' x) (h0 : c ≠ theorem HasFDerivAt.cpow (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) (h0 : f x ∈ slitPlane) : HasFDerivAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') x := by - convert (@Complex.hasFDerivAt_cpow ((fun x => (f x, g x)) x) h0).comp x (hf.prodMk hg) + convert (@Complex.hasFDerivAt_cpow ((Function.prod f g) x) h0).comp x (hf.prodMk hg) theorem HasFDerivAt.const_cpow (hf : HasFDerivAt f f' x) (h0 : c ≠ 0 ∨ f x ≠ 0) : HasFDerivAt (fun x => c ^ f x) ((c ^ f x * Complex.log c) • f') x := @@ -94,7 +94,7 @@ theorem HasFDerivAt.const_cpow (hf : HasFDerivAt f f' x) (h0 : c ≠ 0 ∨ f x theorem HasFDerivWithinAt.cpow (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt g g' s x) (h0 : f x ∈ slitPlane) : HasFDerivWithinAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') s x := by - convert (@Complex.hasFDerivAt_cpow ((fun x => (f x, g x)) x) h0).comp_hasFDerivWithinAt x + convert (@Complex.hasFDerivAt_cpow ((Function.prod f g) x) h0).comp_hasFDerivWithinAt x (hf.prodMk hg) theorem HasFDerivWithinAt.const_cpow (hf : HasFDerivWithinAt f f' s x) (h0 : c ≠ 0 ∨ f x ≠ 0) : @@ -387,7 +387,7 @@ theorem differentiableAt_rpow_of_ne (p : ℝ × ℝ) (hp : p.1 ≠ 0) : theorem _root_.HasStrictDerivAt.rpow {f g : ℝ → ℝ} {f' g' : ℝ} (hf : HasStrictDerivAt f f' x) (hg : HasStrictDerivAt g g' x) (h : 0 < f x) : HasStrictDerivAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) x := by - convert (hasStrictFDerivAt_rpow_of_pos ((fun x => (f x, g x)) x) h).comp_hasStrictDerivAt x + convert (hasStrictFDerivAt_rpow_of_pos ((Function.prod f g) x) h).comp_hasStrictDerivAt x (hf.prodMk hg) using 1 simp [mul_assoc, mul_comm] diff --git a/Mathlib/CategoryTheory/Bicategory/Kan/HasKan.lean b/Mathlib/CategoryTheory/Bicategory/Kan/HasKan.lean index b1ddc68a75543a..5c8b3b8f52fc9b 100644 --- a/Mathlib/CategoryTheory/Bicategory/Kan/HasKan.lean +++ b/Mathlib/CategoryTheory/Bicategory/Kan/HasKan.lean @@ -73,7 +73,7 @@ def lan (f : a ⟶ b) (g : a ⟶ c) [HasLeftKanExtension f g] : b ⟶ c := /-- `f⁺ g` is the left Kan extension of `g` along `f`. ``` b - △ \ + ⇊ \ | \ f⁺ g f | \ | ◿ diff --git a/Mathlib/Combinatorics/Enumerative/Catalan.lean b/Mathlib/Combinatorics/Enumerative/Catalan.lean index 034c6700f6b596..16fa94194a84d0 100644 --- a/Mathlib/Combinatorics/Enumerative/Catalan.lean +++ b/Mathlib/Combinatorics/Enumerative/Catalan.lean @@ -142,7 +142,7 @@ namespace Tree /-- Given two finsets, find all trees that can be formed with left child in `a` and right child in `b` -/ abbrev pairwiseNode (a b : Finset (Tree Unit)) : Finset (Tree Unit) := - (a ×ˢ b).map ⟨fun x => x.1 △ x.2, fun ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ => fun h => by simpa using h⟩ + (a ×ˢ b).map ⟨fun x => x.1 ⇊ x.2, fun ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ => fun h => by simpa using h⟩ /-- A Finset of all trees with `n` nodes. See `mem_treesOfNodesEq` -/ def treesOfNumNodesEq : ℕ → Finset (Tree Unit) diff --git a/Mathlib/Combinatorics/Enumerative/DyckWord.lean b/Mathlib/Combinatorics/Enumerative/DyckWord.lean index 7e5508cbd0a109..2509617288ac0b 100644 --- a/Mathlib/Combinatorics/Enumerative/DyckWord.lean +++ b/Mathlib/Combinatorics/Enumerative/DyckWord.lean @@ -484,10 +484,10 @@ open Tree `f(0) = nil`. For a nonzero word find the `D` that matches the initial `U`, which has index `p.firstReturn`, then let `x` be everything strictly between said `U` and `D`, and `y` be everything strictly after said `D`. `p = x.nest + y` with `x, y` (possibly empty) -Dyck words. `f(p) = f(x) △ f(y)`, where △ (defined in `Mathlib/Data/Tree/Basic.lean`) joins two +Dyck words. `f(p) = f(x) ⇊ f(y)`, where ⇊ (defined in `Mathlib/Data/Tree/Basic.lean`) joins two subtrees to a new root node. -/ def toTree (p : DyckWord) : Tree Unit := - if p = 0 then nil else p.insidePart.toTree △ p.outsidePart.toTree + if p = 0 then nil else p.insidePart.toTree ⇊ p.outsidePart.toTree termination_by p.semilength decreasing_by exacts [semilength_insidePart_lt ‹_›, semilength_outsidePart_lt ‹_›] diff --git a/Mathlib/Data/Finset/Prod.lean b/Mathlib/Data/Finset/Prod.lean index 9161ff8ee434b8..242990101874a6 100644 --- a/Mathlib/Data/Finset/Prod.lean +++ b/Mathlib/Data/Finset/Prod.lean @@ -240,8 +240,7 @@ variable (s t : Finset α) /-- Given a finite set `s`, the diagonal, `s.diag` is the set of pairs of the form `(a, a)` for `a ∈ s`. -/ -def diag : Finset (α × α) := - s.map ⟨fun a ↦ (a, a), by simp [Function.Injective]⟩ +def diag : Finset (α × α) := s.map ⟨Function.diag, Function.injective_diag⟩ -- TODO: define `Multiset.offDiag`, provide basic API, use it here /-- Given a finite set `s`, the off-diagonal, `s.offDiag` is the set of pairs `(a, b)` with `a ≠ b` @@ -255,7 +254,7 @@ variable {s} {x : α × α} @[simp, grind =] theorem mem_diag : x ∈ s.diag ↔ x.1 ∈ s ∧ x.1 = x.2 := by - aesop (add simp diag) + aesop (add simp [diag, Prod.ext_iff]) @[simp, grind =] theorem mem_offDiag : x ∈ s.offDiag ↔ x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2 := by diff --git a/Mathlib/Data/Int/Cast/Prod.lean b/Mathlib/Data/Int/Cast/Prod.lean index a3473f657d8617..8b81432b435a79 100644 --- a/Mathlib/Data/Int/Cast/Prod.lean +++ b/Mathlib/Data/Int/Cast/Prod.lean @@ -7,6 +7,7 @@ module public import Mathlib.Data.Int.Cast.Basic public import Mathlib.Data.Nat.Cast.Prod +public import Mathlib.Logic.Function.Init /-! # The product of two `AddGroupWithOne`s. @@ -21,7 +22,7 @@ variable {α β : Type*} [AddGroupWithOne α] [AddGroupWithOne β] instance : AddGroupWithOne (α × β) := { Prod.instAddMonoidWithOne, Prod.instAddGroup with - intCast := fun n => (n, n) + intCast := Function.prod IntCast.intCast IntCast.intCast intCast_ofNat := fun _ => by ext <;> simp intCast_negSucc := fun _ => by ext <;> simp } diff --git a/Mathlib/Data/Nat/Cast/Prod.lean b/Mathlib/Data/Nat/Cast/Prod.lean index 8850134e8a6450..07e7ecc774d78c 100644 --- a/Mathlib/Data/Nat/Cast/Prod.lean +++ b/Mathlib/Data/Nat/Cast/Prod.lean @@ -7,6 +7,7 @@ module public import Mathlib.Algebra.Group.Prod public import Mathlib.Data.Nat.Cast.Defs +public import Mathlib.Logic.Function.Init /-! # The product of two `AddMonoidWithOne`s. @@ -24,7 +25,7 @@ variable [AddMonoidWithOne α] [AddMonoidWithOne β] instance instAddMonoidWithOne : AddMonoidWithOne (α × β) := { Prod.instAddMonoid, @Prod.instOne α β _ _ with - natCast := fun n => (n, n) + natCast := Function.prod NatCast.natCast NatCast.natCast natCast_zero := congr_arg₂ Prod.mk Nat.cast_zero Nat.cast_zero natCast_succ := fun _ => congr_arg₂ Prod.mk (Nat.cast_succ _) (Nat.cast_succ _) } diff --git a/Mathlib/Data/Prod/Basic.lean b/Mathlib/Data/Prod/Basic.lean index afaeaafe82632a..3ec15c2ec4af6b 100644 --- a/Mathlib/Data/Prod/Basic.lean +++ b/Mathlib/Data/Prod/Basic.lean @@ -9,6 +9,7 @@ public import Lean.PrettyPrinter.Delaborator.Builtins public import Mathlib.Logic.Function.Defs public import Mathlib.Logic.Function.Iterate public import Mathlib.Tactic.Inhabit +public import Mathlib.Logic.Function.Init public import Batteries.Tactic.Trans import Mathlib.Tactic.Attr.Register @@ -22,6 +23,15 @@ It also defines better delaborators for product projections. @[expose] public section +namespace Pi + +variable {ι} {α β : ι → Type*} (f : ∀ i, α i) (g : ∀ i, β i) {c} + +@[simp] theorem fst_dcomp_pair : Prod.fst ∘' (f ⇊' g) = f := rfl +@[simp] theorem snd_dcomp_pair : Prod.snd ∘' (f ⇊' g) = g := rfl + +end Pi + variable {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} namespace Prod diff --git a/Mathlib/Data/Set/Image.lean b/Mathlib/Data/Set/Image.lean index 8dba5bf16dd163..9bd84d9d2df842 100644 --- a/Mathlib/Data/Set/Image.lean +++ b/Mathlib/Data/Set/Image.lean @@ -140,6 +140,9 @@ theorem preimage_comp {s : Set γ} : g ∘ f ⁻¹' s = f ⁻¹' (g ⁻¹' s) := theorem preimage_comp_eq : preimage (g ∘ f) = preimage f ∘ preimage g := rfl +theorem preimage_prod {f : α → β} {g : α → γ} {s : Set (β × γ)} : + (f ⇊ g) ⁻¹' s = {x | (f x, g x) ∈ s} := rfl + theorem preimage_iterate_eq {f : α → α} {n : ℕ} : Set.preimage f^[n] = (Set.preimage f)^[n] := by induction n with | zero => simp @@ -219,6 +222,14 @@ theorem image_comp (f : β → γ) (g : α → β) (a : Set α) : f ∘ g '' a = theorem image_comp_eq {g : β → γ} : image (g ∘ f) = image g ∘ image f := by grind +theorem image_prodMap {δ} (f : α → β) (g : γ → δ) (s : Set (α × γ)) : + (Prod.map f g) '' s = {q | ∃ a b, (a, b) ∈ s ∧ f a = q.1 ∧ g b = q.2} := by + simp [Set.ext_iff, Prod.ext_iff] + +theorem image_prod (f : α → β) (g : α → γ) (s : Set α) : (f ⇊ g) '' s = + {x | ∃ y ∈ s, f y = x.1 ∧ g y = x.2} := by + simp [Set.ext_iff, Prod.ext_iff] + /-- A variant of `image_comp`, useful for rewriting -/ @[grind =] theorem image_image (g : β → γ) (f : α → β) (s : Set α) : g '' (f '' s) = (fun x => g (f x)) '' s := diff --git a/Mathlib/Data/Set/Lattice/Image.lean b/Mathlib/Data/Set/Lattice/Image.lean index ed904b54db22b2..d06019924b9321 100644 --- a/Mathlib/Data/Set/Lattice/Image.lean +++ b/Mathlib/Data/Set/Lattice/Image.lean @@ -515,15 +515,15 @@ theorem iUnion_image_left : ⋃ a ∈ s, f a '' t = image2 f s t := by simp only [image2_eq_iUnion, image_eq_iUnion] theorem iUnion_image_right : ⋃ b ∈ t, (f · b) '' s = image2 f s t := by - rw [image2_swap, iUnion_image_left] + rw [iUnion_image_left, image2_swap f s t] theorem image2_iUnion_left (s : ι → Set α) (t : Set β) : image2 f (⋃ i, s i) t = ⋃ i, image2 f (s i) t := by - simp only [← image_prod, iUnion_prod_const, image_iUnion] + simp only [← image_uncurry_prod, iUnion_prod_const, image_iUnion] theorem image2_iUnion_right (s : Set α) (t : ι → Set β) : image2 f s (⋃ i, t i) = ⋃ i, image2 f s (t i) := by - simp only [← image_prod, prod_iUnion, image_iUnion] + simp only [← image_uncurry_prod, prod_iUnion, image_iUnion] theorem image2_sUnion_left (S : Set (Set α)) (t : Set β) : image2 f (⋃₀ S) t = ⋃ s ∈ S, image2 f s t := by @@ -598,23 +598,19 @@ theorem seq_singleton {s : Set (α → β)} {a : α} : Set.seq s {a} = (fun f : image2_singleton_right theorem seq_seq {s : Set (β → γ)} {t : Set (α → β)} {u : Set α} : - seq s (seq t u) = seq (seq ((· ∘ ·) '' s) t) u := by - simp only [seq_eq_image2, image2_image_left] - exact .symm <| image2_assoc fun _ _ _ ↦ rfl + seq s (seq t u) = seq (seq ((· ∘ ·) '' s) t) u := by ext; aesop theorem image_seq {f : β → γ} {s : Set (α → β)} {t : Set α} : - f '' seq s t = seq ((f ∘ ·) '' s) t := by - simp only [seq, image_image2, image2_image_left, comp_apply] + f '' seq s t = seq ((f ∘ ·) '' s) t := by ext; aesop -theorem prod_eq_seq {s : Set α} {t : Set β} : s ×ˢ t = (Prod.mk '' s).seq t := by - rw [seq_eq_image2, image2_image_left, image2_mk_eq_prod] +theorem prod_eq_seq {s : Set α} {t : Set β} : s ×ˢ t = (Prod.mk '' s).seq t := by ext; aesop theorem prod_image_seq_comm (s : Set α) (t : Set β) : (Prod.mk '' s).seq t = seq ((fun b a => (a, b)) '' t) s := by rw [← prod_eq_seq, ← image_swap_prod, prod_eq_seq, image_seq, ← image_comp]; rfl theorem image2_eq_seq (f : α → β → γ) (s : Set α) (t : Set β) : image2 f s t = seq (f '' s) t := by - rw [seq_eq_image2, image2_image_left] + ext; aesop end Seq diff --git a/Mathlib/Data/Set/NAry.lean b/Mathlib/Data/Set/NAry.lean index 46fe4f361a25b2..e50f7a5e649dea 100644 --- a/Mathlib/Data/Set/NAry.lean +++ b/Mathlib/Data/Set/NAry.lean @@ -69,30 +69,28 @@ theorem image2_subset_iff_right : image2 f s t ⊆ u ↔ ∀ b ∈ t, (fun a => variable (f) -@[simp] -lemma image_prod : (fun x : α × β ↦ f x.1 x.2) '' s ×ˢ t = image2 f s t := - ext fun _ ↦ by simp [and_assoc] - @[simp] lemma image_uncurry_prod (s : Set α) (t : Set β) : uncurry f '' s ×ˢ t = image2 f s t := - image_prod _ + ext fun _ ↦ by simp [and_assoc] @[simp] lemma image2_mk_eq_prod : image2 Prod.mk s t = s ×ˢ t := ext <| by simp @[simp] lemma image2_curry (f : α × β → γ) (s : Set α) (t : Set β) : - image2 (fun a b ↦ f (a, b)) s t = f '' s ×ˢ t := by - simp [← image_uncurry_prod, uncurry] + image2 f.curry s t = f '' s ×ˢ t := by simp [← image_uncurry_prod] -theorem image2_swap (s : Set α) (t : Set β) : image2 f s t = image2 (fun a b => f b a) t s := by - grind +theorem image2_flip (s : Set α) (t : Set β) : image2 (flip f) t s = image2 f s t := by + grind [flip] + +theorem image2_swap (s : Set α) (t : Set β) : image2 f s t = image2 (fun b x ↦ f x b) t s := + (image2_flip f s t).symm variable {f} theorem image2_union_left : image2 f (s ∪ s') t = image2 f s t ∪ image2 f s' t := by - simp_rw [← image_prod, union_prod, image_union] + simp_rw [← image_uncurry_prod, union_prod, image_union] theorem image2_union_right : image2 f s (t ∪ t') = image2 f s t ∪ image2 f s t' := by - rw [← image2_swap, image2_union_left, image2_swap f, image2_swap f] + rw [← image2_flip, image2_union_left, image2_flip f, image2_flip f] lemma image2_inter_left (hf : Injective2 f) : image2 f (s ∩ s') t = image2 f s t ∩ image2 f s' t := by @@ -130,7 +128,7 @@ theorem image2_eq_empty_iff : image2 f s t = ∅ ↔ s = ∅ ∨ t = ∅ := by theorem Subsingleton.image2 (hs : s.Subsingleton) (ht : t.Subsingleton) (f : α → β → γ) : (image2 f s t).Subsingleton := by - rw [← image_prod] + rw [← image_uncurry_prod] apply (hs.prod ht).image theorem image2_inter_subset_left : image2 f (s ∩ s') t ⊆ image2 f s t ∩ image2 f s' t := @@ -176,16 +174,16 @@ theorem image2_congr' (h : ∀ a b, f a b = f' a b) : image2 f s t = image2 f' s image2_congr fun a _ b _ => h a b theorem image_image2 (f : α → β → γ) (g : γ → δ) : - g '' image2 f s t = image2 (fun a b => g (f a b)) s t := by - simp only [← image_prod, image_image] + g '' image2 f s t = g ∘ uncurry f '' s ×ˢ t := by + simp only [← image_uncurry_prod, image_comp] theorem image2_image_left (f : γ → β → δ) (g : α → γ) : - image2 f (g '' s) t = image2 (fun a b => f (g a) b) s t := by - ext; simp - + image2 f (g '' s) t = uncurry f ∘ Prod.map g id '' s ×ˢ t := by + ext; aesop +--fun a b => f (g a) b theorem image2_image_right (f : α → γ → δ) (g : β → γ) : - image2 f s (g '' t) = image2 (fun a b => f a (g b)) s t := by - ext; simp + image2 f s (g '' t) = uncurry f ∘ Prod.map id g '' s ×ˢ t := by + ext; aesop @[simp] theorem image2_left (h : t.Nonempty) : image2 (fun x _ => x) s t = s := by @@ -196,8 +194,8 @@ theorem image2_right (h : s.Nonempty) : image2 (fun _ y => y) s t = t := by simp [nonempty_def.mp h, Set.ext_iff] lemma image2_range (f : α' → β' → γ) (g : α → α') (h : β → β') : - image2 f (range g) (range h) = range fun x : α × β ↦ f (g x.1) (h x.2) := by - simp_rw [← image_univ, image2_image_left, image2_image_right, ← image_prod, univ_prod_univ] + image2 f (range g) (range h) = range (f.uncurry ∘ Prod.map g h) := by + ext; aesop theorem image2_assoc {f : δ → γ → ε} {g : α → β → δ} {f' : α → ε' → ε} {g' : β → γ → ε'} (h_assoc : ∀ a b c, f (g a b) c = f' a (g' b c)) : @@ -205,18 +203,18 @@ theorem image2_assoc {f : δ → γ → ε} {g : α → β → δ} {f' : α → eq_of_forall_subset_iff fun _ ↦ by simp only [image2_subset_iff, forall_mem_image2, h_assoc] theorem image2_comm {g : β → α → γ} (h_comm : ∀ a b, f a b = g b a) : image2 f s t = image2 g t s := - (image2_swap _ _ _).trans <| by simp_rw [h_comm] + (image2_flip _ _ _).trans <| by simp_rw [h_comm] theorem image2_left_comm {f : α → δ → ε} {g : β → γ → δ} {f' : α → γ → δ'} {g' : β → δ' → ε} (h_left_comm : ∀ a b c, f a (g b c) = g' b (f' a c)) : image2 f s (image2 g t u) = image2 g' t (image2 f' s u) := by - rw [image2_swap f', image2_swap f] + rw [← image2_flip f', ← image2_flip f] exact image2_assoc fun _ _ _ => h_left_comm _ _ _ theorem image2_right_comm {f : δ → γ → ε} {g : α → β → δ} {f' : α → γ → δ'} {g' : δ' → β → ε} (h_right_comm : ∀ a b c, f (g a b) c = g' (f' a c) b) : image2 f (image2 g s t) u = image2 g' (image2 f' s u) t := by - rw [image2_swap g, image2_swap g'] + rw [← image2_flip g, ← image2_flip g'] exact image2_assoc fun _ _ _ => h_right_comm _ _ _ theorem image2_image2_image2_comm {f : ε → ζ → ν} {g : α → β → ε} {h : γ → δ → ζ} {f' : ε' → ζ' → ν} @@ -227,8 +225,7 @@ theorem image2_image2_image2_comm {f : ε → ζ → ν} {g : α → β → ε} theorem image_image2_distrib {g : γ → δ} {f' : α' → β' → δ} {g₁ : α → α'} {g₂ : β → β'} (h_distrib : ∀ a b, g (f a b) = f' (g₁ a) (g₂ b)) : - (image2 f s t).image g = image2 f' (s.image g₁) (t.image g₂) := by - simp_rw [image_image2, image2_image_left, image2_image_right, h_distrib] + (image2 f s t).image g = image2 f' (s.image g₁) (t.image g₂) := by aesop /-- Symmetric statement to `Set.image2_image_left_comm`. -/ theorem image_image2_distrib_left {g : γ → δ} {f' : α' → β → δ} {g' : α → α'} @@ -269,7 +266,7 @@ theorem image2_distrib_subset_right {f : δ → γ → ε} {g : α → β → δ theorem image_image2_antidistrib {g : γ → δ} {f' : β' → α' → δ} {g₁ : β → β'} {g₂ : α → α'} (h_antidistrib : ∀ a b, g (f a b) = f' (g₁ b) (g₂ a)) : (image2 f s t).image g = image2 f' (t.image g₁) (s.image g₂) := by - rw [image2_swap f] + rw [← image2_flip f] exact image_image2_distrib fun _ _ => h_antidistrib _ _ /-- Symmetric statement to `Set.image2_image_left_anticomm`. -/ diff --git a/Mathlib/Data/Set/Operations.lean b/Mathlib/Data/Set/Operations.lean index f855341e8c662b..024a306cbb4709 100644 --- a/Mathlib/Data/Set/Operations.lean +++ b/Mathlib/Data/Set/Operations.lean @@ -11,6 +11,7 @@ public import Mathlib.Data.SProd public import Mathlib.Data.Subtype public import Mathlib.Order.Notation public import Mathlib.Tactic.Push.Attr +public import Mathlib.Logic.Function.Init import Mathlib.Tactic.Attr.Register import Aesop.BuiltinRules @@ -225,11 +226,11 @@ theorem prodMk_mem_set_prod_eq : ((a, b) ∈ s ×ˢ t) = (a ∈ s ∧ b ∈ t) : theorem mk_mem_prod (ha : a ∈ s) (hb : b ∈ t) : (a, b) ∈ s ×ˢ t := ⟨ha, hb⟩ theorem prod_image_left (f : α → γ) (s : Set α) (t : Set β) : - (f '' s) ×ˢ t = (fun x ↦ (f x.1, x.2)) '' s ×ˢ t := by + (f '' s) ×ˢ t = Prod.map f id '' s ×ˢ t := by aesop theorem prod_image_right (f : α → γ) (s : Set α) (t : Set β) : - t ×ˢ (f '' s) = (fun x ↦ (x.1, f x.2)) '' t ×ˢ s := by + t ×ˢ (f '' s) = Prod.map id f '' t ×ˢ s := by aesop end Prod @@ -294,7 +295,7 @@ def InjOn (f : α → β) (s : Set α) : Prop := ∀ ⦃x₁ : α⦄, x₁ ∈ s → ∀ ⦃x₂ : α⦄, x₂ ∈ s → f x₁ = f x₂ → x₁ = x₂ /-- The graph of a function `f : α → β` on a set `s`. -/ -def graphOn (f : α → β) (s : Set α) : Set (α × β) := (fun x ↦ (x, f x)) '' s +def graphOn (f : α → β) (s : Set α) : Set (α × β) := (id ⇊ f) '' s /-- `f` is surjective from `s` to `t` if `t` is contained in the image of `s`. -/ def SurjOn (f : α → β) (s : Set α) (t : Set β) : Prop := t ⊆ f '' s diff --git a/Mathlib/Data/Set/Prod.lean b/Mathlib/Data/Set/Prod.lean index 161b9cca4c1660..57dcf0e9ba1848 100644 --- a/Mathlib/Data/Set/Prod.lean +++ b/Mathlib/Data/Set/Prod.lean @@ -8,6 +8,7 @@ module public import Mathlib.Data.Set.Image public import Mathlib.Data.SProd public import Mathlib.Data.Sum.Basic +public import Mathlib.Logic.Function.Init /-! # Sets in product and pi types @@ -179,7 +180,7 @@ theorem preimage_prod_map_prod (f : α → β) (g : γ → δ) (s : Set β) (t : rfl theorem mk_preimage_prod (f : γ → α) (g : γ → β) : - (fun x => (f x, g x)) ⁻¹' s ×ˢ t = f ⁻¹' s ∩ g ⁻¹' t := + (Function.prod f g) ⁻¹' s ×ˢ t = f ⁻¹' s ∩ g ⁻¹' t := rfl @[simp] @@ -238,7 +239,7 @@ theorem prod_univ_range_eq {m₂ : β → δ} : ext <| by simp [range] theorem range_pair_subset (f : α → β) (g : α → γ) : - (range fun x => (f x, g x)) ⊆ range f ×ˢ range g := by grind + (range (Function.prod f g)) ⊆ range f ×ˢ range g := by grind theorem Nonempty.prod : s.Nonempty → t.Nonempty → (s ×ˢ t).Nonempty := fun ⟨x, hx⟩ ⟨y, hy⟩ => ⟨(x, y), ⟨hx, hy⟩⟩ @@ -259,7 +260,7 @@ theorem prod_sub_preimage_iff {W : Set γ} {f : α × β → γ} : s ×ˢ t ⊆ f ⁻¹' W ↔ ∀ a b, a ∈ s → b ∈ t → f (a, b) ∈ W := by simp [subset_def] theorem image_prodMk_subset_prod {f : α → β} {g : α → γ} {s : Set α} : - (fun x => (f x, g x)) '' s ⊆ (f '' s) ×ˢ (g '' s) := by grind + (Function.prod f g) '' s ⊆ (f '' s) ×ˢ (g '' s) := by grind theorem image_prodMk_subset_prod_left (hb : b ∈ t) : (fun a => (a, b)) '' s ⊆ s ×ˢ t := by grind @@ -408,7 +409,7 @@ end Prod /-! ### Diagonal In this section we prove some lemmas about the diagonal set `{p | p.1 = p.2}` and the diagonal map -`fun x ↦ (x, x)`. +`Function.diag`. -/ @@ -416,37 +417,35 @@ section Diagonal variable {α : Type*} {s t : Set α} +@[simp] theorem range_diag : range Function.diag = diagonal α := Set.ext <| by simp + lemma diagonal_nonempty [Nonempty α] : (diagonal α).Nonempty := - Nonempty.elim ‹_› fun x => ⟨_, mem_diagonal x⟩ + range_diag ▸ (range_nonempty Function.diag) instance decidableMemDiagonal [h : DecidableEq α] (x : α × α) : Decidable (x ∈ diagonal α) := h x.1 x.2 -theorem preimage_coe_coe_diagonal (s : Set α) : - Prod.map (fun x : s => (x : α)) (fun x : s => (x : α)) ⁻¹' diagonal α = diagonal s := by - ext ⟨⟨x, hx⟩, ⟨y, hy⟩⟩ - simp [Set.diagonal] +theorem preimage_val_val_diagonal (s : Set α) : + Prod.map Subtype.val Subtype.val ⁻¹' diagonal α = diagonal s := Set.ext <| by simp -@[simp] -theorem range_diag : (range fun x => (x, x)) = diagonal α := by - ext ⟨x, y⟩ - simp [diagonal, eq_comm] +@[deprecated (since := "2026-04-04")] +alias preimage_coe_coe_diagonal := preimage_val_val_diagonal -theorem diagonal_subset_iff {s} : diagonal α ⊆ s ↔ ∀ x, (x, x) ∈ s := by - rw [← range_diag, range_subset_iff] +theorem diagonal_subset_iff {s} : diagonal α ⊆ s ↔ ∀ x, ⇗x ∈ s := by + simp_rw [← range_diag, range_subset_iff] @[simp] theorem prod_subset_compl_diagonal_iff_disjoint : s ×ˢ t ⊆ (diagonal α)ᶜ ↔ Disjoint s t := prod_subset_iff.trans disjoint_iff_forall_ne.symm @[simp] -theorem diag_preimage_prod (s t : Set α) : (fun x => (x, x)) ⁻¹' s ×ˢ t = s ∩ t := +theorem diag_preimage_prod (s t : Set α) : Function.diag ⁻¹' s ×ˢ t = s ∩ t := rfl -theorem diag_preimage_prod_self (s : Set α) : (fun x => (x, x)) ⁻¹' s ×ˢ s = s := +theorem diag_preimage_prod_self (s : Set α) : Function.diag ⁻¹' s ×ˢ s = s := inter_self s -theorem diag_image (s : Set α) : (fun x => (x, x)) '' s = diagonal α ∩ s ×ˢ s := by +theorem diag_image (s : Set α) : Function.diag '' s = diagonal α ∩ s ×ˢ s := by rw [← range_diag, ← image_preimage_eq_range_inter, diag_preimage_prod_self] theorem diagonal_eq_univ_iff : diagonal α = univ ↔ Subsingleton α := by @@ -927,7 +926,8 @@ variable {α β γ δ : Type*} {s : Set α} {f : α → β} section graphOn variable {x : α × β} -@[simp] lemma mem_graphOn : x ∈ s.graphOn f ↔ x.1 ∈ s ∧ f x.1 = x.2 := by aesop (add simp graphOn) +@[simp] lemma mem_graphOn : x ∈ s.graphOn f ↔ x.1 ∈ s ∧ f x.1 = x.2 := by + simp [graphOn, Prod.ext_iff] @[simp] lemma graphOn_empty (f : α → β) : graphOn f ∅ = ∅ := image_empty _ @[simp] lemma graphOn_eq_empty : graphOn f s = ∅ ↔ s = ∅ := image_eq_empty @@ -957,8 +957,12 @@ lemma image_fst_graphOn (f : α → β) (s : Set α) : Prod.fst '' graphOn f s = lemma fst_injOn_graph : (s.graphOn f).InjOn Prod.fst := by aesop (add simp InjOn) lemma graphOn_comp (s : Set α) (f : α → β) (g : β → γ) : - s.graphOn (g ∘ f) = (fun x ↦ (x.1, g x.2)) '' s.graphOn f := by - simpa using image_comp (fun x ↦ (x.1, g x.2)) (fun x ↦ (x, f x)) _ + s.graphOn (g ∘ f) = Prod.map id g '' s.graphOn f := by + simpa using image_comp (Prod.map id g) (id ⇊ f) _ + +lemma graphOn_prod (s : Set α) (f : α → β) (g : α → γ) : + s.graphOn (f ⇊ g) = {x | x.1 ∈ s ∧ f x.1 = x.2.1 ∧ g x.1 = x.2.2} := by + simp [graphOn, Set.ext_iff, Prod.ext_iff] lemma graphOn_univ_eq_range : univ.graphOn f = range fun x ↦ (x, f x) := image_univ @@ -967,11 +971,11 @@ lemma graphOn_univ_eq_range : univ.graphOn f = range fun x ↦ (x, f x) := image lemma graphOn_prod_graphOn (s : Set α) (t : Set β) (f : α → γ) (g : β → δ) : s.graphOn f ×ˢ t.graphOn g = Equiv.prodProdProdComm .. ⁻¹' (s ×ˢ t).graphOn (Prod.map f g) := by - aesop + simp [Set.ext_iff, Prod.ext_iff, and_and_and_comm] lemma graphOn_prod_prodMap (s : Set α) (t : Set β) (f : α → γ) (g : β → δ) : (s ×ˢ t).graphOn (Prod.map f g) = Equiv.prodProdProdComm .. ⁻¹' s.graphOn f ×ˢ t.graphOn g := by - aesop + simp [Set.ext_iff, Prod.ext_iff, and_and_and_comm] end graphOn diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean index 512aa33acab367..6b9031712231c5 100644 --- a/Mathlib/Data/Tree/Basic.lean +++ b/Mathlib/Data/Tree/Basic.lean @@ -16,7 +16,7 @@ See also `Lean.Data.RBTree` for red-black trees - this version allows more opera to be defined and is better suited for in-kernel computation. We also specialize for `Tree Unit`, which is a binary tree without any -additional data. We provide the notation `a △ b` for making a `Tree Unit` with children +additional data. We provide the notation `a ⇊ b` for making a `Tree Unit` with children `a` and `b`. ## References diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean b/Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean index fe13581917f544..6a50d3b928651b 100644 --- a/Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean +++ b/Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean @@ -55,39 +55,39 @@ section ProdMk theorem ContMDiffWithinAt.prodMk {f : M → M'} {g : M → N'} (hf : ContMDiffWithinAt I I' n f s x) (hg : ContMDiffWithinAt I J' n g s x) : - ContMDiffWithinAt I (I'.prod J') n (fun x => (f x, g x)) s x := by + ContMDiffWithinAt I (I'.prod J') n (Function.prod f g) s x := by rw [contMDiffWithinAt_iff] at * exact ⟨hf.1.prodMk hg.1, hf.2.prodMk hg.2⟩ theorem ContMDiffWithinAt.prodMk_space {f : M → E'} {g : M → F'} (hf : ContMDiffWithinAt I 𝓘(𝕜, E') n f s x) (hg : ContMDiffWithinAt I 𝓘(𝕜, F') n g s x) : - ContMDiffWithinAt I 𝓘(𝕜, E' × F') n (fun x => (f x, g x)) s x := by + ContMDiffWithinAt I 𝓘(𝕜, E' × F') n (Function.prod f g) s x := by rw [contMDiffWithinAt_iff] at * exact ⟨hf.1.prodMk hg.1, hf.2.prodMk hg.2⟩ nonrec theorem ContMDiffAt.prodMk {f : M → M'} {g : M → N'} (hf : ContMDiffAt I I' n f x) - (hg : ContMDiffAt I J' n g x) : ContMDiffAt I (I'.prod J') n (fun x => (f x, g x)) x := + (hg : ContMDiffAt I J' n g x) : ContMDiffAt I (I'.prod J') n (Function.prod f g) x := hf.prodMk hg nonrec theorem ContMDiffAt.prodMk_space {f : M → E'} {g : M → F'} (hf : ContMDiffAt I 𝓘(𝕜, E') n f x) (hg : ContMDiffAt I 𝓘(𝕜, F') n g x) : - ContMDiffAt I 𝓘(𝕜, E' × F') n (fun x => (f x, g x)) x := + ContMDiffAt I 𝓘(𝕜, E' × F') n (Function.prod f g) x := hf.prodMk_space hg theorem ContMDiffOn.prodMk {f : M → M'} {g : M → N'} (hf : ContMDiffOn I I' n f s) - (hg : ContMDiffOn I J' n g s) : ContMDiffOn I (I'.prod J') n (fun x => (f x, g x)) s := + (hg : ContMDiffOn I J' n g s) : ContMDiffOn I (I'.prod J') n (Function.prod f g) s := fun x hx => (hf x hx).prodMk (hg x hx) theorem ContMDiffOn.prodMk_space {f : M → E'} {g : M → F'} (hf : ContMDiffOn I 𝓘(𝕜, E') n f s) - (hg : ContMDiffOn I 𝓘(𝕜, F') n g s) : ContMDiffOn I 𝓘(𝕜, E' × F') n (fun x => (f x, g x)) s := + (hg : ContMDiffOn I 𝓘(𝕜, F') n g s) : ContMDiffOn I 𝓘(𝕜, E' × F') n (Function.prod f g) s := fun x hx => (hf x hx).prodMk_space (hg x hx) nonrec theorem ContMDiff.prodMk {f : M → M'} {g : M → N'} (hf : ContMDiff I I' n f) - (hg : ContMDiff I J' n g) : ContMDiff I (I'.prod J') n fun x => (f x, g x) := fun x => + (hg : ContMDiff I J' n g) : ContMDiff I (I'.prod J') n Function.prod f g := fun x => (hf x).prodMk (hg x) theorem ContMDiff.prodMk_space {f : M → E'} {g : M → F'} (hf : ContMDiff I 𝓘(𝕜, E') n f) - (hg : ContMDiff I 𝓘(𝕜, F') n g) : ContMDiff I 𝓘(𝕜, E' × F') n fun x => (f x, g x) := fun x => + (hg : ContMDiff I 𝓘(𝕜, F') n g) : ContMDiff I 𝓘(𝕜, E' × F') n Function.prod f g := fun x => (hf x).prodMk_space (hg x) end ProdMk @@ -224,15 +224,15 @@ theorem contMDiff_prod_assoc : theorem ContMDiffWithinAt.comp₂ {h : M' × N' → N} {f : M → M'} {g : M → N'} {x : M} {t : Set (M' × N')} (ha : ContMDiffWithinAt (I'.prod J') J n h t (f x, g x)) (fa : ContMDiffWithinAt I I' n f s x) (ga : ContMDiffWithinAt I J' n g s x) - (st : MapsTo (fun x ↦ (f x, g x)) s t) : + (st : MapsTo (f ⇊ g) s t) : ContMDiffWithinAt I J n (fun x ↦ h (f x, g x)) s x := - ha.comp (f := fun x ↦ (f x, g x)) _ (fa.prodMk ga) st + ha.comp (f := f ⇊ g) _ (fa.prodMk ga) st /-- `ContMDiffWithinAt.comp₂`, with a separate argument for point equality. -/ theorem ContMDiffWithinAt.comp₂_of_eq {h : M' × N' → N} {f : M → M'} {g : M → N'} {x : M} {y : M' × N'} {t : Set (M' × N')} (ha : ContMDiffWithinAt (I'.prod J') J n h t y) (fa : ContMDiffWithinAt I I' n f s x) (ga : ContMDiffWithinAt I J' n g s x) - (e : (f x, g x) = y) (st : MapsTo (fun x ↦ (f x, g x)) s t) : + (e : (f x, g x) = y) (st : MapsTo (f ⇊ g) s t) : ContMDiffWithinAt I J n (fun x ↦ h (f x, g x)) s x := by rw [← e] at ha exact ha.comp₂ fa ga st @@ -241,7 +241,7 @@ theorem ContMDiffWithinAt.comp₂_of_eq {h : M' × N' → N} {f : M → M'} {g : theorem ContMDiffAt.comp₂ {h : M' × N' → N} {f : M → M'} {g : M → N'} {x : M} (ha : ContMDiffAt (I'.prod J') J n h (f x, g x)) (fa : ContMDiffAt I I' n f x) (ga : ContMDiffAt I J' n g x) : ContMDiffAt I J n (fun x ↦ h (f x, g x)) x := - ha.comp (f := fun x ↦ (f x, g x)) _ (fa.prodMk ga) + ha.comp (f := f ⇊ g) _ (fa.prodMk ga) /-- `ContMDiffAt.comp₂`, with a separate argument for point equality. -/ theorem ContMDiffAt.comp₂_of_eq {h : M' × N' → N} {f : M → M'} {g : M → N'} {x : M} {y : M' × N'} diff --git a/Mathlib/Geometry/Manifold/ContMDiffMap.lean b/Mathlib/Geometry/Manifold/ContMDiffMap.lean index e0fce000c3f725..72b84928317824 100644 --- a/Mathlib/Geometry/Manifold/ContMDiffMap.lean +++ b/Mathlib/Geometry/Manifold/ContMDiffMap.lean @@ -106,7 +106,7 @@ def snd : C^n⟮I.prod I', M × M'; I', M'⟯ := /-- Given two `C^n` maps `f` and `g`, this is the `C^n` map `x ↦ (f x, g x)`. -/ def prodMk (f : C^n⟮J, N; I, M⟯) (g : C^n⟮J, N; I', M'⟯) : C^n⟮J, N; I.prod I', M × M'⟯ := - ⟨fun x => (f x, g x), f.2.prodMk g.2⟩ + ⟨Function.prod f g, f.2.prodMk g.2⟩ end ContMDiffMap diff --git a/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean b/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean index 19a57d0c91d8d5..6f7939142d1ca2 100644 --- a/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean +++ b/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean @@ -215,7 +215,7 @@ section Prod theorem MDifferentiableWithinAt.prodMk {f : M → M'} {g : M → M''} (hf : MDiffAt[s] f x) (hg : MDiffAt[s] g x) : - MDiffAt[s] (fun x ↦ (f x, g x)) x := + MDiffAt[s] (f ⇊ g) x := ⟨hf.1.prodMk hg.1, hf.2.prodMk hg.2⟩ /-- If `f` and `g` have derivatives `df` and `dg` within `s` at `x`, respectively, @@ -228,17 +228,17 @@ theorem HasMFDerivWithinAt.prodMk {f : M → M'} {g : M → M''} lemma mfderivWithin_prodMk {f : M → M'} {g : M → M''} (hf : MDiffAt[s] f x) (hg : MDiffAt[s] g x) (hs : UniqueMDiffWithinAt I s x) : - mfderiv[s] (fun x ↦ (f x, g x)) x = (mfderiv[s] f x).prod (mfderiv[s] g x) := + mfderiv[s] (f ⇊ g) x = (mfderiv[s] f x).prod (mfderiv[s] g x) := (hf.hasMFDerivWithinAt.prodMk hg.hasMFDerivWithinAt).mfderivWithin hs lemma mfderiv_prodMk {f : M → M'} {g : M → M''} (hf : MDiffAt f x) (hg : MDiffAt g x) : - mfderiv% (fun x ↦ (f x, g x)) x = (mfderiv% f x).prod (mfderiv% g x) := by + mfderiv% (f ⇊ g) x = (mfderiv% f x).prod (mfderiv% g x) := by simp_rw [← mfderivWithin_univ] exact mfderivWithin_prodMk hf.mdifferentiableWithinAt hg.mdifferentiableWithinAt (uniqueMDiffWithinAt_univ I) theorem MDifferentiableAt.prodMk {f : M → M'} {g : M → M''} (hf : MDiffAt f x) (hg : MDiffAt g x) : - MDiffAt (fun x ↦ (f x, g x)) x := + MDiffAt (f ⇊ g) x := ⟨hf.1.prodMk hg.1, hf.2.prodMk hg.2⟩ /-- If `f` and `g` have derivatives `df` and `dg` at `x`, respectively, @@ -251,27 +251,27 @@ theorem HasMFDerivAt.prodMk {f : M → M'} {g : M → M''} theorem MDifferentiableWithinAt.prodMk_space {f : M → E'} {g : M → E''} (hf : MDiffAt[s] f x) (hg : MDiffAt[s] g x) : - MDifferentiableWithinAt I 𝓘(𝕜, E' × E'') (fun x ↦ (f x, g x)) s x := + MDifferentiableWithinAt I 𝓘(𝕜, E' × E'') (f ⇊ g) s x := ⟨hf.1.prodMk hg.1, hf.2.prodMk hg.2⟩ theorem MDifferentiableAt.prodMk_space {f : M → E'} {g : M → E''} (hf : MDiffAt f x) (hg : MDiffAt g x) : - MDifferentiableAt I 𝓘(𝕜, E' × E'') (fun x ↦ (f x, g x)) x := + MDifferentiableAt I 𝓘(𝕜, E' × E'') (f ⇊ g) x := ⟨hf.1.prodMk hg.1, hf.2.prodMk hg.2⟩ theorem MDifferentiableOn.prodMk {f : M → M'} {g : M → M''} (hf : MDiff[s] f) (hg : MDiff[s] g) : - MDiff[s] (fun x ↦ (f x, g x)) := fun x hx ↦ (hf x hx).prodMk (hg x hx) + MDiff[s] (f ⇊ g) := fun x hx ↦ (hf x hx).prodMk (hg x hx) theorem MDifferentiable.prodMk {f : M → M'} {g : M → M''} (hf : MDiff f) (hg : MDiff g) : - MDiff fun x ↦ (f x, g x) := fun x ↦ (hf x).prodMk (hg x) + MDiff f ⇊ g := fun x ↦ (hf x).prodMk (hg x) theorem MDifferentiableOn.prodMk_space {f : M → E'} {g : M → E''} (hf : MDiff[s] f) (hg : MDiff[s] g) : - MDifferentiableOn I 𝓘(𝕜, E' × E'') (fun x ↦ (f x, g x)) s := + MDifferentiableOn I 𝓘(𝕜, E' × E'') (f ⇊ g) s := fun x hx ↦ (hf x hx).prodMk_space (hg x hx) theorem MDifferentiable.prodMk_space {f : M → E'} {g : M → E''} (hf : MDiff f) (hg : MDiff g) : - MDifferentiable I 𝓘(𝕜, E' × E'') fun x ↦ (f x, g x) := + MDifferentiable I 𝓘(𝕜, E' × E'') f ⇊ g := fun x ↦ (hf x).prodMk_space (hg x) theorem hasMFDerivAt_fst (x : M × M') : diff --git a/Mathlib/LinearAlgebra/Prod.lean b/Mathlib/LinearAlgebra/Prod.lean index 6416808409864e..69728fde258738 100644 --- a/Mathlib/LinearAlgebra/Prod.lean +++ b/Mathlib/LinearAlgebra/Prod.lean @@ -93,11 +93,11 @@ theorem snd_surjective : Function.Surjective (snd R M M₂) := fun x => ⟨(0, x /-- The prod of two linear maps is a linear map. -/ @[simps] def prod (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : M →ₗ[R] M₂ × M₃ where - toFun := Pi.prod f g - map_add' x y := by simp only [Pi.prod, Prod.mk_add_mk, map_add] - map_smul' c x := by simp only [Pi.prod, Prod.smul_mk, map_smul, RingHom.id_apply] + toFun := Function.prod f g + map_add' x y := by simp only [Pi.prod_apply, Prod.mk_add_mk, map_add] + map_smul' c x := by simp only [Pi.prod_apply, Prod.smul_mk, map_smul, RingHom.id_apply] -theorem coe_prod (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : ⇑(f.prod g) = Pi.prod f g := +theorem coe_prod (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : ⇑(f.prod g) = Function.prod f g := rfl @[simp] diff --git a/Mathlib/Logic/Equiv/Basic.lean b/Mathlib/Logic/Equiv/Basic.lean index fbc5193ae2dbab..15ee48832a7e6e 100644 --- a/Mathlib/Logic/Equiv/Basic.lean +++ b/Mathlib/Logic/Equiv/Basic.lean @@ -876,12 +876,11 @@ lemma piCongrLeft_apply_eq_cast {P : β → Sort v} {e : α ≃ β} theorem piCongrLeft_sumInl {ι ι' ι''} (π : ι'' → Type*) (e : ι ⊕ ι' ≃ ι'') (f : ∀ i, π (e (inl i))) (g : ∀ i, π (e (inr i))) (i : ι) : piCongrLeft π e (sumPiEquivProdPi (fun x => π (e x)) |>.symm (f, g)) (e (inl i)) = f i := by - grind - + simp theorem piCongrLeft_sumInr {ι ι' ι''} (π : ι'' → Type*) (e : ι ⊕ ι' ≃ ι'') (f : ∀ i, π (e (inl i))) (g : ∀ i, π (e (inr i))) (j : ι') : piCongrLeft π e (sumPiEquivProdPi (fun x => π (e x)) |>.symm (f, g)) (e (inr j)) = g j := by - grind + simp end diff --git a/Mathlib/Logic/Equiv/Prod.lean b/Mathlib/Logic/Equiv/Prod.lean index b5fceded97edfb..2bce1b4ed2a14e 100644 --- a/Mathlib/Logic/Equiv/Prod.lean +++ b/Mathlib/Logic/Equiv/Prod.lean @@ -7,6 +7,7 @@ module public import Mathlib.Logic.Equiv.Defs public import Mathlib.Tactic.Contrapose +public import Mathlib.Logic.Function.Init /-! # Equivalence between product types @@ -96,17 +97,19 @@ theorem prodComm_apply {α β} (x : α × β) : prodComm α β x = x.swap := theorem prodComm_symm (α β) : (prodComm α β).symm = prodComm β α := rfl +open Prod in /-- Type product is associative up to an equivalence. -/ @[simps (attr := grind =)] -def prodAssoc (α β γ) : (α × β) × γ ≃ α × β × γ := - ⟨fun p => (p.1.1, p.1.2, p.2), fun p => ((p.1, p.2.1), p.2.2), fun ⟨⟨_, _⟩, _⟩ => rfl, - fun ⟨_, ⟨_, _⟩⟩ => rfl⟩ +def prodAssoc (α β γ) : (α × β) × γ ≃ α × β × γ where + toFun := (fst ∘ fst) ⇊ ((snd ∘ fst) ⇊ snd) + invFun := (fst ⇊ (fst ∘ snd)) ⇊ (snd ∘ snd) +open Prod in /-- Four-way commutativity of `prod`. The name matches `mul_mul_mul_comm`. -/ @[simps (attr := grind =) apply] def prodProdProdComm (α β γ δ) : (α × β) × γ × δ ≃ (α × γ) × β × δ where - toFun abcd := ((abcd.1.1, abcd.2.1), (abcd.1.2, abcd.2.2)) - invFun acbd := ((acbd.1.1, acbd.2.1), (acbd.1.2, acbd.2.2)) + toFun := ((fst ∘ fst) ⇊ (fst ∘ snd)) ⇊ ((snd ∘ fst) ⇊ (snd ∘ snd)) + invFun := ((fst ∘ fst) ⇊ (fst ∘ snd)) ⇊ ((snd ∘ fst) ⇊ (snd ∘ snd)) @[simp, grind =] theorem prodProdProdComm_symm (α β γ δ) : @@ -117,17 +120,15 @@ theorem prodProdProdComm_symm (α β γ δ) : @[simps (attr := grind =) -fullyApplied] def curry (α β γ) : (α × β → γ) ≃ (α → β → γ) where toFun := Function.curry - invFun := uncurry - left_inv := uncurry_curry - right_inv := curry_uncurry + invFun := Function.uncurry section /-- `PUnit` is a right identity for type product up to an equivalence. -/ @[simps (attr := grind =)] def prodPUnit (α) : α × PUnit ≃ α where - toFun := fun p => p.1 - invFun := fun a => (a, PUnit.unit) + toFun := Prod.fst + invFun := id ⇊ Function.const α () /-- `PUnit` is a left identity for type product up to an equivalence. -/ @[simps! (attr := grind =)] @@ -139,7 +140,7 @@ def punitProd (α) : PUnit × α ≃ α := /-- `PUnit` is a right identity for dependent type product up to an equivalence. -/ @[simps (attr := grind =)] def sigmaPUnit (α) : (_ : α) × PUnit ≃ α where - toFun := fun p => p.1 + toFun := Sigma.fst invFun := fun a => ⟨a, PUnit.unit⟩ /-- Any `Unique` type is a right identity for type product up to equivalence. -/ @@ -338,56 +339,61 @@ section /-- The type of functions to a product `β × γ` is equivalent to the type of pairs of functions `α → β` and `β → γ`. -/ -@[simps] -def arrowProdEquivProdArrow (α : Type*) (β γ : α → Type*) : - ((i : α) → β i × γ i) ≃ ((i : α) → β i) × ((i : α) → γ i) where - toFun := fun f => (fun c => (f c).1, fun c => (f c).2) - invFun := fun p c => (p.1 c, p.2 c) +@[simps! (attr := grind =)] +def arrowProdEquivProdArrow (α β γ : Type*) : (α → β × γ) ≃ (α → β) × (α → γ) where + toFun := Function.prod (Prod.fst <| · ·) (Prod.snd <| · ·) + invFun := Function.prod.uncurry + +/-- The type of a pi-type indexed by `i : ι` to products `β i × γ i` is equivalent to product of two +pi-types `∀ i, β i` and `∀ i, γ i`. This is a dependent version of +`Equiv.arrowProdEquivProdArrow`. -/ +@[simps! (attr := grind =)] +def piProdEquivProdPi (α : Type*) (β γ : α → Type*) : + (∀ i, β i × γ i) ≃ (∀ i, β i) × (∀ i, γ i) where + toFun := Function.prod (Prod.fst <| · ·) (Prod.snd <| · ·) + invFun := Pi.prod.uncurry open Sum +/-- The type of functions on a sum type `α ⊕ β` is equivalent to the type of pairs of functions +on `α` and on `β`. -/ +@[simps! (attr := grind =)] +def sumArrowEquivProdArrow (α β γ : Type*) : (α ⊕ β → γ) ≃ (α → γ) × (β → γ) where + toFun := Function.prod (· <| inl ·) (· <| inr ·) + invFun := Sum.elim.uncurry + left_inv f := by ext (i | i) <;> rfl + +@[deprecated sumArrowEquivProdArrow_symm_apply (since := "2026-04-03")] +theorem sumArrowEquivProdArrow_symm_apply_inl {α β γ} (f : α → γ) (g : β → γ) (a : α) : + ((sumArrowEquivProdArrow α β γ).symm (f, g)) (inl a) = f a := by + apply sumArrowEquivProdArrow_symm_apply + +@[deprecated sumArrowEquivProdArrow_symm_apply (since := "2026-04-03")] +theorem sumArrowEquivProdArrow_symm_apply_inr {α β γ} (f : α → γ) (g : β → γ) (b : β) : + ((sumArrowEquivProdArrow α β γ).symm (f, g)) (inr b) = g b := by + apply sumArrowEquivProdArrow_symm_apply + /-- The type of dependent functions on a sum type `ι ⊕ ι'` is equivalent to the type of pairs of functions on `ι` and on `ι'`. This is a dependent version of `Equiv.sumArrowEquivProdArrow`. -/ @[simps (attr := grind =)] def sumPiEquivProdPi {ι ι'} (π : ι ⊕ ι' → Type*) : (∀ i, π i) ≃ (∀ i, π (inl i)) × ∀ i', π (inr i') where - toFun f := ⟨fun i => f (inl i), fun i' => f (inr i')⟩ - invFun g := Sum.rec g.1 g.2 + toFun := Function.prod (· <| inl ·) (· <| inr ·) + invFun := Sum.rec.uncurry left_inv f := by ext (i | i) <;> rfl /-- The equivalence between a product of two dependent functions types and a single dependent function type. Basically a symmetric version of `Equiv.sumPiEquivProdPi`. -/ @[simps! (attr := grind =)] def prodPiEquivSumPi {ι ι'} (π : ι → Type u) (π' : ι' → Type u) : - ((∀ i, π i) × ∀ i', π' i') ≃ ∀ i, Sum.elim π π' i := + ((∀ i, π i) × ∀ i', π' i') ≃ ∀ i : ι ⊕ ι', i.elim π π' := sumPiEquivProdPi (Sum.elim π π') |>.symm -/-- The type of functions on a sum type `α ⊕ β` is equivalent to the type of pairs of functions -on `α` and on `β`. -/ -def sumArrowEquivProdArrow (α β γ : Type*) : (α ⊕ β → γ) ≃ (α → γ) × (β → γ) := - ⟨fun f => (f ∘ inl, f ∘ inr), fun p => Sum.elim p.1 p.2, fun f => by ext ⟨⟩ <;> rfl, fun p => by - cases p - rfl⟩ - -@[simp, grind =] -theorem sumArrowEquivProdArrow_apply_fst {α β γ} (f : α ⊕ β → γ) (a : α) : - (sumArrowEquivProdArrow α β γ f).1 a = f (inl a) := - rfl - -@[simp, grind =] -theorem sumArrowEquivProdArrow_apply_snd {α β γ} (f : α ⊕ β → γ) (b : β) : - (sumArrowEquivProdArrow α β γ f).2 b = f (inr b) := - rfl - -@[simp, grind =] -theorem sumArrowEquivProdArrow_symm_apply_inl {α β γ} (f : α → γ) (g : β → γ) (a : α) : - ((sumArrowEquivProdArrow α β γ).symm (f, g)) (inl a) = f a := - rfl - -@[simp, grind =] -theorem sumArrowEquivProdArrow_symm_apply_inr {α β γ} (f : α → γ) (g : β → γ) (b : β) : - ((sumArrowEquivProdArrow α β γ).symm (f, g)) (inr b) = g b := - rfl +/-- The equivalence between a pi-type indexed by `i : ι` to products `β i × γ i` +and a pi-type indexed by `α ⊕ α`. -/ +def piProdEquivSumPi (α : Type*) (β γ : α → Type u) : + (∀ i, β i × γ i) ≃ ∀ i : α ⊕ α, i.elim β γ := + (piProdEquivProdPi _ _ _).trans (prodPiEquivSumPi _ _) /-- Type product is right distributive with respect to type sum up to an equivalence. -/ def sumProdDistrib (α β γ) : (α ⊕ β) × γ ≃ α × γ ⊕ β × γ := @@ -423,18 +429,18 @@ def sigmaProdDistrib {ι : Type*} (α : ι → Type*) (β : Type*) : (Σ i, α i /-- The product `Bool × α` is equivalent to `α ⊕ α`. -/ @[simps (attr := grind =)] -def boolProdEquivSum (α) : Bool × α ≃ α ⊕ α where - toFun p := if p.1 then (inr p.2) else (inl p.2) - invFun := Sum.elim (Prod.mk false) (Prod.mk true) - left_inv := by rintro ⟨_ | _, _⟩ <;> rfl - right_inv := by rintro (_ | _) <;> rfl +def boolProdEquivSum (α : Type*) : Bool × α ≃ α ⊕ α where + toFun := (cond · inr inl).uncurry + invFun := Function.prod Sum.isRight (Sum.elim id id) + left_inv := by grind + right_inv := by grind /-- The function type `Bool → α` is equivalent to `α × α`. -/ @[simps (attr := grind =)] def boolArrowEquivProd (α : Type*) : (Bool → α) ≃ α × α where - toFun f := (f false, f true) - invFun p b := if b then p.2 else p.1 - left_inv _ := by grind + toFun := Function.prod (· false) (· true) + invFun := flip (cond · Prod.snd Prod.fst ·) + left_inv _ := by grind [flip] end diff --git a/Mathlib/Logic/Function/Basic.lean b/Mathlib/Logic/Function/Basic.lean index 44534ad0ffc944..06428a1d7597ee 100644 --- a/Mathlib/Logic/Function/Basic.lean +++ b/Mathlib/Logic/Function/Basic.lean @@ -830,6 +830,8 @@ section CurryAndUncurry theorem uncurry_def {α β γ} (f : α → β → γ) : uncurry f = fun p ↦ f p.1 p.2 := rfl +@[simp] theorem uncurry_apply {α β γ} (f : α → β → γ) (p : α × β) : uncurry f p = f p.1 p.2 := rfl + theorem uncurry_injective {α β γ} : Function.Injective (uncurry : (α → β → γ) → _) := LeftInverse.injective curry_uncurry diff --git a/Mathlib/Logic/Function/Init.lean b/Mathlib/Logic/Function/Init.lean new file mode 100644 index 00000000000000..b10bfb4442d606 --- /dev/null +++ b/Mathlib/Logic/Function/Init.lean @@ -0,0 +1,180 @@ +/- +Copyright (c) 2026 Wrenna Robson. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Wrenna Robson +-/ +module + +public import Mathlib.Init + +/-! + +This file defines `(f ⇊ g)`, the operation that pairs two functions `f : ι → α` and +`g : ι → β` into a function `ι → α × β`. + +It also defines the special case when `f = g = id`, `Function.diag`. This is the canonical injection +of a type into its prouduct with itself onto its diagonal. + + +This file should not depend on anything defined in Mathlib (except for notation), so that it can be +upstreamed to Batteries or the Lean standard library easily. + +-/ + +@[expose] public section + +namespace Pi + +/-- The mapping into a product type built from maps into each component. -/ +protected def prod {ι} {α β : ι → Type*} (f : ∀ i, α i) (g : ∀ i, β i) (i : ι) : α i × β i := + Prod.mk (f i) (g i) + +@[inherit_doc] infixr:65 " ⇊' " => Pi.prod + +section + +variable {ι} {α β : ι → Type*} (f f' : ∀ i, α i) (g g' : ∀ i, β i) {c} + +@[grind =] theorem prod_apply : (f ⇊' g) c = (f c, g c) := rfl + +@[simp] theorem fst_prod : ((f ⇊' g) c).fst = f c := rfl +@[simp] theorem snd_prod : ((f ⇊' g) c).snd = g c := rfl + +@[simp] theorem prod_fst_snd {α β} : (Prod.fst : _ → α) ⇊' (Prod.snd : _ → β) = id := rfl +@[simp] theorem prod_snd_fst {α β} : (Prod.snd : _ → β) ⇊' (Prod.fst : _ → α) = .swap := rfl + +theorem prod_fst_snd_comp {h : ∀ i, α i × β i} : + (Prod.fst <| h ·) ⇊' (Prod.snd <| h ·) = h := rfl + +theorem fst_comp_prod {f : ∀ i, α i} {g : ∀ i, β i} : (Prod.fst <| (f ⇊' g) ·) = f := rfl +theorem snd_comp_prod {f : ∀ i, α i} {g : ∀ i, β i} : (Prod.snd <| (f ⇊' g) ·) = g := rfl + +@[simp] +theorem prod_eq_iff {f : ∀ i, α i} {g : ∀ i, β i} : + f ⇊' g = f' ⇊' g' ↔ f = f' ∧ g = g' := by simp [funext_iff, Prod.ext_iff, forall_and] + +theorem prod_ext_iff {h h' : ∀ i, α i × β i} : h = h' ↔ + (Prod.fst <| h ·) = (Prod.fst <| h' ·) ∧ (Prod.snd <| h ·) = (Prod.snd <| h' ·) := by + simp [funext_iff, Prod.ext_iff, forall_and] + +theorem exists_prod_apply_eq (h : ∀ i, α i × β i) : ∃ f g, (f ⇊' g) = h := + ⟨(Prod.fst <| h ·), (Prod.snd <| h ·), prod_fst_snd_comp⟩ + +theorem exists_fst_comp (f : ∀ i, α i) (g : ∀ i, β i) : + ∃ h : ∀ i, α i × β i, (Prod.fst <| h ·) = f := ⟨(f ⇊' g), fst_comp_prod⟩ +theorem exists_snd_comp (f : ∀ i, α i) (g : ∀ i, β i) : + ∃ h : ∀ i, α i × β i, (Prod.snd <| h ·) = g := ⟨(f ⇊' g), snd_comp_prod⟩ + +@[grind =] +theorem prod_const_const {ι} {α β} {a : α} {b : β} : + (Function.const ι a) ⇊' (Function.const ι b) = Function.const ι (a, b) := rfl + +end + +end Pi + +namespace Function + +variable {α β γ δ : Type*} {ι : Sort*} + +/-- This is the pairing operation on functions, dual to `Sum.elim`. -/ +protected def prod : (ι → α) → (ι → β) → ι → α × β := (· ⇊' ·) + +@[inherit_doc] infixr:65 " ⇊ " => Function.prod + +section + +variable (f : ι → α) (g : ι → β) + +@[grind =] theorem prod_apply (c : ι) : (f.prod g) c = (f c, g c) := rfl + +theorem prod_comp {γ} {h : γ → ι} : (f ⇊ g) ∘ h = (f ∘ h) ⇊ (g ∘ h) := rfl + +@[simp] theorem fst_prod {c} : ((f ⇊ g) c).fst = f c := rfl +@[simp] theorem snd_prod {c} : ((f ⇊ g) c).snd = g c := rfl + +@[simp] theorem prod_fst_snd : Prod.fst (α := α) ⇊ Prod.snd (β := β) = id := rfl +@[simp] theorem prod_snd_fst : Prod.snd (β := β) ⇊ Prod.fst (α := α) = .swap := rfl + +@[simp] theorem prod_fst_snd_comp {f : ι → α × β} : (Prod.fst ∘ f) ⇊ (Prod.snd ∘ f) = f := rfl + +@[simp] theorem fst_comp_prod {f : ι → α} {g : ι → β} : Prod.fst ∘ (f ⇊ g) = f := rfl +@[simp] theorem snd_comp_prod {f : ι → α} {g : ι → β} : Prod.snd ∘ (f ⇊ g) = g := rfl + +theorem prod_eq_iff {f f' : ι → α} {g g' : ι → β} : f ⇊ g = f' ⇊ g' ↔ + f = f' ∧ g = g' := by simp [funext_iff, Prod.ext_iff, forall_and] + +theorem prod_ext_iff {h h' : ι → α × β} : h = h' ↔ + Prod.fst ∘ h = Prod.fst ∘ h' ∧ Prod.snd ∘ h = (Prod.snd ∘ h') := by + simp [funext_iff, Prod.ext_iff, forall_and] + +theorem exists_prod_apply_eq (h : ι → α × β) : ∃ f g, f ⇊ g = h := + ⟨Prod.fst ∘ h, Prod.snd ∘ h, prod_fst_snd_comp⟩ + +theorem exists_fst_comp (f : ι → α) (g : ι → β) : + ∃ h : ι → α × β, Prod.fst ∘ h = f := ⟨f ⇊ g, fst_comp_prod⟩ +theorem exists_snd_comp (f : ι → α) (g : ι → β) : + ∃ h : ι → α × β, Prod.snd ∘ h = g := ⟨f ⇊ g, snd_comp_prod⟩ + +theorem leftInverse_uncurry_prod_prod_fst_comp_snd_comp : Function.LeftInverse + (Function.prod (ι := γ)).uncurry ((Prod.fst (α := α) ∘ ·) ⇊ (Prod.snd (β := β) ∘ ·)) := + fun _ => rfl + +theorem rightInverse_uncurry_prod_prod_fst_comp_snd_comp : Function.RightInverse + (Function.prod (ι := γ)).uncurry ((Prod.fst (α := α) ∘ ·) ⇊ (Prod.snd (β := β) ∘ ·)) := + fun _ => rfl + +@[grind =] +theorem prod_const_const (a : α) (b : β) : + (Function.const ι a) ⇊ (Function.const ι b) = Function.const ι (a, b) := rfl + +theorem const_prod {ι} {α β} {p : α × β} : + Function.const ι p = (Function.const ι p.1) ⇊ (Function.const ι p.2) := rfl + +end + +/-- `Function.prodMap` is `Prod.map` in the `Function` namespace. -/ +def prodMap (f : α → β) (g : γ → δ) := (f ∘ Prod.fst) ⇊ (g ∘ Prod.snd) + +@[simp, grind =] +theorem prodMap_eq_prod_map {f : α → β} {g : γ → δ} : f.prodMap g = Prod.map f g := rfl + +@[grind _=_] +theorem map_prod {f : α → β} {g : ι → α} {h : γ → δ} {k : ι → γ} {c} : + Prod.map f h ((g ⇊ k) c) = ((f ∘ g) ⇊ (h ∘ k)) c := rfl + +theorem map_comp_prod {f : α → β} {g : ι → α} {h : γ → δ} {k : ι → γ} : + Prod.map f h ∘ (g ⇊ k) = (f ∘ g) ⇊ (h ∘ k) := rfl + +/-- The diagonal map into `Prod`. -/ +protected def diag : α → α × α := id ⇊ id + +@[inherit_doc] prefix:max "⇗" => Function.diag + +section + +variable {a b : α} + +@[grind =] theorem diag_apply : ⇗a = (a, a) := rfl + +@[simp, grind =] theorem fst_diag : (⇗a).1 = a := rfl +@[simp, grind =] theorem snd_diag : (⇗a).2 = a := rfl + +@[simp, grind =] theorem map_diag {f : α → β} {g : α → γ} : Prod.map f g ⇗a = (f ⇊ g) a := rfl + +@[simp] theorem map_comp_diag {f : α → β} {g : α → γ} : Prod.map f g ∘ Function.diag = f ⇊ g := rfl + +theorem injective_diag : Function.Injective (α := α) Function.diag := fun _ _ => congrArg Prod.fst + +@[simp] theorem exists_diag_apply_iff (p : α × α) : (∃ a, ⇗a = p) ↔ p.1 = p.2 := by + simp [Prod.ext_iff, eq_comm] + +@[simp] theorem diag_eq_iff : ⇗a = ⇗b ↔ a = b := injective_diag.eq_iff + +@[simp] theorem prod_diag_diag : Function.diag ⇊ Function.diag (α := α) = + Function.diag ∘ Function.diag := rfl + +end + + +end Function diff --git a/Mathlib/MeasureTheory/Function/AEEqFun.lean b/Mathlib/MeasureTheory/Function/AEEqFun.lean index 30e7591ffabeb8..0a8f8c8746058f 100644 --- a/Mathlib/MeasureTheory/Function/AEEqFun.lean +++ b/Mathlib/MeasureTheory/Function/AEEqFun.lean @@ -397,15 +397,15 @@ def pair (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) : α →ₘ[μ] β × γ @[simp] theorem pair_mk_mk (f : α → β) (hf) (g : α → γ) (hg) : - (mk f hf : α →ₘ[μ] β).pair (mk g hg) = mk (fun x => (f x, g x)) (hf.prodMk hg) := + (mk f hf : α →ₘ[μ] β).pair (mk g hg) = mk (Function.prod f g) (hf.prodMk hg) := rfl theorem pair_eq_mk (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) : f.pair g = - mk (fun x => (f x, g x)) (f.aestronglyMeasurable.prodMk g.aestronglyMeasurable) := by + mk (Function.prod f g) (f.aestronglyMeasurable.prodMk g.aestronglyMeasurable) := by simp only [← pair_mk_mk, mk_coeFn, f.aestronglyMeasurable, g.aestronglyMeasurable] -theorem coeFn_pair (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) : f.pair g =ᵐ[μ] fun x => (f x, g x) := by +theorem coeFn_pair (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) : f.pair g =ᵐ[μ] Function.prod f g := by rw [pair_eq_mk] apply coeFn_mk diff --git a/Mathlib/MeasureTheory/Function/L1Space/Integrable.lean b/Mathlib/MeasureTheory/Function/L1Space/Integrable.lean index 77cca407c40a70..a8cfac493a6189 100644 --- a/Mathlib/MeasureTheory/Function/L1Space/Integrable.lean +++ b/Mathlib/MeasureTheory/Function/L1Space/Integrable.lean @@ -640,7 +640,7 @@ lemma integrable_of_le_of_le {f g₁ g₂ : α → ℝ} (hf : AEStronglyMeasurab -- TODO: generalising this to enorms requires defining a product instance for enormed monoids first @[fun_prop] theorem Integrable.prodMk {f : α → β} {g : α → γ} (hf : Integrable f μ) (hg : Integrable g μ) : - Integrable (fun x => (f x, g x)) μ := + Integrable (Function.prod f g) μ := ⟨by fun_prop, (hf.norm.add' hg.norm).mono <| Eventually.of_forall fun x => diff --git a/Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean b/Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean index ac19e8f1167772..3f375404d6398d 100644 --- a/Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean +++ b/Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean @@ -229,7 +229,7 @@ protected theorem snd {f : α → β × γ} (hf : AEStronglyMeasurable[m] f μ) @[fun_prop] protected theorem prodMk {f : α → β} {g : α → γ} (hf : AEStronglyMeasurable[m] f μ) - (hg : AEStronglyMeasurable[m] g μ) : AEStronglyMeasurable[m] (fun x => (f x, g x)) μ := + (hg : AEStronglyMeasurable[m] g μ) : AEStronglyMeasurable[m] (Function.prod f g) μ := ⟨fun x => (hf.mk f x, hg.mk g x), hf.stronglyMeasurable_mk.prodMk hg.stronglyMeasurable_mk, hf.ae_eq_mk.prodMk hg.ae_eq_mk⟩ diff --git a/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean b/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean index 3fb9a2f92a404a..adbc34e2567cc6 100644 --- a/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean +++ b/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean @@ -352,7 +352,7 @@ protected theorem snd {m : MeasurableSpace α} [TopologicalSpace β] [Topologica @[fun_prop] protected theorem prodMk {m : MeasurableSpace α} [TopologicalSpace β] [TopologicalSpace γ] {f : α → β} {g : α → γ} (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) : - StronglyMeasurable fun x => (f x, g x) := by + StronglyMeasurable Function.prod f g := by refine ⟨fun n => SimpleFunc.pair (hf.approx n) (hg.approx n), fun x => ?_⟩ rw [nhds_prod_eq] exact Tendsto.prodMk (hf.tendsto_approx x) (hg.tendsto_approx x) diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean b/Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean index a691c2a635bb27..3876b545a47161 100644 --- a/Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean +++ b/Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean @@ -406,7 +406,7 @@ theorem Measurable.prod {f : α → β × γ} (hf₁ : Measurable fun a => (f a) @[fun_prop] theorem Measurable.prodMk {β γ} {_ : MeasurableSpace β} {_ : MeasurableSpace γ} {f : α → β} - {g : α → γ} (hf : Measurable f) (hg : Measurable g) : Measurable fun a : α => (f a, g a) := + {g : α → γ} (hf : Measurable f) (hg : Measurable g) : Measurable (f ⇊ g) := Measurable.prod hf hg @[fun_prop] diff --git a/Mathlib/MeasureTheory/Measure/AEMeasurable.lean b/Mathlib/MeasureTheory/Measure/AEMeasurable.lean index caf6b54410060a..6b1c26db1846d7 100644 --- a/Mathlib/MeasureTheory/Measure/AEMeasurable.lean +++ b/Mathlib/MeasureTheory/Measure/AEMeasurable.lean @@ -190,7 +190,7 @@ protected theorem snd {f : α → β × γ} (hf : AEMeasurable f μ) : @[fun_prop] theorem prodMk {f : α → β} {g : α → γ} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : - AEMeasurable (fun x => (f x, g x)) μ := + AEMeasurable (Function.prod f g) μ := ⟨fun a => (hf.mk f a, hg.mk g a), hf.measurable_mk.prodMk hg.measurable_mk, hf.ae_eq_mk.prodMk hg.ae_eq_mk⟩ diff --git a/Mathlib/MeasureTheory/Measure/Prod.lean b/Mathlib/MeasureTheory/Measure/Prod.lean index 487fe7fd620c50..a231d7cf5fe2e3 100644 --- a/Mathlib/MeasureTheory/Measure/Prod.lean +++ b/Mathlib/MeasureTheory/Measure/Prod.lean @@ -1115,19 +1115,19 @@ lemma fst_prod [IsProbabilityMeasure ν] : (μ.prod ν).fst = μ := by rw [fst_apply hs, ← prod_univ, prod_prod, measure_univ, mul_one] theorem fst_map_prodMk₀ {X : α → β} {Y : α → γ} {μ : Measure α} - (hY : AEMeasurable Y μ) : (μ.map fun a => (X a, Y a)).fst = μ.map X := by + (hY : AEMeasurable Y μ) : (μ.map (X ⇊ Y)).fst = μ.map X := by by_cases hX : AEMeasurable X μ · ext1 s hs rw [Measure.fst_apply hs, Measure.map_apply_of_aemeasurable (hX.prodMk hY) (measurable_fst hs), Measure.map_apply_of_aemeasurable hX hs, ← prod_univ, mk_preimage_prod, preimage_univ, inter_univ] - · have : ¬AEMeasurable (fun x ↦ (X x, Y x)) μ := by + · have : ¬AEMeasurable (X ⇊ Y) μ := by contrapose! hX exact measurable_fst.comp_aemeasurable hX simp [map_of_not_aemeasurable, hX, this] theorem fst_map_prodMk {X : α → β} {Y : α → γ} {μ : Measure α} - (hY : Measurable Y) : (μ.map fun a => (X a, Y a)).fst = μ.map X := + (hY : Measurable Y) : (μ.map (X ⇊ Y)).fst = μ.map X := fst_map_prodMk₀ hY.aemeasurable @[simp] @@ -1177,19 +1177,19 @@ lemma snd_prod [IsProbabilityMeasure μ] : (μ.prod ν).snd = ν := by rw [snd_apply hs, ← univ_prod, prod_prod, measure_univ, one_mul] theorem snd_map_prodMk₀ {X : α → β} {Y : α → γ} {μ : Measure α} (hX : AEMeasurable X μ) : - (μ.map fun a => (X a, Y a)).snd = μ.map Y := by + (μ.map (X ⇊ Y)).snd = μ.map Y := by by_cases hY : AEMeasurable Y μ · ext1 s hs rw [Measure.snd_apply hs, Measure.map_apply_of_aemeasurable (hX.prodMk hY) (measurable_snd hs), Measure.map_apply_of_aemeasurable hY hs, ← univ_prod, mk_preimage_prod, preimage_univ, univ_inter] - · have : ¬AEMeasurable (fun x ↦ (X x, Y x)) μ := by + · have : ¬AEMeasurable (X ⇊ Y) μ := by contrapose! hY exact measurable_snd.comp_aemeasurable hY simp [map_of_not_aemeasurable, hY, this] theorem snd_map_prodMk {X : α → β} {Y : α → γ} {μ : Measure α} (hX : Measurable X) : - (μ.map fun a => (X a, Y a)).snd = μ.map Y := + (μ.map (X ⇊ Y)).snd = μ.map Y := snd_map_prodMk₀ hX.aemeasurable @[simp] diff --git a/Mathlib/NumberTheory/Height/Basic.lean b/Mathlib/NumberTheory/Height/Basic.lean index 5366554e2b265f..5a62146c478ad1 100644 --- a/Mathlib/NumberTheory/Height/Basic.lean +++ b/Mathlib/NumberTheory/Height/Basic.lean @@ -755,7 +755,7 @@ lemma mulHeight_mul_le (x y : ι → K) : mulHeight (x * y) ≤ mulHeight x * mu rcases eq_or_ne y 0 with rfl | hy · simpa using one_le_mulHeight x rw [← mulHeight_fun_mul_eq hx hy, - show x * y = (fun a ↦ x a.1 * y a.2) ∘ fun i ↦ (i, i) by ext1; simp] + show x * y = (fun a ↦ x a.1 * y a.2) ∘ Function.diag by ext1; simp] exact mulHeight_comp_le .. open Real in diff --git a/Mathlib/Order/Basic.lean b/Mathlib/Order/Basic.lean index 009c8e9c49d18f..1f09ab333bd8ff 100644 --- a/Mathlib/Order/Basic.lean +++ b/Mathlib/Order/Basic.lean @@ -13,6 +13,7 @@ public import Mathlib.Tactic.Convert public import Mathlib.Tactic.Inhabit public import Mathlib.Tactic.SimpRw public import Mathlib.Tactic.GCongr.Core +public import Mathlib.Logic.Function.Init /-! # Basic definitions about `≤` and `<` @@ -864,7 +865,7 @@ type synonym `α ×ₗ β = α × β`. namespace Prod section LE -variable [LE α] [LE β] {x y : α × β} {a a₁ a₂ : α} {b b₁ b₂ : β} +variable [LE α] [LE β] {x y : α × β} {a a₁ a₂ : α} {b b₁ b₂ : β} {α₂} {β₂} instance : LE (α × β) where le p q := p.1 ≤ q.1 ∧ p.2 ≤ q.2 @@ -1117,3 +1118,24 @@ noncomputable instance AsLinearOrder.linearOrder [PartialOrder α] [IsTotal α ( __ := (inferInstance : PartialOrder α) le_total := @total_of α (· ≤ ·) _ toDecidableLE := Classical.decRel _ + +namespace Function + +variable {α β₁ β₂ : Type*} [LE β₁] [LE β₂] + +@[simp] +lemma pair_le_pair_iff {u₁ v₁ : α → β₁} {u₂ v₂ : α → β₂} : + u₁ ⇊ u₂ ≤ v₁ ⇊ v₂ ↔ u₁ ≤ v₁ ∧ u₂ ≤ v₂ := by + simp [Pi.le_def, Prod.le_def, forall_and] + +lemma const_le_pair_iff {b : β₁ × β₂} {v₁ : α → β₁} {v₂ : α → β₂} : + Function.const _ b ≤ v₁ ⇊ v₂ ↔ + Function.const _ b.1 ≤ v₁ ∧ Function.const _ b.2 ≤ v₂ := + prod_const_const b.1 b.2 ▸ pair_le_pair_iff .. + +lemma pair_le_const_iff {b : β₁ × β₂} {v₁ : α → β₁} {v₂ : α → β₂} : + v₁ ⇊ v₂ ≤ Function.const _ b ↔ + v₁ ≤ Function.const _ b.1 ∧ v₂ ≤ Function.const _ b.2 := + prod_const_const b.1 b.2 ▸ pair_le_pair_iff .. + +end Function diff --git a/Mathlib/Order/CompleteLattice/Basic.lean b/Mathlib/Order/CompleteLattice/Basic.lean index 2dc62513a3fddb..dc5474812fd98b 100644 --- a/Mathlib/Order/CompleteLattice/Basic.lean +++ b/Mathlib/Order/CompleteLattice/Basic.lean @@ -776,7 +776,7 @@ theorem biSup_prod' {f : β → γ → α} {s : Set β} {t : Set γ} : @[to_dual] theorem iSup_image2 {γ δ} (f : β → γ → δ) (s : Set β) (t : Set γ) (g : δ → α) : ⨆ d ∈ image2 f s t, g d = ⨆ b ∈ s, ⨆ c ∈ t, g (f b c) := by - rw [← image_prod, iSup_image, biSup_prod] + simp_rw [← image_uncurry_prod, iSup_image, biSup_prod, uncurry_apply] @[to_dual] theorem iSup_sum {f : β ⊕ γ → α} : ⨆ x, f x = (⨆ i, f (Sum.inl i)) ⊔ ⨆ j, f (Sum.inr j) := @@ -807,7 +807,8 @@ theorem iSup_ne_bot_subtype (f : ι → α) : ⨆ i : { i // f i ≠ ⊥ }, f i @[to_dual] theorem sSup_image2 {f : β → γ → α} {s : Set β} {t : Set γ} : - sSup (image2 f s t) = ⨆ (a ∈ s) (b ∈ t), f a b := by rw [← image_prod, sSup_image, biSup_prod] + sSup (image2 f s t) = ⨆ (a ∈ s) (b ∈ t), f a b := by + simp_rw [← image_uncurry_prod, sSup_image, biSup_prod, uncurry_apply] end diff --git a/Mathlib/Order/Filter/Basic.lean b/Mathlib/Order/Filter/Basic.lean index 4c785e2440a714..7caafdaaa0a114 100644 --- a/Mathlib/Order/Filter/Basic.lean +++ b/Mathlib/Order/Filter/Basic.lean @@ -976,11 +976,7 @@ instance {l : Filter α} : trans := EventuallyEq.trans theorem EventuallyEq.prodMk {l} {f f' : α → β} (hf : f =ᶠ[l] f') {g g' : α → γ} (hg : g =ᶠ[l] g') : - (fun x => (f x, g x)) =ᶠ[l] fun x => (f' x, g' x) := - hf.mp <| - hg.mono <| by - intros - simp only [*] + (Function.prod f g) =ᶠ[l] (f' ⇊ g') := hf.mp <| hg.mono <| by grind /-- See `EventuallyEq.comp_tendsto` in Mathlib.Order.Filter.Tendsto for a similar statement w.r.t. composition on the right. -/ diff --git a/Mathlib/Order/Filter/EventuallyConst.lean b/Mathlib/Order/Filter/EventuallyConst.lean index ca8acc5962f950..0e6b612d4b3eff 100644 --- a/Mathlib/Order/Filter/EventuallyConst.lean +++ b/Mathlib/Order/Filter/EventuallyConst.lean @@ -125,7 +125,7 @@ lemma comp₂ {g : α → γ} (hf : EventuallyConst f l) (op : β → γ → δ) (tendsto_map (f := op.uncurry)).comp (tendsto_map.prodMk tendsto_map) lemma prodMk {g : α → γ} (hf : EventuallyConst f l) (hg : EventuallyConst g l) : - EventuallyConst (fun x ↦ (f x, g x)) l := + EventuallyConst (f ⇊ g) l := hf.comp₂ Prod.mk hg @[to_additive] diff --git a/Mathlib/Order/Filter/Prod.lean b/Mathlib/Order/Filter/Prod.lean index 7b62056a431787..dbd4bd3fa38d5d 100644 --- a/Mathlib/Order/Filter/Prod.lean +++ b/Mathlib/Order/Filter/Prod.lean @@ -136,12 +136,12 @@ theorem Tendsto.snd {h : Filter γ} {m : α → β × γ} (H : Tendsto m f (g × Tendsto (fun a ↦ (m a).2) f h := tendsto_snd.comp H -theorem Tendsto.prodMk {h : Filter γ} {m₁ : α → β} {m₂ : α → γ} - (h₁ : Tendsto m₁ f g) (h₂ : Tendsto m₂ f h) : Tendsto (fun x => (m₁ x, m₂ x)) f (g ×ˢ h) := +theorem Tendsto.prod {h : Filter γ} {m₁ : α → β} {m₂ : α → γ} + (h₁ : Tendsto m₁ f g) (h₂ : Tendsto m₂ f h) : Tendsto (m₁ ⇊ m₂) f (g ×ˢ h) := tendsto_inf.2 ⟨tendsto_comap_iff.2 h₁, tendsto_comap_iff.2 h₂⟩ theorem tendsto_prod_swap : Tendsto (Prod.swap : α × β → β × α) (f ×ˢ g) (g ×ˢ f) := - tendsto_snd.prodMk tendsto_fst + tendsto_snd.prod tendsto_fst theorem Eventually.prod_inl {la : Filter α} {p : α → Prop} (h : ∀ᶠ x in la, p x) (lb : Filter β) : ∀ᶠ x in la ×ˢ lb, p (x : α × β).1 := @@ -202,7 +202,7 @@ theorem Eventually.diag_of_prod_right {f : Filter α} {g : Filter γ} {p : α × obtain ⟨t, ht, s, hs, hst⟩ := eventually_prod_iff.1 h exact (ht.prod_mk hs.diag_of_prod).mono fun x hx => by simp only [hst hx.1 hx.2] -theorem tendsto_diag : Tendsto (fun i => (i, i)) f (f ×ˢ f) := +theorem tendsto_diag : Tendsto Function.diag f (f ×ˢ f) := tendsto_iff_eventually.mpr fun _ hpr => hpr.diag_of_prod theorem prod_iInf_left [Nonempty ι] {f : ι → Filter α} {g : Filter β} : @@ -293,13 +293,16 @@ lemma Eventually.trans_prod {h : Filter γ} theorem prod_assoc (f : Filter α) (g : Filter β) (h : Filter γ) : map (Equiv.prodAssoc α β γ) ((f ×ˢ g) ×ˢ h) = f ×ˢ (g ×ˢ h) := by - simp_rw [← comap_equiv_symm, prod_eq_inf, comap_inf, comap_comap, inf_assoc, - Function.comp_def, Equiv.prodAssoc_symm_apply] + unfold Equiv.prodAssoc + simp only [prod_eq_inf, comap_inf, comap_comap, inf_assoc, map_inf (Equiv.injective _), + ← comap_equiv_symm, comap_comap, Equiv.coe_fn_symm_mk, Function.comp_assoc, + Function.fst_comp_prod, Function.snd_comp_prod] theorem prod_assoc_symm (f : Filter α) (g : Filter β) (h : Filter γ) : map (Equiv.prodAssoc α β γ).symm (f ×ˢ (g ×ˢ h)) = (f ×ˢ g) ×ˢ h := by - simp_rw [map_equiv_symm, prod_eq_inf, comap_inf, comap_comap, inf_assoc, - Function.comp_def, Equiv.prodAssoc_apply] + unfold Equiv.prodAssoc + simp only [map_equiv_symm, Equiv.coe_fn_mk, prod_eq_inf, comap_inf, comap_comap, inf_assoc, + Function.comp_assoc, Function.fst_comp_prod, Function.snd_comp_prod] theorem tendsto_prodAssoc {h : Filter γ} : Tendsto (Equiv.prodAssoc α β γ) ((f ×ˢ g) ×ˢ h) (f ×ˢ (g ×ˢ h)) := @@ -328,7 +331,7 @@ theorem prod_map_map_eq.{u, v, w, x} {α₁ : Type u} {α₂ : Type v} {β₁ : let ⟨s₁, hs₁, s₂, hs₂, h⟩ := mem_prod_iff.mp hs mem_of_superset (prod_mem_prod (image_mem_map hs₁) (image_mem_map hs₂)) <| by rwa [prod_image_image_eq, image_subset_iff]) - ((tendsto_map.comp tendsto_fst).prodMk (tendsto_map.comp tendsto_snd)) + ((tendsto_map.comp tendsto_fst).prod (tendsto_map.comp tendsto_snd)) theorem prod_map_map_eq' {α₁ : Type*} {α₂ : Type*} {β₁ : Type*} {β₂ : Type*} (f : α₁ → α₂) (g : β₁ → β₂) (F : Filter α₁) (G : Filter β₁) : diff --git a/Mathlib/Order/Hom/Basic.lean b/Mathlib/Order/Hom/Basic.lean index 203d35fd18e021..85eee786978f53 100644 --- a/Mathlib/Order/Hom/Basic.lean +++ b/Mathlib/Order/Hom/Basic.lean @@ -369,7 +369,7 @@ theorem comp_const (γ : Type*) [Preorder γ] (f : α →o β) (c : α) : `OrderHom`. -/ @[simps] protected def prod (f : α →o β) (g : α →o γ) : α →o β × γ := - ⟨fun x => (f x, g x), fun _ _ h => ⟨f.mono h, g.mono h⟩⟩ + ⟨Function.prod f g, fun _ _ h => ⟨f.mono h, g.mono h⟩⟩ @[mono, to_dual self] theorem prod_mono {f₁ f₂ : α →o β} (hf : f₁ ≤ f₂) {g₁ g₂ : α →o γ} (hg : g₁ ≤ g₂) : @@ -894,7 +894,7 @@ def prodComm : α × β ≃o β × α where def prodAssoc (α β γ : Type*) [LE α] [LE β] [LE γ] : (α × β) × γ ≃o α × (β × γ) where toEquiv := .prodAssoc α β γ - map_rel_iff' := @fun ⟨⟨_, _⟩, _⟩ ⟨⟨_, _⟩, _⟩ ↦ by simp [Equiv.prodAssoc, and_assoc] + map_rel_iff' := @fun ⟨⟨_, _⟩, _⟩ ⟨⟨_, _⟩, _⟩ ↦ by simp [and_assoc, Prod.le_def] @[simp] theorem coe_prodComm : ⇑(prodComm : α × β ≃o β × α) = Prod.swap := diff --git a/Mathlib/Order/Monotone/Defs.lean b/Mathlib/Order/Monotone/Defs.lean index 76e1afbe8215dc..c052cef6e38ccc 100644 --- a/Mathlib/Order/Monotone/Defs.lean +++ b/Mathlib/Order/Monotone/Defs.lean @@ -507,11 +507,11 @@ theorem monotone_fst : Monotone (@Prod.fst α β) := fun _ _ ↦ And.left theorem monotone_snd : Monotone (@Prod.snd α β) := fun _ _ ↦ And.right theorem monotone_prodMk_iff {f : γ → α} {g : γ → β} : - Monotone (fun x => (f x, g x)) ↔ Monotone f ∧ Monotone g := by - simp_rw [Monotone, Prod.mk_le_mk, forall_and] + Monotone (Function.prod f g) ↔ Monotone f ∧ Monotone g := by + simp [Monotone, Prod.le_def, forall_and] theorem Monotone.prodMk {f : γ → α} {g : γ → β} (hf : Monotone f) (hg : Monotone g) : - Monotone (fun x => (f x, g x)) := + Monotone (Function.prod f g) := monotone_prodMk_iff.2 ⟨hf, hg⟩ theorem Monotone.prodMap (hf : Monotone f) (hg : Monotone g) : Monotone (Prod.map f g) := diff --git a/Mathlib/Order/OmegaCompletePartialOrder.lean b/Mathlib/Order/OmegaCompletePartialOrder.lean index d7177b87e2b1a0..71efd85366fd64 100644 --- a/Mathlib/Order/OmegaCompletePartialOrder.lean +++ b/Mathlib/Order/OmegaCompletePartialOrder.lean @@ -448,7 +448,7 @@ theorem ωSup_zip (c₀ : Chain α) (c₁ : Chain β) : ωSup (c₀.zip c₁) = @[fun_prop] lemma ωScottContinuous.prodMk {f : α → β} (hf : ωScottContinuous f) {g : α → γ} (hg : ωScottContinuous g) : - ωScottContinuous fun x ↦ (f x, g x) := + ωScottContinuous (f ⇊ g) := ScottContinuousOn.prodMk (fun a b hab ↦ ⟨pair a b hab, range_pair a b hab⟩) hf hg @[fun_prop] diff --git a/Mathlib/Order/ScottContinuity.lean b/Mathlib/Order/ScottContinuity.lean index 0f1b1eebde29ff..d730c9758c7f17 100644 --- a/Mathlib/Order/ScottContinuity.lean +++ b/Mathlib/Order/ScottContinuity.lean @@ -106,16 +106,16 @@ theorem ScottContinuousOn.image_comp {g : β → γ} @[fun_prop] lemma ScottContinuousOn.prodMk {g : α → γ} (hD : ∀ a b : α, a ≤ b → {a, b} ∈ D) (hf : ScottContinuousOn D f) (hg : ScottContinuousOn D g) : - ScottContinuousOn D fun x => (f x, g x) := fun d hd₁ hd₂ hd₃ a hda => by + ScottContinuousOn D (f ⇊ g) := fun d hd₁ hd₂ hd₃ a hda => by rw [IsLUB, IsLeast, upperBounds] constructor · simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq, - Prod.mk_le_mk] + Function.prod_apply, Prod.mk_le_mk] intro b hb exact ⟨hf.monotone D hD (hda.1 hb), hg.monotone D hD (hda.1 hb)⟩ · intro ⟨p₁, p₂⟩ hp simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq, - Prod.mk_le_mk] at hp + Function.prod_apply, Prod.mk_le_mk] at hp ⊢ constructor · rw [isLUB_le_iff (hf hd₁ hd₂ hd₃ hda), upperBounds] simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq] @@ -172,7 +172,7 @@ lemma ScottContinuous.comp {g : β → γ} @[fun_prop] lemma ScottContinuous.prodMk {g : α → γ} (hf : ScottContinuous f) (hg : ScottContinuous g) : - ScottContinuous fun x => (f x, g x) := by + ScottContinuous (f ⇊ g) := by rw [← scottContinuousOn_univ] at ⊢ hf hg exact ScottContinuousOn.prodMk (by grind) hf hg diff --git a/Mathlib/Probability/Independence/Conditional.lean b/Mathlib/Probability/Independence/Conditional.lean index 73824a2ca4f765..e3e76d0a4a4218 100644 --- a/Mathlib/Probability/Independence/Conditional.lean +++ b/Mathlib/Probability/Independence/Conditional.lean @@ -876,7 +876,7 @@ theorem condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight Measure.compProd_eq_comp_prod] let e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm have h_eq : ((Kernel.id ×ₖ condDistrib g k μ) ×ₖ condDistrib f k μ) ∘ₘ μ.map k = - (Kernel.id ×ₖ (condDistrib f k μ).prodMkRight _) ∘ₘ μ.map (fun a ↦ (k a, g a)) := by + (Kernel.id ×ₖ (condDistrib f k μ).prodMkRight _) ∘ₘ μ.map (k ⇊ g) := by calc ((Kernel.id ×ₖ condDistrib g k μ) ×ₖ condDistrib f k μ) ∘ₘ μ.map k _ = (Kernel.id ×ₖ (condDistrib f k μ).prodMkRight _) ∘ₘ (μ.map k ⊗ₘ condDistrib g k μ) := by rw [Measure.compProd_eq_comp_prod, Measure.comp_assoc] @@ -885,7 +885,7 @@ theorem condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight (condDistrib f k μ) Kernel.id measurable_id rw [← Kernel.id] at h simpa using h.symm - _ = (Kernel.id ×ₖ (condDistrib f k μ).prodMkRight _) ∘ₘ μ.map (fun a ↦ (k a, g a)) := by + _ = (Kernel.id ×ₖ (condDistrib f k μ).prodMkRight _) ∘ₘ μ.map (k ⇊ g) := by rw [compProd_map_condDistrib hg.aemeasurable] rw [← h_eq] have h1 : μ.map (fun x ↦ ((k x, g x), f x)) = (μ.map (fun a ↦ (k a, g a, f a))).map e := by diff --git a/Mathlib/Probability/Kernel/Basic.lean b/Mathlib/Probability/Kernel/Basic.lean index b1098ee54922a5..dadf20a07be2ac 100644 --- a/Mathlib/Probability/Kernel/Basic.lean +++ b/Mathlib/Probability/Kernel/Basic.lean @@ -130,7 +130,7 @@ section Copy /-- The deterministic kernel that maps `x : α` to the Dirac measure at `(x, x) : α × α`. -/ noncomputable def copy (α : Type*) [MeasurableSpace α] : Kernel α (α × α) := - Kernel.deterministic (fun x ↦ (x, x)) (measurable_id.prod measurable_id) + Kernel.deterministic Function.diag (measurable_id.prod measurable_id) instance : IsMarkovKernel (copy α) := by rw [copy]; infer_instance diff --git a/Mathlib/Probability/Kernel/Composition/MapComap.lean b/Mathlib/Probability/Kernel/Composition/MapComap.lean index d99d07d86f0cb6..56aeb13bc3f54a 100644 --- a/Mathlib/Probability/Kernel/Composition/MapComap.lean +++ b/Mathlib/Probability/Kernel/Composition/MapComap.lean @@ -450,13 +450,13 @@ instance (priority := 100) isFiniteKernel_of_isFiniteKernel_fst {κ : Kernel α simp lemma fst_map_prod (κ : Kernel α β) {f : β → γ} {g : β → δ} (hg : Measurable g) : - fst (map κ (fun x ↦ (f x, g x))) = map κ f := by + fst (map κ (f ⇊ g)) = map κ f := by by_cases hf : Measurable f · ext x s hs rw [fst_apply' _ _ hs, map_apply' _ (hf.prod hg) _, map_apply' _ hf _ hs] · simp only [Set.preimage, Set.mem_setOf] · exact measurable_fst hs - · have : ¬ Measurable (fun x ↦ (f x, g x)) := by + · have : ¬ Measurable (f ⇊ g) := by contrapose! hf; exact hf.fst simp [map_of_not_measurable _ hf, map_of_not_measurable _ this] @@ -512,13 +512,13 @@ instance (priority := 100) isFiniteKernel_of_isFiniteKernel_snd {κ : Kernel α simp lemma snd_map_prod (κ : Kernel α β) {f : β → γ} {g : β → δ} (hf : Measurable f) : - snd (map κ (fun x ↦ (f x, g x))) = map κ g := by + snd (map κ (f ⇊ g)) = map κ g := by by_cases hg : Measurable g · ext x s hs rw [snd_apply' _ _ hs, map_apply' _ (hf.prod hg), map_apply' _ hg _ hs] · simp only [Set.preimage, Set.mem_setOf] · exact measurable_snd hs - · have : ¬ Measurable (fun x ↦ (f x, g x)) := by + · have : ¬ Measurable (f ⇊ g) := by contrapose! hg; exact hg.snd simp [map_of_not_measurable _ hg, map_of_not_measurable _ this] diff --git a/Mathlib/Probability/Kernel/Composition/MeasureComp.lean b/Mathlib/Probability/Kernel/Composition/MeasureComp.lean index 81bf2b2cfb4af6..be06725c69dcc6 100644 --- a/Mathlib/Probability/Kernel/Composition/MeasureComp.lean +++ b/Mathlib/Probability/Kernel/Composition/MeasureComp.lean @@ -94,7 +94,7 @@ lemma discard_comp (μ : Measure α) : Kernel.discard α ∘ₘ μ = μ .univ ext s hs; simp [Measure.bind_apply hs (Kernel.aemeasurable _), mul_comm] lemma copy_comp_map {f : α → β} (hf : AEMeasurable f μ) : - Kernel.copy β ∘ₘ (μ.map f) = μ.map (fun a ↦ (f a, f a)) := by + Kernel.copy β ∘ₘ (μ.map f) = μ.map (Function.diag ∘ f) := by rw [Kernel.copy, deterministic_comp_eq_map, AEMeasurable.map_map_of_aemeasurable (by fun_prop) hf] rfl diff --git a/Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean b/Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean index cd7d039fbe6cc8..06d950e9c855a1 100644 --- a/Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean +++ b/Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean @@ -99,14 +99,14 @@ lemma _root_.ProbabilityTheory.Kernel.compProd_apply_eq_compProd_sectR {γ : Typ ext s hs simp_rw [Kernel.compProd_apply hs, compProd_apply hs, Kernel.sectR_apply] -lemma compProd_id [SFinite μ] : μ ⊗ₘ Kernel.id = μ.map (fun x ↦ (x, x)) := by +lemma compProd_id [SFinite μ] : μ ⊗ₘ Kernel.id = μ.map Function.diag := by ext s hs rw [compProd_apply hs, map_apply (measurable_id.prod measurable_id) hs] have h_meas a : MeasurableSet (Prod.mk a ⁻¹' s) := measurable_prodMk_left hs simp_rw [Kernel.id_apply, dirac_apply' _ (h_meas _)] calc ∫⁻ a, (Prod.mk a ⁻¹' s).indicator 1 a ∂μ - _ = ∫⁻ a, ((fun x ↦ (x, x)) ⁻¹' s).indicator 1 a ∂μ := rfl - _ = μ ((fun x ↦ (x, x)) ⁻¹' s) := by + _ = ∫⁻ a, (Function.diag ⁻¹' s).indicator 1 a ∂μ := rfl + _ = μ (Function.diag ⁻¹' s) := by rw [lintegral_indicator_one] exact (measurable_id.prod measurable_id) hs diff --git a/Mathlib/Probability/Kernel/Composition/Prod.lean b/Mathlib/Probability/Kernel/Composition/Prod.lean index 4c2ca33414e800..bc7790fbc4e9e4 100644 --- a/Mathlib/Probability/Kernel/Composition/Prod.lean +++ b/Mathlib/Probability/Kernel/Composition/Prod.lean @@ -216,7 +216,7 @@ lemma swap_prod {κ : Kernel α β} [IsSFiniteKernel κ] {η : Kernel α γ} [Is lemma deterministic_prod_deterministic {f : α → β} {g : α → γ} (hf : Measurable f) (hg : Measurable g) : deterministic f hf ×ₖ deterministic g hg - = deterministic (fun a ↦ (f a, g a)) (hf.prodMk hg) := by + = deterministic (Function.prod f g) (hf.prodMk hg) := by ext; simp_rw [prod_apply, deterministic_apply, Measure.dirac_prod_dirac] lemma id_prod_eq : @Kernel.id (α × β) inferInstance = diff --git a/Mathlib/Probability/Kernel/CondDistrib.lean b/Mathlib/Probability/Kernel/CondDistrib.lean index 3a8c1ba8d3f380..93663a650f9076 100644 --- a/Mathlib/Probability/Kernel/CondDistrib.lean +++ b/Mathlib/Probability/Kernel/CondDistrib.lean @@ -63,7 +63,7 @@ the conditional expectation `μ⟦Y ⁻¹' s | mβ.comap X⟧ a`. It also satisf for all integrable functions `f`. -/ noncomputable irreducible_def condDistrib {_ : MeasurableSpace α} [MeasurableSpace β] (Y : α → Ω) (X : α → β) (μ : Measure α) [IsFiniteMeasure μ] : Kernel β Ω := - (μ.map fun a => (X a, Y a)).condKernel + (μ.map (X ⇊ Y)).condKernel instance [MeasurableSpace β] : IsMarkovKernel (condDistrib Y X μ) := by rw [condDistrib]; infer_instance @@ -71,10 +71,10 @@ instance [MeasurableSpace β] : IsMarkovKernel (condDistrib Y X μ) := by variable {mβ : MeasurableSpace β} {s : Set Ω} {t : Set β} {f : β × Ω → F} /-- If the singleton `{x}` has non-zero mass for `μ.map X`, then for all `s : Set Ω`, -`condDistrib Y X μ x s = (μ.map X {x})⁻¹ * μ.map (fun a => (X a, Y a)) ({x} ×ˢ s)` . -/ +`condDistrib Y X μ x s = (μ.map X {x})⁻¹ * μ.map ((X ⇊ Y)) ({x} ×ˢ s)` . -/ lemma condDistrib_apply_of_ne_zero [MeasurableSingletonClass β] (hY : Measurable Y) (x : β) (hX : μ.map X {x} ≠ 0) (s : Set Ω) : - condDistrib Y X μ x s = (μ.map X {x})⁻¹ * μ.map (fun a => (X a, Y a)) ({x} ×ˢ s) := by + condDistrib Y X μ x s = (μ.map X {x})⁻¹ * μ.map ((X ⇊ Y)) ({x} ×ˢ s) := by rw [condDistrib, Measure.condKernel_apply_of_ne_zero _ s] · rw [Measure.fst_map_prodMk hY] · rwa [Measure.fst_map_prodMk hY] @@ -109,10 +109,10 @@ theorem measurable_condDistrib (hs : MeasurableSet s) : (Kernel.measurable_coe _ hs).comp (Measurable.of_comap_le le_rfl) theorem _root_.MeasureTheory.AEStronglyMeasurable.ae_integrable_condDistrib_map_iff - (hY : AEMeasurable Y μ) (hf : AEStronglyMeasurable f (μ.map fun a => (X a, Y a))) : + (hY : AEMeasurable Y μ) (hf : AEStronglyMeasurable f (μ.map (X ⇊ Y))) : (∀ᵐ a ∂μ.map X, Integrable (fun ω => f (a, ω)) (condDistrib Y X μ a)) ∧ Integrable (fun a => ∫ ω, ‖f (a, ω)‖ ∂condDistrib Y X μ a) (μ.map X) ↔ - Integrable f (μ.map fun a => (X a, Y a)) := by + Integrable f (μ.map (X ⇊ Y)) := by rw [condDistrib, ← hf.ae_integrable_condKernel_iff, Measure.fst_map_prodMk₀ hY] variable [NormedSpace ℝ F] @@ -122,12 +122,12 @@ theorem _root_.MeasureTheory.StronglyMeasurable.integral_condDistrib (hf : Stron rw [condDistrib]; exact hf.integral_kernel_prod_right' theorem _root_.MeasureTheory.AEStronglyMeasurable.integral_condDistrib_map - (hY : AEMeasurable Y μ) (hf : AEStronglyMeasurable f (μ.map fun a => (X a, Y a))) : + (hY : AEMeasurable Y μ) (hf : AEStronglyMeasurable f (μ.map (X ⇊ Y))) : AEStronglyMeasurable (fun x => ∫ y, f (x, y) ∂condDistrib Y X μ x) (μ.map X) := by rw [← Measure.fst_map_prodMk₀ hY, condDistrib]; exact hf.integral_condKernel theorem _root_.MeasureTheory.AEStronglyMeasurable.integral_condDistrib (hX : AEMeasurable X μ) - (hY : AEMeasurable Y μ) (hf : AEStronglyMeasurable f (μ.map fun a => (X a, Y a))) : + (hY : AEMeasurable Y μ) (hf : AEStronglyMeasurable f (μ.map (X ⇊ Y))) : AEStronglyMeasurable (fun a => ∫ y, f (X a, y) ∂condDistrib Y X μ (X a)) μ := (hf.integral_condDistrib_map hY).comp_aemeasurable hX @@ -136,7 +136,7 @@ theorem stronglyMeasurable_integral_condDistrib (hf : StronglyMeasurable f) : (hf.integral_condDistrib).comp_measurable <| Measurable.of_comap_le le_rfl theorem aestronglyMeasurable_integral_condDistrib (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) - (hf : AEStronglyMeasurable f (μ.map fun a => (X a, Y a))) : + (hf : AEStronglyMeasurable f (μ.map (X ⇊ Y))) : AEStronglyMeasurable[mβ.comap X] (fun a => ∫ y, f (X a, y) ∂condDistrib Y X μ (X a)) μ := (hf.integral_condDistrib_map hY).comp_ae_measurable' hX @@ -148,7 +148,7 @@ theorem condDistrib_ae_eq_of_measure_eq_compProd_of_measurable (hX : Measurable X) (hY : Measurable Y) {κ : Kernel β Ω} [IsFiniteKernel κ] (hκ : μ.map (fun x => (X x, Y x)) = μ.map X ⊗ₘ κ) : condDistrib Y X μ =ᵐ[μ.map X] κ := by - have heq : μ.map X = (μ.map (fun x ↦ (X x, Y x))).fst := by + have heq : μ.map X = (μ.map (X ⇊ Y)).fst := by ext s hs rw [Measure.map_apply hX hs, Measure.fst_apply hs, Measure.map_apply] exacts [rfl, Measurable.prod hX hY, measurable_fst hs] @@ -187,7 +187,7 @@ lemma condDistrib_comp {Ω' : Type*} {mΩ' : MeasurableSpace Ω'} [StandardBorel swap; · simp [Measure.map_of_not_aemeasurable hX, Filter.EventuallyEq] refine condDistrib_ae_eq_of_measure_eq_compProd X (by fun_prop) ?_ calc μ.map (fun x ↦ (X x, (f ∘ Y) x)) - _ = (μ.map (fun x ↦ (X x, Y x))).map (Prod.map id f) := by + _ = (μ.map (X ⇊ Y)).map (Prod.map id f) := by rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)] simp [Function.comp_def] _ = (μ.map X ⊗ₘ condDistrib Y X μ).map (Prod.map id f) := by rw [compProd_map_condDistrib hY] @@ -259,45 +259,45 @@ theorem integrable_toReal_condDistrib (hX : AEMeasurable X μ) (hs : MeasurableS _ < ∞ := measure_lt_top _ _ theorem _root_.MeasureTheory.Integrable.condDistrib_ae_map - (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map fun a => (X a, Y a))) : + (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map (X ⇊ Y))) : ∀ᵐ b ∂μ.map X, Integrable (fun ω => f (b, ω)) (condDistrib Y X μ b) := by rw [condDistrib, ← Measure.fst_map_prodMk₀ (X := X) hY]; exact hf_int.condKernel_ae theorem _root_.MeasureTheory.Integrable.condDistrib_ae (hX : AEMeasurable X μ) - (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map fun a => (X a, Y a))) : + (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map (X ⇊ Y))) : ∀ᵐ a ∂μ, Integrable (fun ω => f (X a, ω)) (condDistrib Y X μ (X a)) := ae_of_ae_map hX (hf_int.condDistrib_ae_map hY) theorem _root_.MeasureTheory.Integrable.integral_norm_condDistrib_map - (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map fun a => (X a, Y a))) : + (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map (X ⇊ Y))) : Integrable (fun x => ∫ y, ‖f (x, y)‖ ∂condDistrib Y X μ x) (μ.map X) := by rw [condDistrib, ← Measure.fst_map_prodMk₀ (X := X) hY]; exact hf_int.integral_norm_condKernel theorem _root_.MeasureTheory.Integrable.integral_norm_condDistrib (hX : AEMeasurable X μ) - (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map fun a => (X a, Y a))) : + (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map (X ⇊ Y))) : Integrable (fun a => ∫ y, ‖f (X a, y)‖ ∂condDistrib Y X μ (X a)) μ := (hf_int.integral_norm_condDistrib_map hY).comp_aemeasurable hX variable [NormedSpace ℝ F] theorem _root_.MeasureTheory.Integrable.norm_integral_condDistrib_map - (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map fun a => (X a, Y a))) : + (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map (X ⇊ Y))) : Integrable (fun x => ‖∫ y, f (x, y) ∂condDistrib Y X μ x‖) (μ.map X) := by rw [condDistrib, ← Measure.fst_map_prodMk₀ (X := X) hY]; exact hf_int.norm_integral_condKernel theorem _root_.MeasureTheory.Integrable.norm_integral_condDistrib (hX : AEMeasurable X μ) - (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map fun a => (X a, Y a))) : + (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map (X ⇊ Y))) : Integrable (fun a => ‖∫ y, f (X a, y) ∂condDistrib Y X μ (X a)‖) μ := (hf_int.norm_integral_condDistrib_map hY).comp_aemeasurable hX theorem _root_.MeasureTheory.Integrable.integral_condDistrib_map - (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map fun a => (X a, Y a))) : + (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map (X ⇊ Y))) : Integrable (fun x => ∫ y, f (x, y) ∂condDistrib Y X μ x) (μ.map X) := (integrable_norm_iff (hf_int.1.integral_condDistrib_map hY)).mp (hf_int.norm_integral_condDistrib_map hY) theorem _root_.MeasureTheory.Integrable.integral_condDistrib (hX : AEMeasurable X μ) - (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map fun a => (X a, Y a))) : + (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map (X ⇊ Y))) : Integrable (fun a => ∫ y, f (X a, y) ∂condDistrib Y X μ (X a)) μ := (hf_int.integral_condDistrib_map hY).comp_aemeasurable hX @@ -336,7 +336,7 @@ theorem condDistrib_ae_eq_condExp (hX : Measurable X) (hY : Measurable Y) (hs : to the integral of `y ↦ f(X, y)` against the `condDistrib` kernel. -/ theorem condExp_prod_ae_eq_integral_condDistrib' [NormedSpace ℝ F] [CompleteSpace F] (hX : Measurable X) (hY : AEMeasurable Y μ) - (hf_int : Integrable f (μ.map fun a => (X a, Y a))) : + (hf_int : Integrable f (μ.map (X ⇊ Y))) : μ[fun a => f (X a, Y a) | mβ.comap X] =ᵐ[μ] fun a => ∫ y, f (X a, y) ∂condDistrib Y X μ (X a) := by have hf_int' : Integrable (fun a => f (X a, Y a)) μ := @@ -361,10 +361,10 @@ theorem condExp_prod_ae_eq_integral_condDistrib' [NormedSpace ℝ F] [CompleteSp to the integral of `y ↦ f(X, y)` against the `condDistrib` kernel. -/ theorem condExp_prod_ae_eq_integral_condDistrib₀ [NormedSpace ℝ F] [CompleteSpace F] (hX : Measurable X) (hY : AEMeasurable Y μ) - (hf : AEStronglyMeasurable f (μ.map fun a => (X a, Y a))) + (hf : AEStronglyMeasurable f (μ.map (X ⇊ Y))) (hf_int : Integrable (fun a => f (X a, Y a)) μ) : μ[fun a => f (X a, Y a) | mβ.comap X] =ᵐ[μ] fun a => ∫ y, f (X a, y) ∂condDistrib Y X μ (X a) := - have hf_int' : Integrable f (μ.map fun a => (X a, Y a)) := by + have hf_int' : Integrable f (μ.map (X ⇊ Y)) := by rwa [integrable_map_measure hf (hX.aemeasurable.prodMk hY)] condExp_prod_ae_eq_integral_condDistrib' hX hY hf_int' @@ -374,7 +374,7 @@ theorem condExp_prod_ae_eq_integral_condDistrib [NormedSpace ℝ F] [CompleteSpa (hX : Measurable X) (hY : AEMeasurable Y μ) (hf : StronglyMeasurable f) (hf_int : Integrable (fun a => f (X a, Y a)) μ) : μ[fun a => f (X a, Y a) | mβ.comap X] =ᵐ[μ] fun a => ∫ y, f (X a, y) ∂condDistrib Y X μ (X a) := - have hf_int' : Integrable f (μ.map fun a => (X a, Y a)) := by + have hf_int' : Integrable f (μ.map (X ⇊ Y)) := by rwa [integrable_map_measure hf.aestronglyMeasurable (hX.aemeasurable.prodMk hY)] condExp_prod_ae_eq_integral_condDistrib' hX hY hf_int' diff --git a/Mathlib/Tactic/FunProp.lean b/Mathlib/Tactic/FunProp.lean index a3dfd2a7215af4..3c955ac5b077b9 100644 --- a/Mathlib/Tactic/FunProp.lean +++ b/Mathlib/Tactic/FunProp.lean @@ -214,7 +214,7 @@ There are four types of theorems that are used a bit differently. Continuous (fun x ↦ (f x).snd) := ... @[fun_prop] theorem continuous_prod_mk (f : X → Y) (g : X → Z) (hf : Continuous f) (hg : Continuous g) : - Continuous (fun x ↦ (f x, g x)) := ... + Continuous (f ⇊ g) := ... ``` - Function Theorems: diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean b/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean index dd08bd9caf1a31..8c8a560405527c 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean +++ b/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean @@ -67,7 +67,7 @@ section ProdCodomain variable [CommMonoid α] [TopologicalSpace α] [CommMonoid γ] [TopologicalSpace γ] @[to_additive HasSum.prodMk] -theorem HasProd.prodMk {f : β → α} {g : β → γ} {a : α} {b : γ} (hf : HasProd f a L) +theorem HasFunction.prod {f : β → α} {g : β → γ} {a : α} {b : γ} (hf : HasProd f a L) (hg : HasProd g b L) : HasProd (fun x ↦ (⟨f x, g x⟩ : α × γ)) ⟨a, b⟩ L := by simp [HasProd, ← prod_mk_prod, Filter.Tendsto.prodMk_nhds hf hg] diff --git a/Mathlib/Topology/Algebra/IsUniformGroup/Defs.lean b/Mathlib/Topology/Algebra/IsUniformGroup/Defs.lean index 9767b1bebd2cc1..94cffc50abf862 100644 --- a/Mathlib/Topology/Algebra/IsUniformGroup/Defs.lean +++ b/Mathlib/Topology/Algebra/IsUniformGroup/Defs.lean @@ -523,7 +523,7 @@ theorem uniformContinuous_of_tendsto_one {hom : Type*} [UniformSpace β] [Group [FunLike hom α β] [MonoidHomClass hom α β] {f : hom} (h : Tendsto f (𝓝 1) (𝓝 1)) : UniformContinuous f := by have : - ((fun x : β × β => x.2 / x.1) ∘ fun x : α × α => (f x.1, f x.2)) = fun x : α × α => + ((fun x : β × β => x.2 / x.1) ∘ Prod.map.uncurry ⇗f) = fun x : α × α => f (x.2 / x.1) := by ext; simp only [Function.comp_apply, map_div] rw [UniformContinuous, uniformity_eq_comap_nhds_one α, uniformity_eq_comap_nhds_one β, tendsto_comap_iff, this] diff --git a/Mathlib/Topology/Algebra/ProperAction/Basic.lean b/Mathlib/Topology/Algebra/ProperAction/Basic.lean index fb7302e13d1098..2c5f7d6ec0ed4d 100644 --- a/Mathlib/Topology/Algebra/ProperAction/Basic.lean +++ b/Mathlib/Topology/Algebra/ProperAction/Basic.lean @@ -139,8 +139,8 @@ theorem t2Space_of_properSMul_of_t1Group [h_proper : ProperSMul G X] [T1Space G] rw [t2_iff_isClosed_diagonal] let g := fun gx : G × X ↦ (gx.1 • gx.2, gx.2) have proper_g : IsProperMap g := (properSMul_iff G X).1 h_proper - have : g ∘ f = fun x ↦ (x, x) := by ext x <;> simp [f, g] - have range_gf : range (g ∘ f) = diagonal X := by simp [this] + have : g ∘ f = Function.diag := by ext x <;> simp [f, g] + have range_gf : range (g ∘ f) = diagonal X := range_diag rw [← range_gf] exact (proper_g.comp proper_f).isClosed_range diff --git a/Mathlib/Topology/ClopenBox.lean b/Mathlib/Topology/ClopenBox.lean index a191acd6ea765d..e22a88e7d7965c 100644 --- a/Mathlib/Topology/ClopenBox.lean +++ b/Mathlib/Topology/ClopenBox.lean @@ -61,7 +61,7 @@ theorem exists_finset_eq_sup_prod (W : Clopens (X × Y)) : rcases W.2.1.isCompact.elim_nhds_subcover (fun x ↦ U x ×ˢ V x) (fun x hx ↦ (U x ×ˢ V x).2.isOpen.mem_nhds ⟨hxU x hx, hxV x hx⟩) with ⟨I, hIW, hWI⟩ classical - use I.image fun x ↦ (U x, V x) + use I.image U ⇊ V rw [Finset.sup_image] refine le_antisymm (fun x hx ↦ ?_) (Finset.sup_le fun x hx ↦ ?_) · rcases Set.mem_iUnion₂.1 (hWI hx) with ⟨i, hi, hxi⟩ diff --git a/Mathlib/Topology/Compactness/Compact.lean b/Mathlib/Topology/Compactness/Compact.lean index cdcc570028e7e6..a32afb2e8668db 100644 --- a/Mathlib/Topology/Compactness/Compact.lean +++ b/Mathlib/Topology/Compactness/Compact.lean @@ -411,7 +411,7 @@ theorem IsCompact.mem_prod_nhdsSet_of_forall {K : Set Y} {X} {l : Filter X} {s : -- That would seem a bit more natural. theorem IsCompact.nhdsSet_inf_eq_biSup {K : Set X} (hK : IsCompact K) (l : Filter X) : (𝓝ˢ K) ⊓ l = ⨆ x ∈ K, 𝓝 x ⊓ l := by - have : ∀ f : Filter X, f ⊓ l = comap (fun x ↦ (x, x)) (f ×ˢ l) := fun f ↦ by + have : ∀ f : Filter X, f ⊓ l = comap Function.diag (f ×ˢ l) := fun f ↦ by simpa only [comap_prod] using congrArg₂ (· ⊓ ·) comap_id.symm comap_id.symm simp_rw [this, ← comap_iSup, hK.nhdsSet_prod_eq_biSup] diff --git a/Mathlib/Topology/Constructions/SumProd.lean b/Mathlib/Topology/Constructions/SumProd.lean index 004b2a64bf8222..aa3a339749c7cf 100644 --- a/Mathlib/Topology/Constructions/SumProd.lean +++ b/Mathlib/Topology/Constructions/SumProd.lean @@ -60,93 +60,96 @@ variable [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [Topolog [TopologicalSpace ε] [TopologicalSpace ζ] @[simp] -theorem continuous_prodMk {f : X → Y} {g : X → Z} : - (Continuous fun x => (f x, g x)) ↔ Continuous f ∧ Continuous g := +theorem continuous_prod {f : X → Y} {g : X → Z} : + (Continuous (f ⇊ g)) ↔ Continuous f ∧ Continuous g := continuous_inf_rng.trans <| continuous_induced_rng.and continuous_induced_rng +@[continuity, fun_prop] +theorem Continuous.prod {f : Z → X} {g : Z → Y} (hf : Continuous f) (hg : Continuous g) : + Continuous (f ⇊ g) := continuous_prod.2 ⟨hf, hg⟩ + +@[continuity, fun_prop] +theorem Continuous.fst_of_prod {f : Z → X} {g : Z → Y} (hfg : Continuous (f ⇊ g)) : + Continuous f := (continuous_prod.1 hfg).1 + +@[continuity, fun_prop] +theorem Continuous.snd_of_prod {f : Z → X} {g : Z → Y} (hfg : Continuous (f ⇊ g)) : + Continuous g := (continuous_prod.1 hfg).2 + +@[continuity, fun_prop] +theorem continuous_fst : Continuous (@Prod.fst X Y) := continuous_id.fst_of_prod + +@[continuity, fun_prop] +theorem continuous_snd : Continuous (@Prod.snd X Y) := continuous_id.snd_of_prod + +@[continuity, fun_prop] +theorem Continuous.prodMk : + Continuous (Prod.mk.uncurry (α := X) (β := Y)) := continuous_fst.prod continuous_snd + @[continuity] -theorem continuous_fst : Continuous (@Prod.fst X Y) := - (continuous_prodMk.1 continuous_id).1 +theorem Continuous.prod_right (x : X) : Continuous (Prod.mk (β := Y) x) := + Continuous.prodMk.comp (continuous_const.prod continuous_id) + +@[continuity] +theorem Continuous.prod_left (y : Y) : Continuous (Prod.mk (α := X) · y) := + Continuous.prodMk.comp (continuous_id.prod continuous_const) /-- Postcomposing `f` with `Prod.fst` is continuous -/ @[fun_prop] -theorem Continuous.fst {f : X → Y × Z} (hf : Continuous f) : Continuous fun x : X => (f x).1 := - continuous_fst.comp hf +theorem Continuous.fst {f : X → Y × Z} (hf : Continuous f) : Continuous (Prod.fst ∘ f) := by + fun_prop /-- Precomposing `f` with `Prod.fst` is continuous -/ -theorem Continuous.fst' {f : X → Z} (hf : Continuous f) : Continuous fun x : X × Y => f x.fst := - hf.comp continuous_fst +theorem Continuous.fst' {f : X → Z} (hf : Continuous f) : Continuous (f ∘ Prod.fst (β := Y)) := by + fun_prop -theorem continuousAt_fst {p : X × Y} : ContinuousAt Prod.fst p := - continuous_fst.continuousAt +theorem continuousAt_fst {p : X × Y} : ContinuousAt Prod.fst p := by fun_prop /-- Postcomposing `f` with `Prod.fst` is continuous at `x` -/ @[fun_prop] theorem ContinuousAt.fst {f : X → Y × Z} {x : X} (hf : ContinuousAt f x) : - ContinuousAt (fun x : X => (f x).1) x := - continuousAt_fst.comp hf + ContinuousAt (Prod.fst ∘ f) x := by fun_prop /-- Precomposing `f` with `Prod.fst` is continuous at `(x, y)` -/ theorem ContinuousAt.fst' {f : X → Z} {x : X} {y : Y} (hf : ContinuousAt f x) : - ContinuousAt (fun x : X × Y => f x.fst) (x, y) := - ContinuousAt.comp hf continuousAt_fst + ContinuousAt (f ∘ Prod.fst) (x, y) := by fun_prop /-- Precomposing `f` with `Prod.fst` is continuous at `x : X × Y` -/ theorem ContinuousAt.fst'' {f : X → Z} {x : X × Y} (hf : ContinuousAt f x.fst) : - ContinuousAt (fun x : X × Y => f x.fst) x := - hf.comp continuousAt_fst + ContinuousAt (f ∘ Prod.fst) x := by fun_prop theorem Filter.Tendsto.fst_nhds {X} {l : Filter X} {f : X → Y × Z} {p : Y × Z} - (h : Tendsto f l (𝓝 p)) : Tendsto (fun a ↦ (f a).1) l (𝓝 <| p.1) := + (h : Tendsto f l (𝓝 p)) : Tendsto (Prod.fst ∘ f) l (𝓝 <| p.1) := continuousAt_fst.tendsto.comp h -@[continuity] -theorem continuous_snd : Continuous (@Prod.snd X Y) := - (continuous_prodMk.1 continuous_id).2 - /-- Postcomposing `f` with `Prod.snd` is continuous -/ @[fun_prop] -theorem Continuous.snd {f : X → Y × Z} (hf : Continuous f) : Continuous fun x : X => (f x).2 := - continuous_snd.comp hf +theorem Continuous.snd {f : X → Y × Z} (hf : Continuous f) : Continuous (Prod.snd ∘ f) := by + fun_prop /-- Precomposing `f` with `Prod.snd` is continuous -/ -theorem Continuous.snd' {f : Y → Z} (hf : Continuous f) : Continuous fun x : X × Y => f x.snd := - hf.comp continuous_snd +theorem Continuous.snd' {f : Y → Z} (hf : Continuous f) : Continuous (f ∘ Prod.snd (α := X)) := by + fun_prop -theorem continuousAt_snd {p : X × Y} : ContinuousAt Prod.snd p := - continuous_snd.continuousAt +theorem continuousAt_snd {p : X × Y} : ContinuousAt Prod.snd p := by fun_prop /-- Postcomposing `f` with `Prod.snd` is continuous at `x` -/ @[fun_prop] theorem ContinuousAt.snd {f : X → Y × Z} {x : X} (hf : ContinuousAt f x) : - ContinuousAt (fun x : X => (f x).2) x := - continuousAt_snd.comp hf + ContinuousAt (Prod.snd ∘ f) x := by fun_prop /-- Precomposing `f` with `Prod.snd` is continuous at `(x, y)` -/ theorem ContinuousAt.snd' {f : Y → Z} {x : X} {y : Y} (hf : ContinuousAt f y) : - ContinuousAt (fun x : X × Y => f x.snd) (x, y) := - ContinuousAt.comp hf continuousAt_snd + ContinuousAt (f ∘ Prod.snd) (x, y) := by fun_prop /-- Precomposing `f` with `Prod.snd` is continuous at `x : X × Y` -/ theorem ContinuousAt.snd'' {f : Y → Z} {x : X × Y} (hf : ContinuousAt f x.snd) : - ContinuousAt (fun x : X × Y => f x.snd) x := - hf.comp continuousAt_snd + ContinuousAt (f ∘ Prod.snd) x := by fun_prop theorem Filter.Tendsto.snd_nhds {X} {l : Filter X} {f : X → Y × Z} {p : Y × Z} - (h : Tendsto f l (𝓝 p)) : Tendsto (fun a ↦ (f a).2) l (𝓝 <| p.2) := + (h : Tendsto f l (𝓝 p)) : Tendsto (Prod.snd ∘ f) l (𝓝 <| p.2) := continuousAt_snd.tendsto.comp h -@[continuity, fun_prop] -theorem Continuous.prodMk {f : Z → X} {g : Z → Y} (hf : Continuous f) (hg : Continuous g) : - Continuous fun x => (f x, g x) := - continuous_prodMk.2 ⟨hf, hg⟩ - -@[continuity] -theorem Continuous.prodMk_right (x : X) : Continuous fun y : Y => (x, y) := by fun_prop - -@[continuity] -theorem Continuous.prodMk_left (y : Y) : Continuous fun x : X => (x, y) := by fun_prop - /-- If `f x y` is continuous in `x` for all `y ∈ s`, then the set of `x` such that `f x` maps `s` to `t` is closed. -/ lemma IsClosed.setOf_mapsTo {α : Type*} {f : X → α → Z} {s : Set α} {t : Set Z} (ht : IsClosed t) @@ -155,22 +158,22 @@ lemma IsClosed.setOf_mapsTo {α : Type*} {f : X → α → Z} {s : Set α} {t : theorem Continuous.comp₂ {g : X × Y → Z} (hg : Continuous g) {e : W → X} (he : Continuous e) {f : W → Y} (hf : Continuous f) : Continuous fun w => g (e w, f w) := - hg.comp <| he.prodMk hf + hg.comp <| he.prod hf theorem Continuous.comp₃ {g : X × Y × Z → ε} (hg : Continuous g) {e : W → X} (he : Continuous e) {f : W → Y} (hf : Continuous f) {k : W → Z} (hk : Continuous k) : Continuous fun w => g (e w, f w, k w) := - hg.comp₂ he <| hf.prodMk hk + hg.comp₂ he <| hf.prod hk theorem Continuous.comp₄ {g : X × Y × Z × ζ → ε} (hg : Continuous g) {e : W → X} (he : Continuous e) {f : W → Y} (hf : Continuous f) {k : W → Z} (hk : Continuous k) {l : W → ζ} (hl : Continuous l) : Continuous fun w => g (e w, f w, k w, l w) := - hg.comp₃ he hf <| hk.prodMk hl + hg.comp₃ he hf <| hk.prod hl @[continuity, fun_prop] theorem Continuous.prodMap {f : Z → X} {g : W → Y} (hf : Continuous f) (hg : Continuous g) : Continuous (Prod.map f g) := - hf.fst'.prodMk hg.snd' + hf.fst'.prod hg.snd' /-- A version of `continuous_inf_dom_left` for binary functions -/ theorem continuous_inf_dom_left₂ {X Y Z} {f : X → Y → Z} {ta1 ta2 : TopologicalSpace X} @@ -212,13 +215,13 @@ theorem Filter.Eventually.prod_inr_nhds {p : Y → Prop} {y : Y} (h : ∀ᶠ x i ∀ᶠ x in 𝓝 (x, y), p (x : X × Y).2 := continuousAt_snd h -theorem Filter.Eventually.prodMk_nhds {px : X → Prop} {x} (hx : ∀ᶠ x in 𝓝 x, px x) {py : Y → Prop} +theorem Filter.Eventually.prod_nhds {px : X → Prop} {x} (hx : ∀ᶠ x in 𝓝 x, px x) {py : Y → Prop} {y} (hy : ∀ᶠ y in 𝓝 y, py y) : ∀ᶠ p in 𝓝 (x, y), px (p : X × Y).1 ∧ py p.2 := (hx.prod_inl_nhds y).and (hy.prod_inr_nhds x) @[fun_prop] theorem continuous_swap : Continuous (Prod.swap : X × Y → Y × X) := - continuous_snd.prodMk continuous_fst + continuous_snd.prod continuous_fst lemma isClosedMap_swap : IsClosedMap (Prod.swap : X × Y → Y × X) := fun s hs ↦ by rw [image_swap_eq_preimage_swap] @@ -226,11 +229,11 @@ lemma isClosedMap_swap : IsClosedMap (Prod.swap : X × Y → Y × X) := fun s hs theorem Continuous.uncurry_left {f : X → Y → Z} (x : X) (h : Continuous (uncurry f)) : Continuous (f x) := - h.comp (.prodMk_right _) + h.comp (.prod_right _) theorem Continuous.uncurry_right {f : X → Y → Z} (y : Y) (h : Continuous (uncurry f)) : Continuous fun a => f a y := - h.comp (.prodMk_left _) + h.comp (.prod_left _) theorem continuous_curry {g : X × Y → Z} (x : X) (h : Continuous g) : Continuous (curry g x) := Continuous.uncurry_left x h @@ -307,7 +310,7 @@ theorem isOpen_setOf_disjoint_nhds_nhds : IsOpen { p : X × X | Disjoint (𝓝 p exact mem_nhds_prod_iff'.mpr ⟨U, V, hU.2, hU.1, hV.2, hV.1, fun ⟨x', y'⟩ ⟨hx', hy'⟩ => disjoint_of_disjoint_of_mem hd (hU.2.mem_nhds hx') (hV.2.mem_nhds hy')⟩ -theorem Filter.Eventually.prod_nhds {p : X → Prop} {q : Y → Prop} {x : X} {y : Y} +theorem Filter.Eventually.prodMk_nhds {p : X → Prop} {q : Y → Prop} {x : X} {y : Y} (hx : ∀ᶠ x in 𝓝 x, p x) (hy : ∀ᶠ y in 𝓝 y, q y) : ∀ᶠ z : X × Y in 𝓝 (x, y), p z.1 ∧ q z.2 := prod_mem_nhds hx hy @@ -326,11 +329,11 @@ theorem Filter.EventuallyLE.prodMap_nhds {α β : Type*} [LE α] [LE β] {f₁ f theorem nhds_swap (x : X) (y : Y) : 𝓝 (x, y) = (𝓝 (y, x)).map Prod.swap := by rw [nhds_prod_eq, Filter.prod_comm, nhds_prod_eq] -theorem Filter.Tendsto.prodMk_nhds {γ} {x : X} {y : Y} {f : Filter γ} {mx : γ → X} {my : γ → Y} +theorem Filter.Tendsto.prod_nhds {γ} {x : X} {y : Y} {f : Filter γ} {mx : γ → X} {my : γ → Y} (hx : Tendsto mx f (𝓝 x)) (hy : Tendsto my f (𝓝 y)) : Tendsto (fun c => (mx c, my c)) f (𝓝 (x, y)) := by rw [nhds_prod_eq] - exact hx.prodMk hy + exact hx.prod hy theorem Filter.Tendsto.prodMap_nhds {x : X} {y : Y} {z : Z} {w : W} {f : X → Y} {g : Z → W} (hf : Tendsto f (𝓝 x) (𝓝 y)) (hg : Tendsto g (𝓝 z) (𝓝 w)) : @@ -344,13 +347,13 @@ theorem Filter.Eventually.curry_nhds {p : X × Y → Prop} {x : X} {y : Y} exact h.curry @[fun_prop] -theorem ContinuousAt.prodMk {f : X → Y} {g : X → Z} {x : X} (hf : ContinuousAt f x) - (hg : ContinuousAt g x) : ContinuousAt (fun x => (f x, g x)) x := - hf.prodMk_nhds hg +theorem ContinuousAt.prod {f : X → Y} {g : X → Z} {x : X} (hf : ContinuousAt f x) + (hg : ContinuousAt g x) : ContinuousAt (Function.prod f g) x := + hf.prod_nhds hg theorem ContinuousAt.prodMap {f : X → Z} {g : Y → W} {p : X × Y} (hf : ContinuousAt f p.fst) (hg : ContinuousAt g p.snd) : ContinuousAt (Prod.map f g) p := - hf.fst''.prodMk hg.snd'' + hf.fst''.prod hg.snd'' /-- A version of `ContinuousAt.prodMap` that avoids `Prod.fst`/`Prod.snd` by assuming that the point is `(x, y)`. -/ @@ -361,7 +364,7 @@ theorem ContinuousAt.prodMap' {f : X → Z} {g : Y → W} {x : X} {y : Y} (hf : theorem ContinuousAt.comp₂ {f : Y × Z → W} {g : X → Y} {h : X → Z} {x : X} (hf : ContinuousAt f (g x, h x)) (hg : ContinuousAt g x) (hh : ContinuousAt h x) : ContinuousAt (fun x ↦ f (g x, h x)) x := - ContinuousAt.comp hf (hg.prodMk hh) + ContinuousAt.comp hf (hg.prod hh) theorem ContinuousAt.comp₂_of_eq {f : Y × Z → W} {g : X → Y} {h : X → Z} {x : X} {y : Y × Z} (hf : ContinuousAt f y) (hg : ContinuousAt g x) (hh : ContinuousAt h x) (e : (g x, h x) = y) : @@ -372,13 +375,13 @@ theorem ContinuousAt.comp₂_of_eq {f : Y × Z → W} {g : X → Y} {h : X → Z /-- Continuous functions on products are continuous in their first argument -/ theorem Continuous.curry_left {f : X × Y → Z} (hf : Continuous f) {y : Y} : Continuous fun x ↦ f (x, y) := - hf.comp (.prodMk_left _) + hf.comp (.prod_left _) alias Continuous.along_fst := Continuous.curry_left /-- Continuous functions on products are continuous in their second argument -/ theorem Continuous.curry_right {f : X × Y → Z} (hf : Continuous f) {x : X} : Continuous fun y ↦ f (x, y) := - hf.comp (.prodMk_right _) + hf.comp (.prod_right _) alias Continuous.along_snd := Continuous.curry_right -- todo: prove a version of `generateFrom_union` with `image2 (∩) s t` in the LHS and use it here @@ -572,10 +575,10 @@ lemma Topology.isInducing_prod_const {y : Y} {f : X → Z} : Function.comp_def, induced_const, inf_top_eq] lemma isInducing_prodMkLeft (y : Y) : IsInducing (fun x : X ↦ (x, y)) := - .of_comp (.prodMk_left y) continuous_fst .id + .of_comp (.prod_left y) continuous_fst .id lemma isInducing_prodMkRight (x : X) : IsInducing (Prod.mk x : Y → X × Y) := - .of_comp (.prodMk_right x) continuous_snd .id + .of_comp (.prod_right x) continuous_snd .id lemma Topology.IsEmbedding.prodMap {f : X → Y} {g : Z → W} (hf : IsEmbedding f) (hg : IsEmbedding g) : IsEmbedding (Prod.map f g) where @@ -594,13 +597,13 @@ protected lemma Topology.IsOpenEmbedding.prodMap {f : X → Y} {g : Z → W} (hf .of_isEmbedding_isOpenMap (hf.1.prodMap hg.1) (hf.isOpenMap.prodMap hg.isOpenMap) lemma isEmbedding_graph {f : X → Y} (hf : Continuous f) : IsEmbedding fun x => (x, f x) := - .of_comp (continuous_id.prodMk hf) continuous_fst .id + .of_comp (continuous_id.prod hf) continuous_fst .id lemma isEmbedding_prodMkLeft (y : Y) : IsEmbedding (fun x : X ↦ (x, y)) := - .of_comp (.prodMk_left y) continuous_fst .id + .of_comp (.prod_left y) continuous_fst .id lemma isEmbedding_prodMkRight (x : X) : IsEmbedding (Prod.mk x : Y → X × Y) := - .of_comp (.prodMk_right x) continuous_snd .id + .of_comp (.prod_right x) continuous_snd .id theorem IsOpenQuotientMap.prodMap {f : X → Y} {g : Z → W} (hf : IsOpenQuotientMap f) (hg : IsOpenQuotientMap g) : IsOpenQuotientMap (Prod.map f g) := diff --git a/Mathlib/Topology/ContinuousOn.lean b/Mathlib/Topology/ContinuousOn.lean index f1a9f9c1334284..e5edc8e7cce1b2 100644 --- a/Mathlib/Topology/ContinuousOn.lean +++ b/Mathlib/Topology/ContinuousOn.lean @@ -577,12 +577,12 @@ theorem ContinuousOn.image_closure (hf : ContinuousOn f (closure s)) : theorem ContinuousWithinAt.prodMk {f : α → β} {g : α → γ} {s : Set α} {x : α} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) : - ContinuousWithinAt (fun x => (f x, g x)) s x := + ContinuousWithinAt (Function.prod f g) s x := hf.prodMk_nhds hg @[fun_prop] theorem ContinuousOn.prodMk {f : α → β} {g : α → γ} {s : Set α} (hf : ContinuousOn f s) - (hg : ContinuousOn g s) : ContinuousOn (fun x => (f x, g x)) s := fun x hx => + (hg : ContinuousOn g s) : ContinuousOn (Function.prod f g) s := fun x hx => (hf x hx).prodMk (hg x hx) theorem continuousOn_fst {s : Set (α × β)} : ContinuousOn Prod.fst s := diff --git a/Mathlib/Topology/EMetricSpace/Lipschitz.lean b/Mathlib/Topology/EMetricSpace/Lipschitz.lean index 8e37ed75fa5d38..e161593eeb3e4b 100644 --- a/Mathlib/Topology/EMetricSpace/Lipschitz.lean +++ b/Mathlib/Topology/EMetricSpace/Lipschitz.lean @@ -244,7 +244,7 @@ protected theorem prod_snd : LipschitzWith 1 (@Prod.snd α β) := /-- If `f` and `g` are Lipschitz functions, so is the induced map `f × g` to the product type. -/ protected theorem prodMk {f : α → β} {Kf : ℝ≥0} (hf : LipschitzWith Kf f) {g : α → γ} {Kg : ℝ≥0} - (hg : LipschitzWith Kg g) : LipschitzWith (max Kf Kg) fun x => (f x, g x) := by + (hg : LipschitzWith Kg g) : LipschitzWith (max Kf Kg) Function.prod f g := by intro x y rw [ENNReal.coe_mono.map_max, Prod.edist_eq, max_mul] exact max_le_max (hf x y) (hg x y) @@ -331,7 +331,7 @@ protected theorem comp {g : β → γ} {t : Set β} {Kg : ℝ≥0} (hg : Lipschi /-- If `f` and `g` are Lipschitz on `s`, so is the induced map `f × g` to the product type. -/ protected theorem prodMk {g : α → γ} {Kf Kg : ℝ≥0} (hf : LipschitzOnWith Kf f s) - (hg : LipschitzOnWith Kg g s) : LipschitzOnWith (max Kf Kg) (fun x => (f x, g x)) s := by + (hg : LipschitzOnWith Kg g s) : LipschitzOnWith (max Kf Kg) (Function.prod f g) s := by intro _ hx _ hy rw [ENNReal.coe_mono.map_max, Prod.edist_eq, max_mul] exact max_le_max (hf hx hy) (hg hx hy) @@ -385,7 +385,7 @@ protected lemma comp {f : β → γ} {g : α → β} /-- If `f` and `g` are locally Lipschitz, so is the induced map `f × g` to the product type. -/ protected lemma prodMk {f : α → β} (hf : LocallyLipschitz f) {g : α → γ} (hg : LocallyLipschitz g) : - LocallyLipschitz fun x => (f x, g x) := by + LocallyLipschitz Function.prod f g := by intro x rcases hf x with ⟨Kf, t₁, h₁t, hfL⟩ rcases hg x with ⟨Kg, t₂, h₂t, hgL⟩ diff --git a/Mathlib/Topology/UniformSpace/Basic.lean b/Mathlib/Topology/UniformSpace/Basic.lean index 890f5efd1ed61d..b8a3ed7a253362 100644 --- a/Mathlib/Topology/UniformSpace/Basic.lean +++ b/Mathlib/Topology/UniformSpace/Basic.lean @@ -1073,9 +1073,9 @@ lemma exists_is_open_mem_uniformity_of_forall_mem_eq end Uniform theorem Filter.Tendsto.congr_uniformity {α β} [UniformSpace β] {f g : α → β} {l : Filter α} {b : β} - (hf : Tendsto f l (𝓝 b)) (hg : Tendsto (fun x => (f x, g x)) l (𝓤 β)) : Tendsto g l (𝓝 b) := + (hf : Tendsto f l (𝓝 b)) (hg : Tendsto (Function.prod f g) l (𝓤 β)) : Tendsto g l (𝓝 b) := Uniform.tendsto_nhds_right.2 <| (Uniform.tendsto_nhds_right.1 hf).uniformity_trans hg theorem Uniform.tendsto_congr {α β} [UniformSpace β] {f g : α → β} {l : Filter α} {b : β} - (hfg : Tendsto (fun x => (f x, g x)) l (𝓤 β)) : Tendsto f l (𝓝 b) ↔ Tendsto g l (𝓝 b) := + (hfg : Tendsto (Function.prod f g) l (𝓤 β)) : Tendsto f l (𝓝 b) ↔ Tendsto g l (𝓝 b) := ⟨fun h => h.congr_uniformity hfg, fun h => h.congr_uniformity hfg.uniformity_symm⟩ diff --git a/Mathlib/Topology/UniformSpace/Defs.lean b/Mathlib/Topology/UniformSpace/Defs.lean index f4adcf7562c83b..8ca5185671be67 100644 --- a/Mathlib/Topology/UniformSpace/Defs.lean +++ b/Mathlib/Topology/UniformSpace/Defs.lean @@ -491,21 +491,21 @@ theorem tendsto_swap_uniformity : Tendsto (@Prod.swap α α) (𝓤 α) (𝓤 α) theorem comp_mem_uniformity_sets {s : SetRel α α} (hs : s ∈ 𝓤 α) : ∃ t ∈ 𝓤 α, t ○ t ⊆ s := (mem_lift'_sets <| monotone_id.relComp monotone_id).mp <| comp_le_uniformity hs -/-- Relation `fun f g ↦ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)` is transitive. -/ +/-- Relation `fun f g ↦ Tendsto (f ⇊ g) l (𝓤 α)` is transitive. -/ theorem Filter.Tendsto.uniformity_trans {l : Filter β} {f₁ f₂ f₃ : β → α} - (h₁₂ : Tendsto (fun x => (f₁ x, f₂ x)) l (𝓤 α)) - (h₂₃ : Tendsto (fun x => (f₂ x, f₃ x)) l (𝓤 α)) : Tendsto (fun x => (f₁ x, f₃ x)) l (𝓤 α) := by + (h₁₂ : Tendsto (f₁ ⇊ f₂) l (𝓤 α)) + (h₂₃ : Tendsto (f₂ ⇊ f₃) l (𝓤 α)) : Tendsto (f₁ ⇊ f₃) l (𝓤 α) := by refine le_trans (le_lift'.2 fun s hs => mem_map.2 ?_) comp_le_uniformity filter_upwards [mem_map.1 (h₁₂ hs), mem_map.1 (h₂₃ hs)] with x hx₁₂ hx₂₃ using ⟨_, hx₁₂, hx₂₃⟩ -/-- Relation `fun f g ↦ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)` is symmetric. -/ +/-- Relation `fun f g ↦ Tendsto (f ⇊ g) l (𝓤 α)` is symmetric. -/ theorem Filter.Tendsto.uniformity_symm {l : Filter β} {f : β → α × α} (h : Tendsto f l (𝓤 α)) : - Tendsto (fun x => ((f x).2, (f x).1)) l (𝓤 α) := + Tendsto (Prod.swap ∘ f) l (𝓤 α) := tendsto_swap_uniformity.comp h -/-- Relation `fun f g ↦ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)` is reflexive. -/ +/-- Relation `fun f g ↦ Tendsto (f ⇊ g) l (𝓤 α)` is reflexive. -/ theorem tendsto_diag_uniformity (f : β → α) (l : Filter β) : - Tendsto (fun x => (f x, f x)) l (𝓤 α) := fun _s hs => + Tendsto (Function.diag ∘ f) l (𝓤 α) := fun _s hs => mem_map.2 <| univ_mem' fun _ => refl_mem_uniformity hs theorem tendsto_const_uniformity {a : α} {f : Filter β} : Tendsto (fun _ => (a, a)) f (𝓤 α) := @@ -805,7 +805,7 @@ variable [UniformSpace β] as `(x, y)` tends to the diagonal. In other words, if `x` is sufficiently close to `y`, then `f x` is close to `f y` no matter where `x` and `y` are located in `α`. -/ def UniformContinuous (f : α → β) := - Tendsto (fun x : α × α => (f x.1, f x.2)) (𝓤 α) (𝓤 β) + Tendsto (Prod.map.uncurry ⇗f) (𝓤 α) (𝓤 β) /-- Notation for uniform continuity with respect to non-standard `UniformSpace` instances. -/ scoped[Uniformity] notation "UniformContinuous[" u₁ ", " u₂ "]" => @UniformContinuous _ _ u₁ u₂ @@ -815,7 +815,7 @@ the diagonal as `(x, y)` tends to the diagonal while remaining in `s ×ˢ s`. In other words, if `x` is sufficiently close to `y`, then `f x` is close to `f y` no matter where `x` and `y` are located in `s`. -/ def UniformContinuousOn (f : α → β) (s : Set α) : Prop := - Tendsto (fun x : α × α => (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (𝓤 β) + Tendsto (Prod.map.uncurry ⇗f) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (𝓤 β) theorem uniformContinuous_def {f : α → β} : UniformContinuous f ↔ ∀ r ∈ 𝓤 β, { x : α × α | (f x.1, f x.2) ∈ r } ∈ 𝓤 α := @@ -831,9 +831,9 @@ theorem uniformContinuousOn_univ {f : α → β} : theorem uniformContinuous_of_const {c : α → β} (h : ∀ a b, c a = c b) : UniformContinuous c := - have : (fun x : α × α => (c x.fst, c x.snd)) ⁻¹' SetRel.id = univ := - eq_univ_iff_forall.2 fun ⟨a, b⟩ => h a b - le_trans (map_le_iff_le_comap.2 <| by simp [comap_principal, this]) refl_le_uniformity + have H : Prod.map.uncurry ⇗c ⁻¹' SetRel.id = univ := eq_univ_iff_forall.2 (by simpa using h) + (le_principal_iff.mpr <| mem_map.mpr <| Set.mem_of_eq_of_mem H Filter.univ_mem).trans + refl_le_uniformity theorem uniformContinuous_id : UniformContinuous (@id α) := tendsto_id @@ -856,7 +856,8 @@ theorem Filter.HasBasis.uniformContinuous_iff {ι'} {p : ι → Prop} {s : ι → SetRel α α} (ha : (𝓤 α).HasBasis p s) {q : ι' → Prop} {t : ι' → Set (β × β)} (hb : (𝓤 β).HasBasis q t) {f : α → β} : UniformContinuous f ↔ ∀ i, q i → ∃ j, p j ∧ ∀ x y, (x, y) ∈ s j → (f x, f y) ∈ t i := - (ha.tendsto_iff hb).trans <| by simp only [Prod.forall] + (ha.tendsto_iff hb).trans <| by simp only [Function.uncurry_apply, Function.fst_diag, + Function.snd_diag, Prod.forall, Prod.map_apply] theorem Filter.HasBasis.uniformContinuousOn_iff {ι'} {p : ι → Prop} {s : ι → SetRel α α} (ha : (𝓤 α).HasBasis p s) {q : ι' → Prop} {t : ι' → Set (β × β)} @@ -864,7 +865,8 @@ theorem Filter.HasBasis.uniformContinuousOn_iff {ι'} {p : ι → Prop} UniformContinuousOn f S ↔ ∀ i, q i → ∃ j, p j ∧ ∀ x, x ∈ S → ∀ y, y ∈ S → (x, y) ∈ s j → (f x, f y) ∈ t i := ((ha.inf_principal (S ×ˢ S)).tendsto_iff hb).trans <| by - simp_rw [Prod.forall, Set.inter_comm (s _), forall_mem_comm, mem_inter_iff, mem_prod, and_imp] + simp_rw [Set.inter_comm (s _), mem_inter_iff, mem_prod, Function.uncurry_apply, + Function.fst_diag, Function.snd_diag, and_imp, Prod.forall, Prod.map_apply, forall_mem_comm] /-- A map `f : α → β` between uniform spaces is called *uniform inducing* if the uniformity filter on `α` is the pullback of the uniformity filter on `β` under `Prod.map f f`. If `α` is a separated diff --git a/Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean b/Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean index 2170661fd474fb..02422a7037b04d 100644 --- a/Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean +++ b/Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean @@ -200,7 +200,7 @@ end Comp theorem TendstoLocallyUniformlyOn.prodMk [UniformSpace γ] {G : ι → α → γ} {g : α → γ} (hF : TendstoLocallyUniformlyOn F f p s) (hG : TendstoLocallyUniformlyOn G g p s) : - TendstoLocallyUniformlyOn (fun n x ↦ (F n x, G n x)) (fun x ↦ (f x, g x)) p s := by + TendstoLocallyUniformlyOn (fun n x ↦ (F n x, G n x)) (f ⇊ g) p s := by rw [tendstoLocallyUniformlyOn_iff_forall_tendsto] at * intro x hx rw [uniformity_prod_eq_comap_prod, tendsto_comap_iff] @@ -213,7 +213,7 @@ theorem TendstoLocallyUniformlyOn.piProd [UniformSpace γ] {G : ι → α → γ theorem TendstoLocallyUniformly.prodMk [UniformSpace γ] {G : ι → α → γ} {g : α → γ} (hF : TendstoLocallyUniformly F f p) (hG : TendstoLocallyUniformly G g p) : - TendstoLocallyUniformly (fun n x ↦ (F n x, G n x)) (fun x ↦ (f x, g x)) p := by + TendstoLocallyUniformly (fun n x ↦ (F n x, G n x)) (f ⇊ g) p := by rw [← tendstoLocallyUniformlyOn_univ] at * exact hF.prodMk hG diff --git a/Mathlib/Topology/UniformSpace/Separation.lean b/Mathlib/Topology/UniformSpace/Separation.lean index f98785563d78df..0f5e601585dad6 100644 --- a/Mathlib/Topology/UniformSpace/Separation.lean +++ b/Mathlib/Topology/UniformSpace/Separation.lean @@ -207,7 +207,7 @@ theorem eq_of_clusterPt_uniformity [T0Space α] {x y : α} (h : ClusterPt (x, y) theorem Filter.Tendsto.inseparable_iff_uniformity {β} {l : Filter β} [NeBot l] {f g : β → α} {a b : α} (ha : Tendsto f l (𝓝 a)) (hb : Tendsto g l (𝓝 b)) : - Inseparable a b ↔ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α) := by + Inseparable a b ↔ Tendsto (f ⇊ g) l (𝓤 α) := by refine ⟨fun h ↦ (ha.prodMk_nhds hb).mono_right h.nhds_le_uniformity, fun h ↦ ?_⟩ rw [inseparable_iff_clusterPt_uniformity] exact (ClusterPt.of_le_nhds (ha.prodMk_nhds hb)).mono h diff --git a/Mathlib/Topology/UniformSpace/UniformConvergence.lean b/Mathlib/Topology/UniformSpace/UniformConvergence.lean index be119d39d3a840..7e6d93000dd153 100644 --- a/Mathlib/Topology/UniformSpace/UniformConvergence.lean +++ b/Mathlib/Topology/UniformSpace/UniformConvergence.lean @@ -290,12 +290,12 @@ protected theorem TendstoUniformlyOn.prodMk {ι' β' : Type*} [UniformSpace β'] (h' : TendstoUniformlyOn F' f' p' s) : TendstoUniformlyOn (fun (i : ι × ι') a => (F i.1 a, F' i.2 a)) (fun a => (f a, f' a)) (p ×ˢ p') s := - (congr_arg _ s.inter_self).mp ((h.prodMap h').comp fun a => (a, a)) + (congr_arg _ s.inter_self).mp ((h.prodMap h').comp Function.diag) theorem TendstoUniformly.prodMk {ι' β' : Type*} [UniformSpace β'] {F' : ι' → α → β'} {f' : α → β'} {p' : Filter ι'} (h : TendstoUniformly F f p) (h' : TendstoUniformly F' f' p') : TendstoUniformly (fun (i : ι × ι') a => (F i.1 a, F' i.2 a)) (fun a => (f a, f' a)) (p ×ˢ p') := - (h.prodMap h').comp fun a => (a, a) + (h.prodMap h').comp Function.diag /-- Uniform convergence on a filter `p'` to a constant function is equivalent to convergence in `p ×ˢ p'`. -/ @@ -542,12 +542,12 @@ theorem UniformCauchySeqOn.prodMap {ι' α' β' : Type*} [UniformSpace β'] {F' theorem UniformCauchySeqOn.prod {ι' β' : Type*} [UniformSpace β'] {F' : ι' → α → β'} {p' : Filter ι'} (h : UniformCauchySeqOn F p s) (h' : UniformCauchySeqOn F' p' s) : UniformCauchySeqOn (fun (i : ι × ι') a => (F i.fst a, F' i.snd a)) (p ×ˢ p') s := - (congr_arg _ s.inter_self).mp ((h.prodMap h').comp fun a => (a, a)) + (congr_arg _ s.inter_self).mp ((h.prodMap h').comp Function.diag) theorem UniformCauchySeqOn.prod' {β' : Type*} [UniformSpace β'] {F' : ι → α → β'} (h : UniformCauchySeqOn F p s) (h' : UniformCauchySeqOn F' p s) : UniformCauchySeqOn (fun (i : ι) a => (F i a, F' i a)) p s := fun u hu => - have hh : Tendsto (fun x : ι => (x, x)) p (p ×ˢ p) := tendsto_diag + have hh : Tendsto Function.diag p (p ×ˢ p) := tendsto_diag (hh.prodMap hh).eventually ((h.prod h') u hu) /-- If a sequence of functions is uniformly Cauchy on a set, then the values at each point form diff --git a/MathlibTest/Continuity.lean b/MathlibTest/Continuity.lean index 9eaa064c713956..dba115d41095af 100644 --- a/MathlibTest/Continuity.lean +++ b/MathlibTest/Continuity.lean @@ -51,7 +51,7 @@ example (b : Y) : Continuous (fun _ : X => b) := by continuity example (f : C(X, Y)) (g : C(Y, Z)) : Continuous (g ∘ f) := by continuity -example (f : C(X, Y)) (g : C(X, Z)) : Continuous (fun x => (f x, g x)) := by continuity +example (f : C(X, Y)) (g : C(X, Z)) : Continuous (Function.prod f g) := by continuity example (f : C(X, Y)) (g : C(W, Z)) : Continuous (Prod.map f g) := by continuity diff --git a/MathlibTest/DifferentialGeometry/Notation/Basic.lean b/MathlibTest/DifferentialGeometry/Notation/Basic.lean index 2976d90b7c9fc8..9efbd036b6a4f9 100644 --- a/MathlibTest/DifferentialGeometry/Notation/Basic.lean +++ b/MathlibTest/DifferentialGeometry/Notation/Basic.lean @@ -1067,7 +1067,7 @@ section product /-- info: MDifferentiable I (I'.prod I') fun x ↦ Prod.mk (f x) (g x) : Prop -/ #guard_msgs in -#check MDiff (fun x ↦ (f x, g x)) +#check MDiff (f ⇊ g) /-- info: MDifferentiable (I.prod (modelWithCornersSelf 𝕜 E)) I' k : Prop -/ #guard_msgs in diff --git a/MathlibTest/fun_prop.lean b/MathlibTest/fun_prop.lean index b730948c2830a5..ea31f74b8ff205 100644 --- a/MathlibTest/fun_prop.lean +++ b/MathlibTest/fun_prop.lean @@ -50,7 +50,7 @@ Let's mark the product constructor. -/ attribute [fun_prop] - Measurable.prodMk -- Measurable f → Measurable g → Measurable fun x => (f x, g x) + Measurable.prodMk -- Measurable f → Measurable g → Measurable Function.prod f g /-! When it comes to product projection, their properties are usually stated in two different ways