From eba7871095e834365616b5e43c8c7bb0b37058d0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Wed, 21 Jun 2023 18:29:27 +0000 Subject: [PATCH 1/5] =?UTF-8?q?feat(data/finset/pointwise):=20`|s|=20?= =?UTF-8?q?=E2=88=A3=20|s=20*=20t|`=20(#18663)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/data/finset/basic.lean | 8 ++++++++ src/data/finset/n_ary.lean | 31 +++++++++++++++++++++++++++++++ src/data/finset/pointwise.lean | 18 ++++++++++++++++++ 3 files changed, 57 insertions(+) diff --git a/src/data/finset/basic.lean b/src/data/finset/basic.lean index 30687beee91e0..43bca0b7aca26 100644 --- a/src/data/finset/basic.lean +++ b/src/data/finset/basic.lean @@ -570,6 +570,10 @@ lemma forall_mem_cons (h : a ∉ s) (p : α → Prop) : (∀ x, x ∈ cons a s h → p x) ↔ p a ∧ ∀ x, x ∈ s → p x := by simp only [mem_cons, or_imp_distrib, forall_and_distrib, forall_eq] +/-- Useful in proofs by induction. -/ +lemma forall_of_forall_cons {p : α → Prop} {h : a ∉ s} (H : ∀ x, x ∈ cons a s h → p x) (x) + (h : x ∈ s) : p x := H _ $ mem_cons.2 $ or.inr h + @[simp] lemma mk_cons {s : multiset α} (h : (a ::ₘ s).nodup) : (⟨a ::ₘ s, h⟩ : finset α) = cons a ⟨s, (nodup_cons.1 h).2⟩ (nodup_cons.1 h).1 := rfl @@ -2084,6 +2088,10 @@ lemma forall_mem_insert [decidable_eq α] (a : α) (s : finset α) (p : α → P (∀ x, x ∈ insert a s → p x) ↔ p a ∧ ∀ x, x ∈ s → p x := by simp only [mem_insert, or_imp_distrib, forall_and_distrib, forall_eq] +/-- Useful in proofs by induction. -/ +lemma forall_of_forall_insert [decidable_eq α] {p : α → Prop} {a : α} {s : finset α} + (H : ∀ x, x ∈ insert a s → p x) (x) (h : x ∈ s) : p x := H _ $ mem_insert_of_mem h + end finset /-- Equivalence between the set of natural numbers which are `≥ k` and `ℕ`, given by `n → n - k`. -/ diff --git a/src/data/finset/n_ary.lean b/src/data/finset/n_ary.lean index 3a0db131eab7b..dd7d4df71f086 100644 --- a/src/data/finset/n_ary.lean +++ b/src/data/finset/n_ary.lean @@ -358,6 +358,37 @@ lemma image₂_right_identity {f : γ → β → γ} {b : β} (h : ∀ a, f a b image₂ f s {b} = s := by rw [image₂_singleton_right, funext h, image_id'] +/-- If each partial application of `f` is injective, and images of `s` under those partial +applications are disjoint (but not necessarily distinct!), then the size of `t` divides the size of +`finset.image₂ f s t`. -/ +lemma card_dvd_card_image₂_right (hf : ∀ a ∈ s, injective (f a)) + (hs : ((λ a, t.image $ f a) '' s).pairwise_disjoint id) : + t.card ∣ (image₂ f s t).card := +begin + classical, + induction s using finset.induction with a s ha ih, + { simp }, + specialize ih (forall_of_forall_insert hf) + (hs.subset $ set.image_subset _ $ coe_subset.2 $ subset_insert _ _), + rw image₂_insert_left, + by_cases h : disjoint (image (f a) t) (image₂ f s t), + { rw card_union_eq h, + exact (card_image_of_injective _ $ hf _ $ mem_insert_self _ _).symm.dvd.add ih }, + simp_rw [←bUnion_image_left, disjoint_bUnion_right, not_forall] at h, + obtain ⟨b, hb, h⟩ := h, + rwa union_eq_right_iff_subset.2, + exact (hs.eq (set.mem_image_of_mem _ $ mem_insert_self _ _) + (set.mem_image_of_mem _ $ mem_insert_of_mem hb) h).trans_subset (image_subset_image₂_right hb), +end + +/-- If each partial application of `f` is injective, and images of `t` under those partial +applications are disjoint (but not necessarily distinct!), then the size of `s` divides the size of +`finset.image₂ f s t`. -/ +lemma card_dvd_card_image₂_left (hf : ∀ b ∈ t, injective (λ a, f a b)) + (ht : ((λ b, s.image $ λ a, f a b) '' t).pairwise_disjoint id) : + s.card ∣ (image₂ f s t).card := +by { rw ←image₂_swap, exact card_dvd_card_image₂_right hf ht } + variables [decidable_eq α] [decidable_eq β] lemma image₂_inter_union_subset_union : diff --git a/src/data/finset/pointwise.lean b/src/data/finset/pointwise.lean index 03063a1ed2bc6..0f441be5a12ec 100644 --- a/src/data/finset/pointwise.lean +++ b/src/data/finset/pointwise.lean @@ -1078,6 +1078,24 @@ coe_injective $ by { push_cast, exact set.smul_univ hs } @[simp, to_additive] lemma card_smul_finset (a : α) (s : finset β) : (a • s).card = s.card := card_image_of_injective _ $ mul_action.injective _ +/-- If the left cosets of `t` by elements of `s` are disjoint (but not necessarily distinct!), then +the size of `t` divides the size of `s * t`. -/ +@[to_additive "If the left cosets of `t` by elements of `s` are disjoint (but not necessarily +distinct!), then the size of `t` divides the size of `s + t`."] +lemma card_dvd_card_smul_right {s : finset α} : + ((• t) '' (s : set α)).pairwise_disjoint id → t.card ∣ (s • t).card := +card_dvd_card_image₂_right (λ _ _, mul_action.injective _) + +variables [decidable_eq α] + +/-- If the right cosets of `s` by elements of `t` are disjoint (but not necessarily distinct!), then +the size of `s` divides the size of `s * t`. -/ +@[to_additive "If the right cosets of `s` by elements of `t` are disjoint (but not necessarily +distinct!), then the size of `s` divides the size of `s + t`."] +lemma card_dvd_card_mul_left {s t : finset α} : + ((λ b, s.image $ λ a, a * b) '' (t : set α)).pairwise_disjoint id → s.card ∣ (s * t).card := +card_dvd_card_image₂_left (λ _ _, mul_left_injective _) + end group section group_with_zero From 3efd324a3a31eaa40c9d5bfc669c4fafee5f9423 Mon Sep 17 00:00:00 2001 From: Anatole Dedecker Date: Wed, 21 Jun 2023 18:29:28 +0000 Subject: [PATCH 2/5] feat(topology/algebra/order/compact): remove conditional completeness assumption in `is_compact.exists_forall_le` (#18991) --- src/order/directed.lean | 6 +- src/topology/algebra/order/compact.lean | 219 ++++++++++++++++-------- src/topology/order/basic.lean | 42 ----- src/topology/subset_properties.lean | 42 +++-- 4 files changed, 172 insertions(+), 137 deletions(-) diff --git a/src/order/directed.lean b/src/order/directed.lean index b5c5f44c6f8fc..83c44b4bf2b62 100644 --- a/src/order/directed.lean +++ b/src/order/directed.lean @@ -131,6 +131,10 @@ lemma directed_on_of_inf_mem [semilattice_inf α] {S : set α} (H : ∀ ⦃i j⦄, i ∈ S → j ∈ S → i ⊓ j ∈ S) : directed_on (≥) S := λ a ha b hb, ⟨a ⊓ b, H ha hb, inf_le_left, inf_le_right⟩ +lemma is_total.directed [is_total α r] (f : ι → α) : + directed r f := +λ i j, or.cases_on (total_of r (f i) (f j)) (λ h, ⟨j, h, refl _⟩) (λ h, ⟨i, refl _, h⟩) + /-- `is_directed α r` states that for any elements `a`, `b` there exists an element `c` such that `r a c` and `r b c`. -/ class is_directed (α : Type*) (r : α → α → Prop) : Prop := @@ -150,7 +154,7 @@ lemma directed_on_univ_iff : directed_on r set.univ ↔ is_directed α r := @[priority 100] -- see Note [lower instance priority] instance is_total.to_is_directed [is_total α r] : is_directed α r := -⟨λ a b, or.cases_on (total_of r a b) (λ h, ⟨b, h, refl _⟩) (λ h, ⟨a, refl _, h⟩)⟩ +by rw ← directed_id_iff; exact is_total.directed _ lemma is_directed_mono [is_directed α r] (h : ∀ ⦃a b⦄, r a b → s a b) : is_directed α s := ⟨λ a b, let ⟨c, ha, hb⟩ := is_directed.directed a b in ⟨c, h ha, h hb⟩⟩ diff --git a/src/topology/algebra/order/compact.lean b/src/topology/algebra/order/compact.lean index c7e46e18e122e..0eedd6364138d 100644 --- a/src/topology/algebra/order/compact.lean +++ b/src/topology/algebra/order/compact.lean @@ -136,80 +136,39 @@ is_compact_iff_compact_space.mp is_compact_Icc end /-! -### Min and max elements of a compact set +### Extreme value theorem -/ -variables {α β γ : Type*} [conditionally_complete_linear_order α] [topological_space α] - [order_topology α] [topological_space β] [topological_space γ] - -lemma is_compact.Inf_mem {s : set α} (hs : is_compact s) (ne_s : s.nonempty) : - Inf s ∈ s := -hs.is_closed.cInf_mem ne_s hs.bdd_below - -lemma is_compact.Sup_mem {s : set α} (hs : is_compact s) (ne_s : s.nonempty) : Sup s ∈ s := -@is_compact.Inf_mem αᵒᵈ _ _ _ _ hs ne_s - -lemma is_compact.is_glb_Inf {s : set α} (hs : is_compact s) (ne_s : s.nonempty) : - is_glb s (Inf s) := -is_glb_cInf ne_s hs.bdd_below - -lemma is_compact.is_lub_Sup {s : set α} (hs : is_compact s) (ne_s : s.nonempty) : - is_lub s (Sup s) := -@is_compact.is_glb_Inf αᵒᵈ _ _ _ _ hs ne_s - -lemma is_compact.is_least_Inf {s : set α} (hs : is_compact s) (ne_s : s.nonempty) : - is_least s (Inf s) := -⟨hs.Inf_mem ne_s, (hs.is_glb_Inf ne_s).1⟩ +section linear_order -lemma is_compact.is_greatest_Sup {s : set α} (hs : is_compact s) (ne_s : s.nonempty) : - is_greatest s (Sup s) := -@is_compact.is_least_Inf αᵒᵈ _ _ _ _ hs ne_s +variables {α β γ : Type*} [linear_order α] [topological_space α] + [order_closed_topology α] [topological_space β] [topological_space γ] lemma is_compact.exists_is_least {s : set α} (hs : is_compact s) (ne_s : s.nonempty) : ∃ x, is_least s x := -⟨_, hs.is_least_Inf ne_s⟩ +begin + haveI : nonempty s := ne_s.to_subtype, + suffices : (s ∩ ⋂ x ∈ s, Iic x).nonempty, + from ⟨this.some, this.some_spec.1, mem_Inter₂.mp this.some_spec.2⟩, + rw bInter_eq_Inter, + by_contra H, + rw not_nonempty_iff_eq_empty at H, + rcases hs.elim_directed_family_closed (λ x : s, Iic ↑x) (λ x, is_closed_Iic) H + ((is_total.directed coe).mono_comp _ (λ _ _, Iic_subset_Iic.mpr)) with ⟨x, hx⟩, + exact not_nonempty_iff_eq_empty.mpr hx ⟨x, x.2, le_rfl⟩ +end lemma is_compact.exists_is_greatest {s : set α} (hs : is_compact s) (ne_s : s.nonempty) : ∃ x, is_greatest s x := -⟨_, hs.is_greatest_Sup ne_s⟩ +@is_compact.exists_is_least αᵒᵈ _ _ _ _ hs ne_s lemma is_compact.exists_is_glb {s : set α} (hs : is_compact s) (ne_s : s.nonempty) : ∃ x ∈ s, is_glb s x := -⟨_, hs.Inf_mem ne_s, hs.is_glb_Inf ne_s⟩ +exists_imp_exists (λ x (hx : is_least s x), ⟨hx.1, hx.is_glb⟩) (hs.exists_is_least ne_s) lemma is_compact.exists_is_lub {s : set α} (hs : is_compact s) (ne_s : s.nonempty) : ∃ x ∈ s, is_lub s x := -⟨_, hs.Sup_mem ne_s, hs.is_lub_Sup ne_s⟩ - -lemma is_compact.exists_Inf_image_eq_and_le {s : set β} (hs : is_compact s) (ne_s : s.nonempty) - {f : β → α} (hf : continuous_on f s) : - ∃ x ∈ s, Inf (f '' s) = f x ∧ ∀ y ∈ s, f x ≤ f y := -let ⟨x, hxs, hx⟩ := (hs.image_of_continuous_on hf).Inf_mem (ne_s.image f) -in ⟨x, hxs, hx.symm, λ y hy, - hx.trans_le $ cInf_le (hs.image_of_continuous_on hf).bdd_below $ mem_image_of_mem f hy⟩ - -lemma is_compact.exists_Sup_image_eq_and_ge {s : set β} (hs : is_compact s) (ne_s : s.nonempty) - {f : β → α} (hf : continuous_on f s) : - ∃ x ∈ s, Sup (f '' s) = f x ∧ ∀ y ∈ s, f y ≤ f x := -@is_compact.exists_Inf_image_eq_and_le αᵒᵈ _ _ _ _ _ _ hs ne_s _ hf - -lemma is_compact.exists_Inf_image_eq {s : set β} (hs : is_compact s) (ne_s : s.nonempty) - {f : β → α} (hf : continuous_on f s) : - ∃ x ∈ s, Inf (f '' s) = f x := -let ⟨x, hxs, hx, _⟩ := hs.exists_Inf_image_eq_and_le ne_s hf in ⟨x, hxs, hx⟩ - -lemma is_compact.exists_Sup_image_eq : - ∀ {s : set β}, is_compact s → s.nonempty → ∀ {f : β → α}, continuous_on f s → - ∃ x ∈ s, Sup (f '' s) = f x := -@is_compact.exists_Inf_image_eq αᵒᵈ _ _ _ _ _ - -lemma eq_Icc_of_connected_compact {s : set α} (h₁ : is_connected s) (h₂ : is_compact s) : - s = Icc (Inf s) (Sup s) := -eq_Icc_cInf_cSup_of_connected_bdd_closed h₁ h₂.bdd_below h₂.bdd_above h₂.is_closed - -/-! -### Extreme value theorem --/ +@is_compact.exists_is_glb αᵒᵈ _ _ _ _ hs ne_s /-- The **extreme value theorem**: a continuous function realizes its minimum on a compact set. -/ lemma is_compact.exists_forall_le {s : set β} (hs : is_compact s) (ne_s : s.nonempty) @@ -277,6 +236,68 @@ lemma continuous.exists_forall_ge [nonempty β] {f : β → α} ∃ x, ∀ y, f y ≤ f x := @continuous.exists_forall_le αᵒᵈ _ _ _ _ _ _ _ hf hlim +/-- A continuous function with compact support has a global minimum. -/ +@[to_additive "A continuous function with compact support has a global minimum."] +lemma continuous.exists_forall_le_of_has_compact_mul_support [nonempty β] [has_one α] + {f : β → α} (hf : continuous f) (h : has_compact_mul_support f) : + ∃ (x : β), ∀ (y : β), f x ≤ f y := +begin + obtain ⟨_, ⟨x, rfl⟩, hx⟩ := (h.is_compact_range hf).exists_is_least (range_nonempty _), + rw [mem_lower_bounds, forall_range_iff] at hx, + exact ⟨x, hx⟩, +end + +/-- A continuous function with compact support has a global maximum. -/ +@[to_additive "A continuous function with compact support has a global maximum."] +lemma continuous.exists_forall_ge_of_has_compact_mul_support [nonempty β] [has_one α] + {f : β → α} (hf : continuous f) (h : has_compact_mul_support f) : + ∃ (x : β), ∀ (y : β), f y ≤ f x := +@continuous.exists_forall_le_of_has_compact_mul_support αᵒᵈ _ _ _ _ _ _ _ _ hf h + +/-- A compact set is bounded below -/ +lemma is_compact.bdd_below [nonempty α] {s : set α} (hs : is_compact s) : bdd_below s := +begin + cases s.eq_empty_or_nonempty, + { rw h, + exact bdd_below_empty }, + { obtain ⟨a, ha, has⟩ := hs.exists_is_least h, + exact ⟨a, has⟩ }, +end + +/-- A compact set is bounded above -/ +lemma is_compact.bdd_above [nonempty α] {s : set α} (hs : is_compact s) : bdd_above s := +@is_compact.bdd_below αᵒᵈ _ _ _ _ _ hs + +/-- A continuous function is bounded below on a compact set. -/ +lemma is_compact.bdd_below_image [nonempty α] {f : β → α} {K : set β} + (hK : is_compact K) (hf : continuous_on f K) : bdd_below (f '' K) := +(hK.image_of_continuous_on hf).bdd_below + +/-- A continuous function is bounded above on a compact set. -/ +lemma is_compact.bdd_above_image [nonempty α] {f : β → α} {K : set β} + (hK : is_compact K) (hf : continuous_on f K) : bdd_above (f '' K) := +@is_compact.bdd_below_image αᵒᵈ _ _ _ _ _ _ _ _ hK hf + +/-- A continuous function with compact support is bounded below. -/ +@[to_additive /-" A continuous function with compact support is bounded below. "-/] +lemma continuous.bdd_below_range_of_has_compact_mul_support [has_one α] {f : β → α} + (hf : continuous f) (h : has_compact_mul_support f) : bdd_below (range f) := +(h.is_compact_range hf).bdd_below + +/-- A continuous function with compact support is bounded above. -/ +@[to_additive /-" A continuous function with compact support is bounded above. "-/] +lemma continuous.bdd_above_range_of_has_compact_mul_support [has_one α] + {f : β → α} (hf : continuous f) (h : has_compact_mul_support f) : + bdd_above (range f) := +@continuous.bdd_below_range_of_has_compact_mul_support αᵒᵈ _ _ _ _ _ _ _ hf h + +end linear_order + +section conditionally_complete_linear_order + +variables {α β γ : Type*} [conditionally_complete_linear_order α] [topological_space α] + [order_closed_topology α] [topological_space β] [topological_space γ] + lemma is_compact.Sup_lt_iff_of_continuous {f : β → α} {K : set β} (hK : is_compact K) (h0K : K.nonempty) (hf : continuous_on f K) (y : α) : Sup (f '' K) < y ↔ ∀ x ∈ K, f x < y := @@ -294,23 +315,71 @@ lemma is_compact.lt_Inf_iff_of_continuous {α β : Type*} y < Inf (f '' K) ↔ ∀ x ∈ K, y < f x := @is_compact.Sup_lt_iff_of_continuous αᵒᵈ β _ _ _ _ _ _ hK h0K hf y -/-- A continuous function with compact support has a global minimum. -/ -@[to_additive "A continuous function with compact support has a global minimum."] -lemma continuous.exists_forall_le_of_has_compact_mul_support [nonempty β] [has_one α] - {f : β → α} (hf : continuous f) (h : has_compact_mul_support f) : - ∃ (x : β), ∀ (y : β), f x ≤ f y := -begin - obtain ⟨_, ⟨x, rfl⟩, hx⟩ := (h.is_compact_range hf).exists_is_least (range_nonempty _), - rw [mem_lower_bounds, forall_range_iff] at hx, - exact ⟨x, hx⟩, -end +end conditionally_complete_linear_order -/-- A continuous function with compact support has a global maximum. -/ -@[to_additive "A continuous function with compact support has a global maximum."] -lemma continuous.exists_forall_ge_of_has_compact_mul_support [nonempty β] [has_one α] - {f : β → α} (hf : continuous f) (h : has_compact_mul_support f) : - ∃ (x : β), ∀ (y : β), f y ≤ f x := -@continuous.exists_forall_le_of_has_compact_mul_support αᵒᵈ _ _ _ _ _ _ _ _ hf h +/-! +### Min and max elements of a compact set +-/ + +section order_closed_topology + +variables {α β γ : Type*} [conditionally_complete_linear_order α] [topological_space α] + [order_closed_topology α] [topological_space β] [topological_space γ] + +lemma is_compact.Inf_mem {s : set α} (hs : is_compact s) (ne_s : s.nonempty) : + Inf s ∈ s := +let ⟨a, ha⟩ := hs.exists_is_least ne_s in +ha.Inf_mem + +lemma is_compact.Sup_mem {s : set α} (hs : is_compact s) (ne_s : s.nonempty) : Sup s ∈ s := +@is_compact.Inf_mem αᵒᵈ _ _ _ _ hs ne_s + +lemma is_compact.is_glb_Inf {s : set α} (hs : is_compact s) (ne_s : s.nonempty) : + is_glb s (Inf s) := +is_glb_cInf ne_s hs.bdd_below + +lemma is_compact.is_lub_Sup {s : set α} (hs : is_compact s) (ne_s : s.nonempty) : + is_lub s (Sup s) := +@is_compact.is_glb_Inf αᵒᵈ _ _ _ _ hs ne_s + +lemma is_compact.is_least_Inf {s : set α} (hs : is_compact s) (ne_s : s.nonempty) : + is_least s (Inf s) := +⟨hs.Inf_mem ne_s, (hs.is_glb_Inf ne_s).1⟩ + +lemma is_compact.is_greatest_Sup {s : set α} (hs : is_compact s) (ne_s : s.nonempty) : + is_greatest s (Sup s) := +@is_compact.is_least_Inf αᵒᵈ _ _ _ _ hs ne_s + +lemma is_compact.exists_Inf_image_eq_and_le {s : set β} (hs : is_compact s) (ne_s : s.nonempty) + {f : β → α} (hf : continuous_on f s) : + ∃ x ∈ s, Inf (f '' s) = f x ∧ ∀ y ∈ s, f x ≤ f y := +let ⟨x, hxs, hx⟩ := (hs.image_of_continuous_on hf).Inf_mem (ne_s.image f) +in ⟨x, hxs, hx.symm, λ y hy, + hx.trans_le $ cInf_le (hs.image_of_continuous_on hf).bdd_below $ mem_image_of_mem f hy⟩ + +lemma is_compact.exists_Sup_image_eq_and_ge {s : set β} (hs : is_compact s) (ne_s : s.nonempty) + {f : β → α} (hf : continuous_on f s) : + ∃ x ∈ s, Sup (f '' s) = f x ∧ ∀ y ∈ s, f y ≤ f x := +@is_compact.exists_Inf_image_eq_and_le αᵒᵈ _ _ _ _ _ _ hs ne_s _ hf + +lemma is_compact.exists_Inf_image_eq {s : set β} (hs : is_compact s) (ne_s : s.nonempty) + {f : β → α} (hf : continuous_on f s) : + ∃ x ∈ s, Inf (f '' s) = f x := +let ⟨x, hxs, hx, _⟩ := hs.exists_Inf_image_eq_and_le ne_s hf in ⟨x, hxs, hx⟩ + +lemma is_compact.exists_Sup_image_eq : + ∀ {s : set β}, is_compact s → s.nonempty → ∀ {f : β → α}, continuous_on f s → + ∃ x ∈ s, Sup (f '' s) = f x := +@is_compact.exists_Inf_image_eq αᵒᵈ _ _ _ _ _ + +end order_closed_topology + +variables {α β γ : Type*} [conditionally_complete_linear_order α] [topological_space α] + [order_topology α] [topological_space β] [topological_space γ] + +lemma eq_Icc_of_connected_compact {s : set α} (h₁ : is_connected s) (h₂ : is_compact s) : + s = Icc (Inf s) (Sup s) := +eq_Icc_cInf_cSup_of_connected_bdd_closed h₁ h₂.bdd_below h₂.bdd_above h₂.is_closed lemma is_compact.continuous_Sup {f : γ → β → α} {K : set β} (hK : is_compact K) (hf : continuous ↿f) : diff --git a/src/topology/order/basic.lean b/src/topology/order/basic.lean index 733fa1a9de319..a17106de53df5 100644 --- a/src/topology/order/basic.lean +++ b/src/topology/order/basic.lean @@ -648,48 +648,6 @@ lemma dense.exists_between [densely_ordered α] {s : set α} (hs : dense s) {x y ∃ z ∈ s, z ∈ Ioo x y := hs.exists_mem_open is_open_Ioo (nonempty_Ioo.2 h) -variables [nonempty α] [topological_space β] - -/-- A compact set is bounded below -/ -lemma is_compact.bdd_below {s : set α} (hs : is_compact s) : bdd_below s := -begin - by_contra H, - rcases hs.elim_finite_subcover_image (λ x (_ : x ∈ s), @is_open_Ioi _ _ _ _ x) _ - with ⟨t, st, ft, ht⟩, - { refine H (ft.bdd_below.imp $ λ C hC y hy, _), - rcases mem_Union₂.1 (ht hy) with ⟨x, hx, xy⟩, - exact le_trans (hC hx) (le_of_lt xy) }, - { refine λ x hx, mem_Union₂.2 (not_imp_comm.1 _ H), - exact λ h, ⟨x, λ y hy, le_of_not_lt (h.imp $ λ ys, ⟨_, hy, ys⟩)⟩ } -end - -/-- A compact set is bounded above -/ -lemma is_compact.bdd_above {s : set α} (hs : is_compact s) : bdd_above s := -@is_compact.bdd_below αᵒᵈ _ _ _ _ _ hs - -/-- A continuous function is bounded below on a compact set. -/ -lemma is_compact.bdd_below_image {f : β → α} {K : set β} - (hK : is_compact K) (hf : continuous_on f K) : bdd_below (f '' K) := -(hK.image_of_continuous_on hf).bdd_below - -/-- A continuous function is bounded above on a compact set. -/ -lemma is_compact.bdd_above_image {f : β → α} {K : set β} - (hK : is_compact K) (hf : continuous_on f K) : bdd_above (f '' K) := -@is_compact.bdd_below_image αᵒᵈ _ _ _ _ _ _ _ _ hK hf - -/-- A continuous function with compact support is bounded below. -/ -@[to_additive /-" A continuous function with compact support is bounded below. "-/] -lemma continuous.bdd_below_range_of_has_compact_mul_support [has_one α] {f : β → α} - (hf : continuous f) (h : has_compact_mul_support f) : bdd_below (range f) := -(h.is_compact_range hf).bdd_below - -/-- A continuous function with compact support is bounded above. -/ -@[to_additive /-" A continuous function with compact support is bounded above. "-/] -lemma continuous.bdd_above_range_of_has_compact_mul_support [has_one α] - {f : β → α} (hf : continuous f) (h : has_compact_mul_support f) : - bdd_above (range f) := -@continuous.bdd_below_range_of_has_compact_mul_support αᵒᵈ _ _ _ _ _ _ _ _ hf h - end linear_order end order_closed_topology diff --git a/src/topology/subset_properties.lean b/src/topology/subset_properties.lean index 36f63e1120bbb..97d583e2dacd9 100644 --- a/src/topology/subset_properties.lean +++ b/src/topology/subset_properties.lean @@ -230,6 +230,19 @@ lemma is_compact.disjoint_nhds_set_right {l : filter α} (hs : is_compact s) : disjoint l (𝓝ˢ s) ↔ ∀ x ∈ s, disjoint l (𝓝 x) := by simpa only [disjoint.comm] using hs.disjoint_nhds_set_left +/-- For every directed family of closed sets whose intersection avoids a compact set, +there exists a single element of the family which itself avoids this compact set. -/ +lemma is_compact.elim_directed_family_closed {ι : Type v} [hι : nonempty ι] (hs : is_compact s) + (Z : ι → set α) (hZc : ∀ i, is_closed (Z i)) (hsZ : s ∩ (⋂ i, Z i) = ∅) (hdZ : directed (⊇) Z) : + ∃ i : ι, s ∩ Z i = ∅ := +let ⟨t, ht⟩ := hs.elim_directed_cover (compl ∘ Z) (λ i, (hZc i).is_open_compl) + (by simpa only [subset_def, not_forall, eq_empty_iff_forall_not_mem, mem_Union, + exists_prop, mem_inter_iff, not_and, iff_self, mem_Inter, mem_compl_iff] using hsZ) + (hdZ.mono_comp _ $ λ _ _, compl_subset_compl.mpr) + in +⟨t, by simpa only [subset_def, not_forall, eq_empty_iff_forall_not_mem, mem_Union, + exists_prop, mem_inter_iff, not_and, iff_self, mem_Inter, mem_compl_iff] using ht⟩ + /-- For every family of closed sets whose intersection avoids a compact set, there exists a finite subfamily whose intersection avoids this compact set. -/ lemma is_compact.elim_finite_subfamily_closed {s : set α} {ι : Type v} (hs : is_compact s) @@ -273,25 +286,16 @@ lemma is_compact.nonempty_Inter_of_directed_nonempty_compact_closed (hZn : ∀ i, (Z i).nonempty) (hZc : ∀ i, is_compact (Z i)) (hZcl : ∀ i, is_closed (Z i)) : (⋂ i, Z i).nonempty := begin - apply hι.elim, - intro i₀, - let Z' := λ i, Z i ∩ Z i₀, - suffices : (⋂ i, Z' i).nonempty, - { exact this.mono (Inter_mono $ λ i, inter_subset_left (Z i) (Z i₀)) }, - rw nonempty_iff_ne_empty, - intro H, - obtain ⟨t, ht⟩ : ∃ (t : finset ι), ((Z i₀) ∩ ⋂ (i ∈ t), Z' i) = ∅, - from (hZc i₀).elim_finite_subfamily_closed Z' - (assume i, is_closed.inter (hZcl i) (hZcl i₀)) (by rw [H, inter_empty]), - obtain ⟨i₁, hi₁⟩ : ∃ i₁ : ι, Z i₁ ⊆ Z i₀ ∧ ∀ i ∈ t, Z i₁ ⊆ Z' i, - { rcases directed.finset_le hZd t with ⟨i, hi⟩, - rcases hZd i i₀ with ⟨i₁, hi₁, hi₁₀⟩, - use [i₁, hi₁₀], - intros j hj, - exact subset_inter (subset.trans hi₁ (hi j hj)) hi₁₀ }, - suffices : ((Z i₀) ∩ ⋂ (i ∈ t), Z' i).nonempty, - { rw nonempty_iff_ne_empty at this, contradiction }, - exact (hZn i₁).mono (subset_inter hi₁.left $ subset_Inter₂ hi₁.right), + let i₀ := hι.some, + suffices : (Z i₀ ∩ ⋂ i, Z i).nonempty, + by rwa inter_eq_right_iff_subset.mpr (Inter_subset _ i₀) at this, + simp only [nonempty_iff_ne_empty] at hZn ⊢, + apply mt ((hZc i₀).elim_directed_family_closed Z hZcl), + push_neg, + simp only [← nonempty_iff_ne_empty] at hZn ⊢, + refine ⟨hZd, λ i, _⟩, + rcases hZd i₀ i with ⟨j, hji₀, hji⟩, + exact (hZn j).mono (subset_inter hji₀ hji) end /-- Cantor's intersection theorem for sequences indexed by `ℕ`: From 6285167a053ad0990fc88e56c48ccd9fae6550eb Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 21 Jun 2023 18:29:29 +0000 Subject: [PATCH 3/5] chore(topology/algebra/module/basic): generalize `to_span_singleton` to topological spaces (#19116) This should be straightforward to forward-port, as it involves deleting one hunk and pasting in another. --- .../normed_space/continuous_linear_map.lean | 21 ------------- src/topology/algebra/module/basic.lean | 31 +++++++++++++++++++ 2 files changed, 31 insertions(+), 21 deletions(-) diff --git a/src/analysis/normed_space/continuous_linear_map.lean b/src/analysis/normed_space/continuous_linear_map.lean index 693adffcd123e..87ad5e2c41002 100644 --- a/src/analysis/normed_space/continuous_linear_map.lean +++ b/src/analysis/normed_space/continuous_linear_map.lean @@ -192,27 +192,6 @@ lemma to_span_singleton_homothety (x : E) (c : 𝕜) : ‖linear_map.to_span_singleton 𝕜 E x c‖ = ‖x‖ * ‖c‖ := by {rw mul_comm, exact norm_smul _ _} -/-- Given an element `x` of a normed space `E` over a field `𝕜`, the natural continuous - linear map from `𝕜` to `E` by taking multiples of `x`.-/ -def to_span_singleton (x : E) : 𝕜 →L[𝕜] E := -of_homothety (linear_map.to_span_singleton 𝕜 E x) ‖x‖ (to_span_singleton_homothety 𝕜 x) - -lemma to_span_singleton_apply (x : E) (r : 𝕜) : to_span_singleton 𝕜 x r = r • x := -by simp [to_span_singleton, of_homothety, linear_map.to_span_singleton] - -lemma to_span_singleton_add (x y : E) : - to_span_singleton 𝕜 (x + y) = to_span_singleton 𝕜 x + to_span_singleton 𝕜 y := -by { ext1, simp [to_span_singleton_apply], } - -lemma to_span_singleton_smul' (𝕜') [normed_field 𝕜'] [normed_space 𝕜' E] - [smul_comm_class 𝕜 𝕜' E] (c : 𝕜') (x : E) : - to_span_singleton 𝕜 (c • x) = c • to_span_singleton 𝕜 x := -by { ext1, rw [to_span_singleton_apply, smul_apply, to_span_singleton_apply, smul_comm], } - -lemma to_span_singleton_smul (c : 𝕜) (x : E) : - to_span_singleton 𝕜 (c • x) = c • to_span_singleton 𝕜 x := -to_span_singleton_smul' 𝕜 𝕜 c x - end continuous_linear_map section diff --git a/src/topology/algebra/module/basic.lean b/src/topology/algebra/module/basic.lean index 5379fd79c140b..f7d3e1befccef 100644 --- a/src/topology/algebra/module/basic.lean +++ b/src/topology/algebra/module/basic.lean @@ -1003,6 +1003,37 @@ lemma smul_right_comp [has_continuous_mul R₁] {x : M₂} {c : R₁} : smul_right (1 : R₁ →L[R₁] R₁) (c • x) := by { ext, simp [mul_smul] } +section to_span_singleton +variables (R₁) +variables [has_continuous_smul R₁ M₁] + +/-- Given an element `x` of a topological space `M` over a semiring `R`, the natural continuous +linear map from `R` to `M` by taking multiples of `x`.-/ +def to_span_singleton (x : M₁) : R₁ →L[R₁] M₁ := +{ to_linear_map := linear_map.to_span_singleton R₁ M₁ x, + cont := continuous_id.smul continuous_const } + +lemma to_span_singleton_apply (x : M₁) (r : R₁) : to_span_singleton R₁ x r = r • x := +rfl + +lemma to_span_singleton_add [has_continuous_add M₁] (x y : M₁) : + to_span_singleton R₁ (x + y) = to_span_singleton R₁ x + to_span_singleton R₁ y := +by { ext1, simp [to_span_singleton_apply], } + +lemma to_span_singleton_smul' {α} [monoid α] [distrib_mul_action α M₁] + [has_continuous_const_smul α M₁] + [smul_comm_class R₁ α M₁] (c : α) (x : M₁) : + to_span_singleton R₁ (c • x) = c • to_span_singleton R₁ x := +by { ext1, rw [to_span_singleton_apply, smul_apply, to_span_singleton_apply, smul_comm], } + +/-- A special case of `to_span_singleton_smul'` for when `R` is commutative. -/ +lemma to_span_singleton_smul (R) {M₁} [comm_semiring R] [add_comm_monoid M₁] [module R M₁] + [topological_space R] [topological_space M₁] [has_continuous_smul R M₁] (c : R) (x : M₁) : + to_span_singleton R (c • x) = c • to_span_singleton R x := +to_span_singleton_smul' R c x + +end to_span_singleton + end semiring section pi From 554bb38de8ded0dafe93b7f18f0bfee6ef77dc5d Mon Sep 17 00:00:00 2001 From: Eric Rodriguez Date: Wed, 21 Jun 2023 22:24:16 +0000 Subject: [PATCH 4/5] feat(order/monotone): add `decidable` instances (#19175) These can be written in a very nice, elegant way. Co-authored-by: Yury G. Kudryashov --- .../ascending_descending_sequences.lean | 1 - src/order/monotone/basic.lean | 15 +++++++++++++++ 2 files changed, 15 insertions(+), 1 deletion(-) diff --git a/archive/wiedijk_100_theorems/ascending_descending_sequences.lean b/archive/wiedijk_100_theorems/ascending_descending_sequences.lean index 2c2d3931d8d69..a0d947a8089a5 100644 --- a/archive/wiedijk_100_theorems/ascending_descending_sequences.lean +++ b/archive/wiedijk_100_theorems/ascending_descending_sequences.lean @@ -24,7 +24,6 @@ sequences, increasing, decreasing, Ramsey, Erdos-Szekeres, Erdős–Szekeres, Er variables {α : Type*} [linear_order α] {β : Type*} open function finset -open_locale classical namespace theorems_100 diff --git a/src/order/monotone/basic.lean b/src/order/monotone/basic.lean index 84433c7deff17..9ca070071a7ca 100644 --- a/src/order/monotone/basic.lean +++ b/src/order/monotone/basic.lean @@ -102,6 +102,21 @@ def strict_anti_on (f : α → β) (s : set α) : Prop := end monotone_def +section decidable + +variables [preorder α] [preorder β] {f : α → β} {s : set α} + +instance [i : decidable (∀ a b, a ≤ b → f a ≤ f b)] : decidable (monotone f) := i +instance [i : decidable (∀ a b, a ≤ b → f b ≤ f a)] : decidable (antitone f) := i +instance [i : decidable (∀ a b ∈ s, a ≤ b → f a ≤ f b)] : decidable (monotone_on f s) := i +instance [i : decidable (∀ a b ∈ s, a ≤ b → f b ≤ f a)] : decidable (antitone_on f s) := i +instance [i : decidable (∀ a b, a < b → f a < f b)] : decidable (strict_mono f) := i +instance [i : decidable (∀ a b, a < b → f b < f a)] : decidable (strict_anti f) := i +instance [i : decidable (∀ a b ∈ s, a < b → f a < f b)] : decidable (strict_mono_on f s) := i +instance [i : decidable (∀ a b ∈ s, a < b → f b < f a)] : decidable (strict_anti_on f s) := i + +end decidable + /-! ### Monotonicity on the dual order Strictly, many of the `*_on.dual` lemmas in this section should use `of_dual ⁻¹' s` instead of `s`, From f40476639bac089693a489c9e354ebd75dc0f886 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Thu, 22 Jun 2023 02:23:51 +0000 Subject: [PATCH 5/5] feat(analysis/normed_space/multilinear): add lemmas/defs (#19114) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Add `simps` here and there. * Add `continuous_multilinear_map.norm_of_subsingleton_le` and `continuous_multilinear_map.nnnorm_of_subsingleton_le`. * Add `continuous_multilinear_map.cod_restrict`. * Add `continuous_multilinear_map.restrict_scalarsₗᵢ`, a `linear_isometry_equiv` version of `continuous_multilinear_map.restrict_scalars`. * Split `continuous_multilinear_map.dom_dom_congr` into 3 definitions: a map, an equivalence, and a linear isometry (the old def). --- src/analysis/normed_space/multilinear.lean | 65 +++++++++++--------- src/topology/algebra/module/multilinear.lean | 25 ++++++++ 2 files changed, 62 insertions(+), 28 deletions(-) diff --git a/src/analysis/normed_space/multilinear.lean b/src/analysis/normed_space/multilinear.lean index da305f925b08a..e2db42edbc5b3 100644 --- a/src/analysis/normed_space/multilinear.lean +++ b/src/analysis/normed_space/multilinear.lean @@ -446,18 +446,23 @@ end section variables (𝕜 G) +lemma norm_of_subsingleton_le [subsingleton ι] (i' : ι) : ‖of_subsingleton 𝕜 G i'‖ ≤ 1 := +op_norm_le_bound _ zero_le_one $ λ m, + by rw [fintype.prod_subsingleton _ i', one_mul, of_subsingleton_apply] + @[simp] lemma norm_of_subsingleton [subsingleton ι] [nontrivial G] (i' : ι) : ‖of_subsingleton 𝕜 G i'‖ = 1 := begin - apply le_antisymm, - { refine op_norm_le_bound _ zero_le_one (λ m, _), - rw [fintype.prod_subsingleton _ i', one_mul, of_subsingleton_apply] }, - { obtain ⟨g, hg⟩ := exists_ne (0 : G), - rw ←norm_ne_zero_iff at hg, - have := (of_subsingleton 𝕜 G i').ratio_le_op_norm (λ _, g), - rwa [fintype.prod_subsingleton _ i', of_subsingleton_apply, div_self hg] at this }, + apply le_antisymm (norm_of_subsingleton_le 𝕜 G i'), + obtain ⟨g, hg⟩ := exists_ne (0 : G), + rw ←norm_ne_zero_iff at hg, + have := (of_subsingleton 𝕜 G i').ratio_le_op_norm (λ _, g), + rwa [fintype.prod_subsingleton _ i', of_subsingleton_apply, div_self hg] at this, end +lemma nnnorm_of_subsingleton_le [subsingleton ι] (i' : ι) : ‖of_subsingleton 𝕜 G i'‖₊ ≤ 1 := +norm_of_subsingleton_le _ _ _ + @[simp] lemma nnnorm_of_subsingleton [subsingleton ι] [nontrivial G] (i' : ι) : ‖of_subsingleton 𝕜 G i'‖₊ = 1 := nnreal.eq $ norm_of_subsingleton _ _ _ @@ -518,18 +523,22 @@ variables {𝕜' : Type*} [nontrivially_normed_field 𝕜'] [normed_algebra 𝕜 variables [normed_space 𝕜' G] [is_scalar_tower 𝕜' 𝕜 G] variables [Π i, normed_space 𝕜' (E i)] [∀ i, is_scalar_tower 𝕜' 𝕜 (E i)] -@[simp] lemma norm_restrict_scalars : ‖f.restrict_scalars 𝕜'‖ = ‖f‖ := -by simp only [norm_def, coe_restrict_scalars] +@[simp] lemma norm_restrict_scalars : ‖f.restrict_scalars 𝕜'‖ = ‖f‖ := rfl variable (𝕜') -/-- `continuous_multilinear_map.restrict_scalars` as a `continuous_multilinear_map`. -/ -def restrict_scalars_linear : - continuous_multilinear_map 𝕜 E G →L[𝕜'] continuous_multilinear_map 𝕜' E G := -linear_map.mk_continuous +/-- `continuous_multilinear_map.restrict_scalars` as a `linear_isometry`. -/ +def restrict_scalarsₗᵢ : + continuous_multilinear_map 𝕜 E G →ₗᵢ[𝕜'] continuous_multilinear_map 𝕜' E G := { to_fun := restrict_scalars 𝕜', map_add' := λ m₁ m₂, rfl, - map_smul' := λ c m, rfl } 1 $ λ f, by simp + map_smul' := λ c m, rfl, + norm_map' := λ f, rfl } + +/-- `continuous_multilinear_map.restrict_scalars` as a `continuous_linear_map`. -/ +def restrict_scalars_linear : + continuous_multilinear_map 𝕜 E G →L[𝕜'] continuous_multilinear_map 𝕜' E G := +(restrict_scalarsₗᵢ 𝕜').to_continuous_linear_map variable {𝕜'} @@ -922,6 +931,7 @@ rfl /-- Flip arguments in `f : G →L[𝕜] continuous_multilinear_map 𝕜 E G'` to get `continuous_multilinear_map 𝕜 E (G →L[𝕜] G')` -/ +@[simps apply_apply] def flip_multilinear (f : G →L[𝕜] continuous_multilinear_map 𝕜 E G') : continuous_multilinear_map 𝕜 E (G →L[𝕜] G') := multilinear_map.mk_continuous @@ -1503,23 +1513,22 @@ namespace continuous_multilinear_map variables (𝕜 G G') +-- fails to unify without `@`; TODO: try again in Lean 4 +@[simp] theorem norm_dom_dom_congr (σ : ι ≃ ι') (f : continuous_multilinear_map 𝕜 (λ _ : ι, G) G') : + ‖@dom_dom_congr 𝕜 ι G G' _ _ _ _ _ _ _ ι' σ f‖ = ‖f‖ := +by simp only [norm_def, linear_equiv.coe_mk, ← σ.prod_comp, + (σ.arrow_congr (equiv.refl G)).surjective.forall, dom_dom_congr_apply, equiv.arrow_congr_apply, + equiv.coe_refl, comp.left_id, comp_app, equiv.symm_apply_apply, id] + /-- An equivalence of the index set defines a linear isometric equivalence between the spaces of multilinear maps. -/ -def dom_dom_congr (σ : ι ≃ ι') : +def dom_dom_congrₗᵢ (σ : ι ≃ ι') : continuous_multilinear_map 𝕜 (λ _ : ι, G) G' ≃ₗᵢ[𝕜] continuous_multilinear_map 𝕜 (λ _ : ι', G) G' := -linear_isometry_equiv.of_bounds - { to_fun := λ f, (multilinear_map.dom_dom_congr σ f.to_multilinear_map).mk_continuous ‖f‖ $ - λ m, (f.le_op_norm (λ i, m (σ i))).trans_eq $ by rw [← σ.prod_comp], - inv_fun := λ f, (multilinear_map.dom_dom_congr σ.symm f.to_multilinear_map).mk_continuous ‖f‖ $ - λ m, (f.le_op_norm (λ i, m (σ.symm i))).trans_eq $ by rw [← σ.symm.prod_comp], - left_inv := λ f, ext $ λ m, congr_arg f $ by simp only [σ.symm_apply_apply], - right_inv := λ f, ext $ λ m, congr_arg f $ by simp only [σ.apply_symm_apply], - map_add' := λ f g, rfl, - map_smul' := λ c f, rfl } - (λ f, multilinear_map.mk_continuous_norm_le _ (norm_nonneg f) _) - (λ f, multilinear_map.mk_continuous_norm_le _ (norm_nonneg f) _) - + { map_add' := λ _ _, rfl, + map_smul' := λ _ _, rfl, + norm_map' := norm_dom_dom_congr 𝕜 G G' σ, + .. dom_dom_congr_equiv σ } variables {𝕜 G G'} section @@ -1589,7 +1598,7 @@ values in the space of continuous multilinear maps of `l` variables. -/ def curry_fin_finset {k l n : ℕ} {s : finset (fin n)} (hk : s.card = k) (hl : sᶜ.card = l) : (G [×n]→L[𝕜] G') ≃ₗᵢ[𝕜] (G [×k]→L[𝕜] G [×l]→L[𝕜] G') := -(dom_dom_congr 𝕜 G G' (fin_sum_equiv_of_finset hk hl).symm).trans +(dom_dom_congrₗᵢ 𝕜 G G' (fin_sum_equiv_of_finset hk hl).symm).trans (curry_sum_equiv 𝕜 (fin k) (fin l) G G') variables {𝕜 G G'} diff --git a/src/topology/algebra/module/multilinear.lean b/src/topology/algebra/module/multilinear.lean index efa86ed869ffc..ef1fead7e6fc3 100644 --- a/src/topology/algebra/module/multilinear.lean +++ b/src/topology/algebra/module/multilinear.lean @@ -217,6 +217,12 @@ lemma pi_apply {ι' : Type*} {M' : ι' → Type*} [Π i, add_comm_monoid (M' i)] pi f m j = f j m := rfl +/-- Restrict the codomain of a continuous multilinear map to a submodule. -/ +@[simps to_multilinear_map apply_coe] +def cod_restrict (f : continuous_multilinear_map R M₁ M₂) (p : submodule R M₂) (h : ∀ v, f v ∈ p) : + continuous_multilinear_map R M₁ p := +⟨f.1.cod_restrict p h, f.cont.subtype_mk _⟩ + section variables (R M₂) @@ -276,6 +282,25 @@ def pi_equiv {ι' : Type*} {M' : ι' → Type*} [Π i, add_comm_monoid (M' i)] left_inv := λ f, by { ext, refl }, right_inv := λ f, by { ext, refl } } +/-- An equivalence of the index set defines an equivalence between the spaces of continuous +multilinear maps. This is the forward map of this equivalence. -/ +@[simps to_multilinear_map apply] +def dom_dom_congr {ι' : Type*} (e : ι ≃ ι') (f : continuous_multilinear_map R (λ _ : ι, M₂) M₃) : + continuous_multilinear_map R (λ _ : ι', M₂) M₃ := +{ to_multilinear_map := f.dom_dom_congr e, + cont := f.cont.comp $ continuous_pi $ λ _, continuous_apply _ } + +/-- An equivalence of the index set defines an equivalence between the spaces of continuous +multilinear maps. In case of normed spaces, this is a linear isometric equivalence, see +`continuous.multilinear_map.dom_dom_congrₗᵢ`. -/ +@[simps] +def dom_dom_congr_equiv {ι' : Type*} (e : ι ≃ ι') : + continuous_multilinear_map R (λ _ : ι, M₂) M₃ ≃ continuous_multilinear_map R (λ _ : ι', M₂) M₃ := +{ to_fun := dom_dom_congr e, + inv_fun := dom_dom_congr e.symm, + left_inv := λ _, ext $ λ _, by simp, + right_inv := λ _, ext $ λ _, by simp } + /-- In the specific case of continuous multilinear maps on spaces indexed by `fin (n+1)`, where one can build an element of `Π(i : fin (n+1)), M i` using `cons`, one can express directly the additivity of a multilinear map along the first variable. -/