From 250bf30b823d812379be4b3b5fe134edbc6ea8cc Mon Sep 17 00:00:00 2001 From: damiano Date: Wed, 30 Oct 2024 10:00:11 +0000 Subject: [PATCH] chore: remove more unused variables (#18425) #17715 --- Mathlib/Combinatorics/Digraph/Basic.lean | 2 +- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean | 7 +++---- Mathlib/Combinatorics/SetFamily/Compression/UV.lean | 4 ++-- Mathlib/Combinatorics/SetFamily/FourFunctions.lean | 4 ++-- Mathlib/Data/Finset/Sups.lean | 10 +++++----- Mathlib/GroupTheory/GroupAction/Blocks.lean | 2 +- Mathlib/GroupTheory/GroupAction/Support.lean | 2 +- Mathlib/GroupTheory/Order/Min.lean | 2 +- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean | 2 +- Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean | 5 ++--- Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean | 1 - Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean | 2 +- Mathlib/LinearAlgebra/QuadraticForm/Isometry.lean | 2 +- Mathlib/LinearAlgebra/QuadraticForm/Prod.lean | 4 +--- .../LinearAlgebra/TensorProduct/Graded/External.lean | 2 +- Mathlib/Order/Filter/Cocardinal.lean | 4 +--- Mathlib/Order/KonigLemma.lean | 2 +- Mathlib/Order/PFilter.lean | 2 +- Mathlib/RingTheory/WittVector/Defs.lean | 2 -- Mathlib/Tactic/Widget/StringDiagram.lean | 2 +- Mathlib/Topology/ContinuousMap/CompactlySupported.lean | 2 -- Mathlib/Topology/FiberBundle/Trivialization.lean | 8 +++----- 22 files changed, 30 insertions(+), 43 deletions(-) diff --git a/Mathlib/Combinatorics/Digraph/Basic.lean b/Mathlib/Combinatorics/Digraph/Basic.lean index f29d31b9e8121..bc72f31b7b8b4 100644 --- a/Mathlib/Combinatorics/Digraph/Basic.lean +++ b/Mathlib/Combinatorics/Digraph/Basic.lean @@ -96,7 +96,7 @@ Any bipartite digraph may be regarded as a subgraph of one of these. def completeBipartiteGraph (V W : Type*) : Digraph (Sum V W) where Adj v w := v.isLeft ∧ w.isRight ∨ v.isRight ∧ w.isLeft -variable {ι : Sort*} {V W X : Type*} (G : Digraph V) (G' : Digraph W) {a b c u v w : V} +variable {ι : Sort*} {V : Type*} (G : Digraph V) {a b : V} theorem adj_injective : Injective (Adj : Digraph V → V → V → Prop) := fun _ _ ↦ Digraph.ext diff --git a/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean b/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean index a7d1c6345f5ca..d2173e136b147 100644 --- a/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean +++ b/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean @@ -100,8 +100,7 @@ variable {α β : Type*} /-! ### Truncated supremum, truncated infimum -/ section SemilatticeSup -variable [SemilatticeSup α] [SemilatticeSup β] - [BoundedOrder β] {s t : Finset α} {a b : α} +variable [SemilatticeSup α] [SemilatticeSup β] [BoundedOrder β] {s t : Finset α} {a : α} private lemma sup_aux [@DecidableRel α (· ≤ ·)] : a ∈ lowerClosure s → {b ∈ s | a ≤ b}.Nonempty := fun ⟨b, hb, hab⟩ ↦ ⟨b, mem_filter.2 ⟨hb, hab⟩⟩ @@ -283,7 +282,7 @@ lemma truncatedInf_sups_of_not_mem (ha : a ∉ upperClosure s ⊔ upperClosure t end DistribLattice section BooleanAlgebra -variable [BooleanAlgebra α] [@DecidableRel α (· ≤ ·)] {s : Finset α} {a : α} +variable [BooleanAlgebra α] [@DecidableRel α (· ≤ ·)] @[simp] lemma compl_truncatedSup (s : Finset α) (a : α) : (truncatedSup s a)ᶜ = truncatedInf sᶜˢ aᶜ := map_truncatedSup (OrderIso.compl α) _ _ @@ -329,7 +328,7 @@ open Finset hiding card open Fintype Nat namespace AhlswedeZhang -variable {α : Type*} [Fintype α] [DecidableEq α] {𝒜 ℬ : Finset (Finset α)} {s : Finset α} +variable {α : Type*} [Fintype α] [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} /-- Weighted sum of the size of the truncated infima of a set family. Relevant to the Ahlswede-Zhang identity. -/ diff --git a/Mathlib/Combinatorics/SetFamily/Compression/UV.lean b/Mathlib/Combinatorics/SetFamily/Compression/UV.lean index 537a0a3db2b6f..cb2a27b1ef1eb 100644 --- a/Mathlib/Combinatorics/SetFamily/Compression/UV.lean +++ b/Mathlib/Combinatorics/SetFamily/Compression/UV.lean @@ -70,7 +70,7 @@ namespace UV section GeneralizedBooleanAlgebra variable [GeneralizedBooleanAlgebra α] [DecidableRel (@Disjoint α _ _)] - [DecidableRel ((· ≤ ·) : α → α → Prop)] {s : Finset α} {u v a b : α} + [DecidableRel ((· ≤ ·) : α → α → Prop)] {s : Finset α} {u v a : α} /-- UV-compressing `a` means removing `v` from it and adding `u` if `a` and `u` are disjoint and `v ≤ a` (it replaces the `v` part of `a` by the `u` part). Else, UV-compressing `a` doesn't do @@ -265,7 +265,7 @@ end GeneralizedBooleanAlgebra open FinsetFamily -variable [DecidableEq α] {𝒜 : Finset (Finset α)} {u v a : Finset α} {r : ℕ} +variable [DecidableEq α] {𝒜 : Finset (Finset α)} {u v : Finset α} {r : ℕ} /-- Compressing a finset doesn't change its size. -/ theorem card_compress (huv : #u = #v) (a : Finset α) : #(compress u v a) = #a := by diff --git a/Mathlib/Combinatorics/SetFamily/FourFunctions.lean b/Mathlib/Combinatorics/SetFamily/FourFunctions.lean index 6f6dbafc9c630..7e044d51a7439 100644 --- a/Mathlib/Combinatorics/SetFamily/FourFunctions.lean +++ b/Mathlib/Combinatorics/SetFamily/FourFunctions.lean @@ -58,8 +58,8 @@ open scoped FinsetFamily variable {α β : Type*} section Finset -variable [DecidableEq α] [LinearOrderedCommSemiring β] {𝒜 ℬ : Finset (Finset α)} - {a : α} {f f₁ f₂ f₃ f₄ g μ : Finset α → β} {s t u : Finset α} +variable [DecidableEq α] [LinearOrderedCommSemiring β] {𝒜 : Finset (Finset α)} + {a : α} {f f₁ f₂ f₃ f₄ : Finset α → β} {s t u : Finset α} /-- The `n = 1` case of the Ahlswede-Daykin inequality. Note that we can't just expand everything out and bound termwise since `c₀ * d₁` appears twice on the RHS of the assumptions while `c₁ * d₀` diff --git a/Mathlib/Data/Finset/Sups.lean b/Mathlib/Data/Finset/Sups.lean index 15185f0898be6..0b2bf2e8a4359 100644 --- a/Mathlib/Data/Finset/Sups.lean +++ b/Mathlib/Data/Finset/Sups.lean @@ -356,7 +356,7 @@ end DistribLattice section Finset variable [DecidableEq α] -variable {𝒜 ℬ : Finset (Finset α)} {s t : Finset α} {a : α} +variable {𝒜 ℬ : Finset (Finset α)} {s t : Finset α} @[simp] lemma powerset_union (s t : Finset α) : (s ∪ t).powerset = s.powerset ⊻ t.powerset := by ext u @@ -508,7 +508,7 @@ theorem disjSups_disjSups_disjSups_comm : s ○ t ○ (u ○ v) = s ○ u ○ (t end DistribLattice section Diffs variable [DecidableEq α] -variable [GeneralizedBooleanAlgebra α] (s s₁ s₂ t t₁ t₂ u v : Finset α) +variable [GeneralizedBooleanAlgebra α] (s s₁ s₂ t t₁ t₂ u : Finset α) /-- `s \\ t` is the finset of elements of the form `a \ b` where `a ∈ s`, `b ∈ t`. -/ def diffs : Finset α → Finset α → Finset α := image₂ (· \ ·) @@ -592,7 +592,7 @@ lemma diffs_right_comm : s \\ t \\ u = s \\ u \\ t := image₂_right_comm sdiff_ end Diffs section Compls -variable [BooleanAlgebra α] (s s₁ s₂ t t₁ t₂ u v : Finset α) +variable [BooleanAlgebra α] (s s₁ s₂ t : Finset α) /-- `sᶜˢ` is the finset of elements of the form `aᶜ` where `a ∈ s`. -/ def compls : Finset α → Finset α := map ⟨compl, compl_injective⟩ @@ -602,7 +602,7 @@ scoped[FinsetFamily] postfix:max "ᶜˢ" => Finset.compls open FinsetFamily -variable {s t} {a b c : α} +variable {s t} {a : α} @[simp] lemma mem_compls : a ∈ sᶜˢ ↔ aᶜ ∈ s := by rw [Iff.comm, ← mem_map' ⟨compl, compl_injective⟩, Embedding.coeFn_mk, compl_compl, compls] @@ -615,7 +615,7 @@ variable (s t) @[simp] lemma card_compls : #sᶜˢ = #s := card_map _ -variable {s s₁ s₂ t t₁ t₂ u} +variable {s s₁ s₂ t} lemma compl_mem_compls : a ∈ s → aᶜ ∈ sᶜˢ := mem_map_of_mem _ @[simp] lemma compls_subset_compls : s₁ᶜˢ ⊆ s₂ᶜˢ ↔ s₁ ⊆ s₂ := map_subset_map diff --git a/Mathlib/GroupTheory/GroupAction/Blocks.lean b/Mathlib/GroupTheory/GroupAction/Blocks.lean index 054bfb7524698..8359ba6ca7c44 100644 --- a/Mathlib/GroupTheory/GroupAction/Blocks.lean +++ b/Mathlib/GroupTheory/GroupAction/Blocks.lean @@ -348,7 +348,7 @@ theorem IsBlockSystem.of_normal {N : Subgroup G} [N.Normal] : exact .orbit_of_normal a section Group -variable {S H : Type*} [Group H] [SetLike S H] [SubgroupClass S H] {s : S} {a b : G} +variable {S H : Type*} [Group H] [SetLike S H] [SubgroupClass S H] {s : S} {a : G} /-! Annoyingly, it seems like the following two lemmas cannot be unified. diff --git a/Mathlib/GroupTheory/GroupAction/Support.lean b/Mathlib/GroupTheory/GroupAction/Support.lean index 392881eb03ad9..bda425911ec09 100644 --- a/Mathlib/GroupTheory/GroupAction/Support.lean +++ b/Mathlib/GroupTheory/GroupAction/Support.lean @@ -44,7 +44,7 @@ theorem Supports.mono (h : s ⊆ t) (hs : Supports G s b) : Supports G t b := fu end SMul variable [Group H] [SMul G α] [SMul G β] [MulAction H α] [SMul H β] [SMulCommClass G H β] - [SMulCommClass G H α] {s t : Set α} {b : β} + [SMulCommClass G H α] {s : Set α} {b : β} -- TODO: This should work without `SMulCommClass` @[to_additive] diff --git a/Mathlib/GroupTheory/Order/Min.lean b/Mathlib/GroupTheory/Order/Min.lean index 6cbf10250be02..3d1047b06f179 100644 --- a/Mathlib/GroupTheory/Order/Min.lean +++ b/Mathlib/GroupTheory/Order/Min.lean @@ -49,7 +49,7 @@ lemma minOrder_le_orderOf (ha : a ≠ 1) (ha' : IsOfFinOrder a) : minOrder α end Monoid -variable [Group α] {s : Subgroup α} {n : ℕ} +variable [Group α] {s : Subgroup α} @[to_additive] lemma le_minOrder_iff_forall_subgroup {n : ℕ∞} : diff --git a/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean b/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean index 624873b85abc2..806d527b92bc4 100644 --- a/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean +++ b/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean @@ -118,7 +118,7 @@ end List namespace Cycle -variable [DecidableEq α] (s s' : Cycle α) +variable [DecidableEq α] (s : Cycle α) /-- A cycle `s : Cycle α`, given `Nodup s` can be interpreted as an `Equiv.Perm α` where each element in the list is permuted to the next one, defined as `formPerm`. diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index 5b0fb0f4e2877..27fae6ed0d462 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -21,10 +21,9 @@ import Mathlib.LinearAlgebra.BilinearForm.Hom suppress_compilation -universe u v w uι uR uA uM₁ uM₂ uN₁ uN₂ +universe u v w uR uA uM₁ uM₂ uN₁ uN₂ -variable {ι : Type uι} {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁} - {N₂ : Type uN₂} +variable {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁} {N₂ : Type uN₂} open TensorProduct diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean index 8f6b4168968e9..410d9c7363d47 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean @@ -46,7 +46,6 @@ This file is almost identical to `Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.le variable {R : Type*} [CommRing R] variable {M : Type*} [AddCommGroup M] [Module R M] variable (Q : QuadraticForm R M) -variable {n : ℕ} namespace CliffordAlgebra diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean index 2285548a3e107..82b7f5635657c 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean @@ -354,7 +354,7 @@ open scoped DualNumber open DualNumber TrivSqZeroExt -variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] +variable {R : Type*} [CommRing R] theorem ι_mul_ι (r₁ r₂) : ι (0 : QuadraticForm R R) r₁ * ι (0 : QuadraticForm R R) r₂ = 0 := by rw [← mul_one r₁, ← mul_one r₂, ← smul_eq_mul R, ← smul_eq_mul R, LinearMap.map_smul, diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Isometry.lean b/Mathlib/LinearAlgebra/QuadraticForm/Isometry.lean index c662062c74bc4..4208354f24bc0 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Isometry.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Isometry.lean @@ -17,7 +17,7 @@ import Mathlib.LinearAlgebra.QuadraticForm.Basic `Q₁ →qᵢ Q₂` is notation for `Q₁.Isometry Q₂`. -/ -variable {ι R M M₁ M₂ M₃ M₄ N : Type*} +variable {R M M₁ M₂ M₃ M₄ N : Type*} namespace QuadraticMap diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean b/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean index e6c65901442b7..328b2319e0765 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean @@ -346,9 +346,7 @@ end Semiring namespace Ring variable [CommRing R] -variable [∀ i, AddCommGroup (Mᵢ i)] [∀ i, AddCommGroup (Nᵢ i)] [AddCommGroup P] -variable [∀ i, Module R (Mᵢ i)] [∀ i, Module R (Nᵢ i)] [Module R P] -variable [Fintype ι] +variable [∀ i, AddCommGroup (Mᵢ i)] [AddCommGroup P] [∀ i, Module R (Mᵢ i)] [Module R P] [Fintype ι] @[simp] theorem polar_pi (Q : ∀ i, QuadraticMap R (Mᵢ i) P) (x y : ∀ i, Mᵢ i) : polar (pi Q) x y = ∑ i, polar (Q i) (x i) (y i) := by diff --git a/Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean b/Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean index e9896dd5d9c21..de51f0a712aab 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean @@ -47,7 +47,7 @@ suppress_compilation open scoped TensorProduct DirectSum -variable {R ι A B : Type*} +variable {R ι : Type*} namespace TensorProduct diff --git a/Mathlib/Order/Filter/Cocardinal.lean b/Mathlib/Order/Filter/Cocardinal.lean index b0fed85fce86e..25e10e20a8fa3 100644 --- a/Mathlib/Order/Filter/Cocardinal.lean +++ b/Mathlib/Order/Filter/Cocardinal.lean @@ -22,9 +22,7 @@ In this file we define `Filter.cocardinal hc`: the filter of sets with cardinali open Set Filter Cardinal universe u -variable {ι : Type u} {α β : Type u} -variable {c : Cardinal.{u}} {hreg : c.IsRegular} -variable {l : Filter α} +variable {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} namespace Filter diff --git a/Mathlib/Order/KonigLemma.lean b/Mathlib/Order/KonigLemma.lean index b38fa275198d5..3e2ecf7719504 100644 --- a/Mathlib/Order/KonigLemma.lean +++ b/Mathlib/Order/KonigLemma.lean @@ -51,7 +51,7 @@ Formulate the lemma as a statement about graphs. open Set section Sequence -variable {α : Type*} [PartialOrder α] [IsStronglyAtomic α] {a b : α} +variable {α : Type*} [PartialOrder α] [IsStronglyAtomic α] {b : α} /-- **Kőnig's infinity lemma** : if each element in a strongly atomic order is covered by only finitely many others, and `b` is an element with infinitely many things above it, diff --git a/Mathlib/Order/PFilter.lean b/Mathlib/Order/PFilter.lean index 5e663221d21fc..d461174544550 100644 --- a/Mathlib/Order/PFilter.lean +++ b/Mathlib/Order/PFilter.lean @@ -143,7 +143,7 @@ end SemilatticeInf section CompleteSemilatticeInf -variable [CompleteSemilatticeInf P] {F : PFilter P} +variable [CompleteSemilatticeInf P] theorem sInf_gc : GaloisConnection (fun x => toDual (principal x)) fun F => sInf (ofDual F : PFilter P) := diff --git a/Mathlib/RingTheory/WittVector/Defs.lean b/Mathlib/RingTheory/WittVector/Defs.lean index 5003404660142..859c75ad0e563 100644 --- a/Mathlib/RingTheory/WittVector/Defs.lean +++ b/Mathlib/RingTheory/WittVector/Defs.lean @@ -156,8 +156,6 @@ evaluating this at `(x₀, x₁)` gives us the sum of two Witt vectors `x₀ + x def eval {k : ℕ} (φ : ℕ → MvPolynomial (Fin k × ℕ) ℤ) (x : Fin k → 𝕎 R) : 𝕎 R := mk p fun n => peval (φ n) fun i => (x i).coeff -variable (R) [Fact p.Prime] - instance : Zero (𝕎 R) := ⟨eval (wittZero p) ![]⟩ diff --git a/Mathlib/Tactic/Widget/StringDiagram.lean b/Mathlib/Tactic/Widget/StringDiagram.lean index 9ba22761bcd5e..c2745df6eff9a 100644 --- a/Mathlib/Tactic/Widget/StringDiagram.lean +++ b/Mathlib/Tactic/Widget/StringDiagram.lean @@ -182,7 +182,7 @@ def WhiskerLeft.nodes (v h₁ h₂ : ℕ) : WhiskerLeft → List Node let ss := η.nodes v (h₁ + 1) (h₂ + 1) s :: ss -variable {ρ : Type} [Context ρ] [MonadMor₁ (CoherenceM ρ)] +variable {ρ : Type} [MonadMor₁ (CoherenceM ρ)] /-- The list of nodes at the top of a string diagram. -/ def topNodes (η : WhiskerLeft) : CoherenceM ρ (List Node) := do diff --git a/Mathlib/Topology/ContinuousMap/CompactlySupported.lean b/Mathlib/Topology/ContinuousMap/CompactlySupported.lean index cea48f4937a02..cb59956edbce0 100644 --- a/Mathlib/Topology/ContinuousMap/CompactlySupported.lean +++ b/Mathlib/Topology/ContinuousMap/CompactlySupported.lean @@ -447,8 +447,6 @@ theorem zero_comp (g : β →co γ) : (0 : C_c(γ, δ)).comp g = 0 := end -variable [T2Space γ] - /-- Composition as an additive monoid homomorphism. -/ def compAddMonoidHom [AddMonoid δ] [ContinuousAdd δ] (g : β →co γ) : C_c(γ, δ) →+ C_c(β, δ) where toFun f := f.comp g diff --git a/Mathlib/Topology/FiberBundle/Trivialization.lean b/Mathlib/Topology/FiberBundle/Trivialization.lean index 87a1362341a73..dfc2f24a5deeb 100644 --- a/Mathlib/Topology/FiberBundle/Trivialization.lean +++ b/Mathlib/Topology/FiberBundle/Trivialization.lean @@ -50,7 +50,7 @@ type of linear trivializations is not even particularly well-behaved. open TopologicalSpace Filter Set Bundle Function open scoped Topology -variable {ι : Type*} {B : Type*} (F : Type*) {E : B → Type*} +variable {B : Type*} (F : Type*) {E : B → Type*} variable {Z : Type*} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} /-- This structure contains the information left for a local trivialization (which is implemented @@ -194,7 +194,7 @@ theorem symm_trans_target_eq (e e' : Pretrivialization F proj) : (e.toPartialEquiv.symm.trans e'.toPartialEquiv).target = (e.baseSet ∩ e'.baseSet) ×ˢ univ := by rw [← PartialEquiv.symm_source, symm_trans_symm, symm_trans_source_eq, inter_comm] -variable (e' : Pretrivialization F (π F E)) {x' : TotalSpace F E} {b : B} {y : E b} +variable (e' : Pretrivialization F (π F E)) {b : B} {y : E b} @[simp] theorem coe_mem_source : ↑y ∈ e'.source ↔ b ∈ e'.baseSet := @@ -502,7 +502,7 @@ theorem continuousAt_of_comp_left {X : Type*} [TopologicalSpace X] {f : X → Z} rw [e.source_eq, ← preimage_comp] exact hf_proj.preimage_mem_nhds (e.open_baseSet.mem_nhds he) -variable (e' : Trivialization F (π F E)) {x' : TotalSpace F E} {b : B} {y : E b} +variable (e' : Trivialization F (π F E)) {b : B} {y : E b} protected theorem continuousOn : ContinuousOn e' e'.source := e'.continuousOn_toFun @@ -643,8 +643,6 @@ theorem coordChangeHomeomorph_coe (e₁ e₂ : Trivialization F proj) {b : B} (h (h₂ : b ∈ e₂.baseSet) : ⇑(e₁.coordChangeHomeomorph e₂ h₁ h₂) = e₁.coordChange e₂ b := rfl -variable {B' : Type*} [TopologicalSpace B'] - theorem isImage_preimage_prod (e : Trivialization F proj) (s : Set B) : e.toPartialHomeomorph.IsImage (proj ⁻¹' s) (s ×ˢ univ) := fun x hx => by simp [e.coe_fst', hx]