From a154f5e68ada13509a7ed86aa5c92d2e04ed3550 Mon Sep 17 00:00:00 2001 From: leanprover-community-bot Date: Thu, 14 Dec 2023 06:39:51 +0000 Subject: [PATCH] bump to nightly-2023-12-14-06 mathlib commit https://github.com/leanprover-community/mathlib/commit/65a1391a0106c9204fe45bc73a039f056558cb83 --- Mathbin/Algebra/IndicatorFunction.lean | 40 +- Mathbin/Algebra/Star/Basic.lean | 6 +- Mathbin/Algebra/Support.lean | 14 +- Mathbin/Analysis/Calculus/Inverse.lean | 16 +- .../SpecialFunctions/Complex/Circle.lean | 14 +- Mathbin/Control/Random.lean | 21 +- Mathbin/Geometry/Euclidean/Circumcenter.lean | 4 +- Mathbin/Geometry/Manifold/ChartedSpace.lean | 25 +- Mathbin/Geometry/Manifold/ContMdiff.lean | 12 +- .../Geometry/Manifold/ContMdiffMfderiv.lean | 6 +- Mathbin/Geometry/Manifold/Diffeomorph.lean | 2 +- .../Geometry/Manifold/Instances/Sphere.lean | 4 +- .../Manifold/SmoothManifoldWithCorners.lean | 62 +- .../Geometry/Manifold/VectorBundle/Basic.lean | 12 +- .../VectorBundle/FiberwiseLinear.lean | 4 +- .../Manifold/VectorBundle/Tangent.lean | 23 +- .../AffineSpace/Combination.lean | 7 +- .../AffineSpace/Independent.lean | 10 +- Mathbin/Logic/Equiv/LocalEquiv.lean | 806 +++++++++--------- Mathbin/MeasureTheory/Function/Jacobian.lean | 2 +- .../Function/UniformIntegrable.lean | 2 +- .../Probability/Martingale/Upcrossing.lean | 2 +- .../Topology/Algebra/InfiniteSum/Basic.lean | 2 +- Mathbin/Topology/Covering.lean | 2 +- Mathbin/Topology/FiberBundle/Basic.lean | 94 +- .../Topology/FiberBundle/Constructions.lean | 2 +- .../Topology/FiberBundle/Trivialization.lean | 67 +- Mathbin/Topology/LocalHomeomorph.lean | 212 ++--- Mathbin/Topology/VectorBundle/Hom.lean | 2 +- lake-manifest.json | 8 +- lakefile.lean | 4 +- 31 files changed, 749 insertions(+), 738 deletions(-) diff --git a/Mathbin/Algebra/IndicatorFunction.lean b/Mathbin/Algebra/IndicatorFunction.lean index 005c80cfdb..505cd3793c 100644 --- a/Mathbin/Algebra/IndicatorFunction.lean +++ b/Mathbin/Algebra/IndicatorFunction.lean @@ -686,7 +686,7 @@ section CommMonoid variable [CommMonoid M] -#print Set.prod_mulIndicator_subset_of_eq_one /- +#print Finset.prod_mulIndicator_subset_of_eq_one /- /-- Consider a product of `g i (f i)` over a `finset`. Suppose `g` is a function such as `pow`, which maps a second argument of `1` to `1`. Then if `f` is replaced by the corresponding multiplicative indicator @@ -706,8 +706,8 @@ theorem prod_mulIndicator_subset_of_eq_one [One N] (f : α → N) (g : α → N · refine' fun i hi hn => _ convert hg i exact mul_indicator_of_not_mem hn _ -#align set.prod_mul_indicator_subset_of_eq_one Set.prod_mulIndicator_subset_of_eq_one -#align set.sum_indicator_subset_of_eq_zero Set.sum_indicator_subset_of_eq_zero +#align set.prod_mul_indicator_subset_of_eq_one Finset.prod_mulIndicator_subset_of_eq_one +#align set.sum_indicator_subset_of_eq_zero Finset.sum_indicator_subset_of_eq_zero -/ /-- Consider a sum of `g i (f i)` over a `finset`. Suppose `g` is a @@ -717,9 +717,9 @@ function such as multiplication, which maps a second argument of 0 to function `h`.) Then if `f` is replaced by the corresponding indicator function, the `finset` may be replaced by a possibly larger `finset` without changing the value of the sum. -/ -add_decl_doc Set.sum_indicator_subset_of_eq_zero +add_decl_doc Finset.sum_indicator_subset_of_eq_zero -#print Set.prod_mulIndicator_subset /- +#print Finset.prod_mulIndicator_subset /- /-- Taking the product of an indicator function over a possibly larger `finset` is the same as taking the original function over the original `finset`. -/ @[to_additive @@ -727,8 +727,8 @@ taking the original function over the original `finset`. -/ theorem prod_mulIndicator_subset (f : α → M) {s t : Finset α} (h : s ⊆ t) : ∏ i in s, f i = ∏ i in t, mulIndicator (↑s) f i := prod_mulIndicator_subset_of_eq_one _ (fun a b => b) h fun _ => rfl -#align set.prod_mul_indicator_subset Set.prod_mulIndicator_subset -#align set.sum_indicator_subset Set.sum_indicator_subset +#align set.prod_mul_indicator_subset Finset.prod_mulIndicator_subset +#align set.sum_indicator_subset Finset.sum_indicator_subset -/ #print Finset.prod_mulIndicator_eq_prod_filter /- @@ -747,18 +747,18 @@ theorem Finset.prod_mulIndicator_eq_prod_filter (s : Finset ι) (f : ι → α #align finset.sum_indicator_eq_sum_filter Finset.sum_indicator_eq_sum_filter -/ -#print Set.mulIndicator_finset_prod /- +#print Finset.mulIndicator_prod /- @[to_additive] -theorem mulIndicator_finset_prod (I : Finset ι) (s : Set α) (f : ι → α → M) : +theorem mulIndicator_prod (I : Finset ι) (s : Set α) (f : ι → α → M) : mulIndicator s (∏ i in I, f i) = ∏ i in I, mulIndicator s (f i) := (mulIndicatorHom M s).map_prod _ _ -#align set.mul_indicator_finset_prod Set.mulIndicator_finset_prod -#align set.indicator_finset_sum Set.indicator_finset_sum +#align set.mul_indicator_finset_prod Finset.mulIndicator_prod +#align set.indicator_finset_sum Finset.indicator_sum -/ -#print Set.mulIndicator_finset_biUnion /- +#print Finset.mulIndicator_biUnion /- @[to_additive] -theorem mulIndicator_finset_biUnion {ι} (I : Finset ι) (s : ι → Set α) {f : α → M} : +theorem mulIndicator_biUnion {ι} (I : Finset ι) (s : ι → Set α) {f : α → M} : (∀ i ∈ I, ∀ j ∈ I, i ≠ j → Disjoint (s i) (s j)) → mulIndicator (⋃ i ∈ I, s i) f = fun a => ∏ i in I, mulIndicator (s i) f a := by @@ -774,18 +774,18 @@ theorem mulIndicator_finset_biUnion {ι} (I : Finset ι) (s : ι → Set α) {f intro hx a' ha' refine' disjoint_left.1 (hI a (Finset.mem_insert_self _ _) a' (Finset.mem_insert_of_mem ha') _) hx exact (ne_of_mem_of_not_mem ha' haI).symm -#align set.mul_indicator_finset_bUnion Set.mulIndicator_finset_biUnion -#align set.indicator_finset_bUnion Set.indicator_finset_biUnion +#align set.mul_indicator_finset_bUnion Finset.mulIndicator_biUnion +#align set.indicator_finset_bUnion Finset.indicator_biUnion -/ -#print Set.mulIndicator_finset_biUnion_apply /- +#print Finset.mulIndicator_biUnion_apply /- @[to_additive] -theorem mulIndicator_finset_biUnion_apply {ι} (I : Finset ι) (s : ι → Set α) {f : α → M} +theorem mulIndicator_biUnion_apply {ι} (I : Finset ι) (s : ι → Set α) {f : α → M} (h : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → Disjoint (s i) (s j)) (x : α) : mulIndicator (⋃ i ∈ I, s i) f x = ∏ i in I, mulIndicator (s i) f x := by - rw [Set.mulIndicator_finset_biUnion I s h] -#align set.mul_indicator_finset_bUnion_apply Set.mulIndicator_finset_biUnion_apply -#align set.indicator_finset_bUnion_apply Set.indicator_finset_biUnion_apply + rw [Finset.mulIndicator_biUnion I s h] +#align set.mul_indicator_finset_bUnion_apply Finset.mulIndicator_biUnion_apply +#align set.indicator_finset_bUnion_apply Finset.indicator_biUnion_apply -/ end CommMonoid diff --git a/Mathbin/Algebra/Star/Basic.lean b/Mathbin/Algebra/Star/Basic.lean index e3eef4a73e..e3609a5966 100644 --- a/Mathbin/Algebra/Star/Basic.lean +++ b/Mathbin/Algebra/Star/Basic.lean @@ -565,11 +565,11 @@ export StarModule (star_smul) attribute [simp] star_smul -#print StarSemigroup.to_starModule /- +#print StarMul.toStarModule /- /-- A commutative star monoid is a star module over itself via `monoid.to_mul_action`. -/ -instance StarSemigroup.to_starModule [CommMonoid R] [StarMul R] : StarModule R R := +instance StarMul.toStarModule [CommMonoid R] [StarMul R] : StarModule R R := ⟨star_mul'⟩ -#align star_semigroup.to_star_module StarSemigroup.to_starModule +#align star_semigroup.to_star_module StarMul.toStarModule -/ namespace RingHomInvPair diff --git a/Mathbin/Algebra/Support.lean b/Mathbin/Algebra/Support.lean index 65cf9a8d3a..c2b231be8c 100644 --- a/Mathbin/Algebra/Support.lean +++ b/Mathbin/Algebra/Support.lean @@ -499,7 +499,7 @@ theorem support_div [GroupWithZero G₀] (f g : α → G₀) : #align function.support_div Function.support_div -/ -#print Function.mulSupport_prod /- +#print Finset.mulSupport_prod /- @[to_additive] theorem mulSupport_prod [CommMonoid M] (s : Finset α) (f : α → β → M) : (mulSupport fun x => ∏ i in s, f i x) ⊆ ⋃ i ∈ s, mulSupport (f i) := @@ -507,23 +507,23 @@ theorem mulSupport_prod [CommMonoid M] (s : Finset α) (f : α → β → M) : rw [mul_support_subset_iff'] simp only [mem_Union, not_exists, nmem_mul_support] exact fun x => Finset.prod_eq_one -#align function.mul_support_prod Function.mulSupport_prod -#align function.support_sum Function.support_sum +#align function.mul_support_prod Finset.mulSupport_prod +#align function.support_sum Finset.support_sum -/ -#print Function.support_prod_subset /- +#print Finset.support_prod_subset /- theorem support_prod_subset [CommMonoidWithZero A] (s : Finset α) (f : α → β → A) : (support fun x => ∏ i in s, f i x) ⊆ ⋂ i ∈ s, support (f i) := fun x hx => mem_iInter₂.2 fun i hi H => hx <| Finset.prod_eq_zero hi H -#align function.support_prod_subset Function.support_prod_subset +#align function.support_prod_subset Finset.support_prod_subset -/ -#print Function.support_prod /- +#print Finset.support_prod /- theorem support_prod [CommMonoidWithZero A] [NoZeroDivisors A] [Nontrivial A] (s : Finset α) (f : α → β → A) : (support fun x => ∏ i in s, f i x) = ⋂ i ∈ s, support (f i) := Set.ext fun x => by simp only [support, Ne.def, Finset.prod_eq_zero_iff, mem_set_of_eq, Set.mem_iInter, not_exists] -#align function.support_prod Function.support_prod +#align function.support_prod Finset.support_prod -/ #print Function.mulSupport_one_add /- diff --git a/Mathbin/Analysis/Calculus/Inverse.lean b/Mathbin/Analysis/Calculus/Inverse.lean index 33d92a4219..9fdfb1630c 100644 --- a/Mathbin/Analysis/Calculus/Inverse.lean +++ b/Mathbin/Analysis/Calculus/Inverse.lean @@ -472,21 +472,21 @@ protected theorem surjective [CompleteSpace E] (hf : ApproximatesLinearOn f (f' #align approximates_linear_on.surjective ApproximatesLinearOn.surjective -/ -#print ApproximatesLinearOn.toLocalEquiv /- +#print ApproximatesLinearOn.toPartialEquiv /- /-- A map approximating a linear equivalence on a set defines a local equivalence on this set. Should not be used outside of this file, because it is superseded by `to_local_homeomorph` below. This is a first step towards the inverse function. -/ -def toLocalEquiv (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c) - (hc : Subsingleton E ∨ c < N⁻¹) : LocalEquiv E F := - (hf.InjOn hc).toLocalEquiv _ _ -#align approximates_linear_on.to_local_equiv ApproximatesLinearOn.toLocalEquiv +def toPartialEquiv (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c) + (hc : Subsingleton E ∨ c < N⁻¹) : PartialEquiv E F := + (hf.InjOn hc).toPartialEquiv _ _ +#align approximates_linear_on.to_local_equiv ApproximatesLinearOn.toPartialEquiv -/ #print ApproximatesLinearOn.inverse_continuousOn /- /-- The inverse function is continuous on `f '' s`. Use properties of `local_homeomorph` instead. -/ theorem inverse_continuousOn (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c) - (hc : Subsingleton E ∨ c < N⁻¹) : ContinuousOn (hf.toLocalEquiv hc).symm (f '' s) := + (hc : Subsingleton E ∨ c < N⁻¹) : ContinuousOn (hf.toPartialEquiv hc).symm (f '' s) := by apply continuousOn_iff_continuous_restrict.2 refine' ((hf.antilipschitz hc).to_rightInvOn' _ (hf.to_local_equiv hc).right_inv').Continuous @@ -497,7 +497,7 @@ theorem inverse_continuousOn (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) #print ApproximatesLinearOn.to_inv /- /-- The inverse function is approximated linearly on `f '' s` by `f'.symm`. -/ theorem to_inv (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c) (hc : Subsingleton E ∨ c < N⁻¹) : - ApproximatesLinearOn (hf.toLocalEquiv hc).symm (f'.symm : F →L[𝕜] E) (f '' s) + ApproximatesLinearOn (hf.toPartialEquiv hc).symm (f'.symm : F →L[𝕜] E) (f '' s) (N * (N⁻¹ - c)⁻¹ * c) := by intro x hx y hy @@ -534,7 +534,7 @@ returns a local homeomorph with `to_fun = f` and `source = s`. -/ def toPartialHomeomorph (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c) (hc : Subsingleton E ∨ c < N⁻¹) (hs : IsOpen s) : PartialHomeomorph E F where - toLocalEquiv := hf.toLocalEquiv hc + toPartialEquiv := hf.toPartialEquiv hc open_source := hs open_target := hf.open_image f'.toNonlinearRightInverse hs diff --git a/Mathbin/Analysis/SpecialFunctions/Complex/Circle.lean b/Mathbin/Analysis/SpecialFunctions/Complex/Circle.lean index 5c49d3ea39..2679cf2349 100644 --- a/Mathbin/Analysis/SpecialFunctions/Complex/Circle.lean +++ b/Mathbin/Analysis/SpecialFunctions/Complex/Circle.lean @@ -56,11 +56,11 @@ theorem expMapCircle_arg (z : circle) : expMapCircle (arg z) = z := namespace circle -#print circle.argLocalEquiv /- +#print circle.argPartialEquiv /- /-- `complex.arg ∘ coe` and `exp_map_circle` define a local equivalence between `circle and `ℝ` with `source = set.univ` and `target = set.Ioc (-π) π`. -/ @[simps (config := { fullyApplied := false })] -noncomputable def argLocalEquiv : LocalEquiv circle ℝ +noncomputable def argPartialEquiv : PartialEquiv circle ℝ where toFun := arg ∘ coe invFun := expMapCircle @@ -70,7 +70,7 @@ noncomputable def argLocalEquiv : LocalEquiv circle ℝ map_target' := mapsTo_univ _ _ left_inv' z _ := expMapCircle_arg z right_inv' x hx := arg_expMapCircle hx.1 hx.2 -#align circle.arg_local_equiv circle.argLocalEquiv +#align circle.arg_local_equiv circle.argPartialEquiv -/ #print circle.argEquiv /- @@ -80,8 +80,8 @@ noncomputable def argEquiv : circle ≃ Ioc (-π) π where toFun z := ⟨arg z, neg_pi_lt_arg _, arg_le_pi _⟩ invFun := expMapCircle ∘ coe - left_inv z := argLocalEquiv.left_inv trivial - right_inv x := Subtype.ext <| argLocalEquiv.right_inv x.2 + left_inv z := argPartialEquiv.left_inv trivial + right_inv x := Subtype.ext <| argPartialEquiv.right_inv x.2 #align circle.arg_equiv circle.argEquiv -/ @@ -95,13 +95,13 @@ theorem leftInverse_expMapCircle_arg : LeftInverse expMapCircle (arg ∘ coe) := #print invOn_arg_expMapCircle /- theorem invOn_arg_expMapCircle : InvOn (arg ∘ coe) expMapCircle (Ioc (-π) π) univ := - circle.argLocalEquiv.symm.InvOn + circle.argPartialEquiv.symm.InvOn #align inv_on_arg_exp_map_circle invOn_arg_expMapCircle -/ #print surjOn_expMapCircle_neg_pi_pi /- theorem surjOn_expMapCircle_neg_pi_pi : SurjOn expMapCircle (Ioc (-π) π) univ := - circle.argLocalEquiv.symm.SurjOn + circle.argPartialEquiv.symm.SurjOn #align surj_on_exp_map_circle_neg_pi_pi surjOn_expMapCircle_neg_pi_pi -/ diff --git a/Mathbin/Control/Random.lean b/Mathbin/Control/Random.lean index f245b52ae4..5530c7876b 100644 --- a/Mathbin/Control/Random.lean +++ b/Mathbin/Control/Random.lean @@ -79,20 +79,16 @@ local infixl:41 " .. " => Set.Icc open Stream' -#print BoundedRandom /- /-- `bounded_random α` gives us machinery to generate values of type `α` between certain bounds -/ class BoundedRandom (α : Type u) [Preorder α] where randomR : ∀ (g) [RandomGen g] (x y : α), x ≤ y → RandG g (x .. y) -#align bounded_random BoundedRandom --/ +#align bounded_random BoundedRandomₓ -#print Random /- -/- ./././Mathport/Syntax/Translate/Command.lean:394:30: infer kinds are unsupported in Lean 4: #[`Random] [] -/ +/- ./././Mathport/Syntax/Translate/Command.lean:394:30: infer kinds are unsupported in Lean 4: #[`Randomₓ] [] -/ /-- `random α` gives us machinery to generate values of type `α` -/ class Random (α : Type u) where - Random : ∀ (g : Type) [RandomGen g], RandG g α -#align random Random --/ + Randomₓ : ∀ (g : Type) [RandomGen g], RandG g α +#align random Randomₓ /-- shift_31_left = 2^31; multiplying by it shifts the binary representation of a number left by 31 bits, dividing by it shifts it @@ -121,7 +117,7 @@ section Random variable [Random α] -export Random (Random) +export Random (Randomₓ) /-- Generate a random value of type `α`. -/ def random : RandG g α := @@ -300,7 +296,8 @@ instance intBoundedRandom : BoundedRandom ℤ (le_of_eq <| Int.ofNat_natAbs_eq_of_nonneg (Int.sub_nonneg_of_le hxy))⟩ #align int_bounded_random intBoundedRandom -instance finRandom (n : ℕ) [NeZero n] : Random (Fin n) where Random g inst := @Fin.random g inst _ _ +instance finRandom (n : ℕ) [NeZero n] : Random (Fin n) + where Randomₓ g inst := @Fin.random g inst _ _ #align fin_random finRandom instance finBoundedRandom (n : ℕ) : BoundedRandom (Fin n) @@ -326,7 +323,7 @@ theorem bool_ofNat_mem_Icc_of_mem_Icc_toNat (x y : Bool) (n : ℕ) : #align bool_of_nat_mem_Icc_of_mem_Icc_to_nat bool_ofNat_mem_Icc_of_mem_Icc_toNat instance : Random Bool - where Random g inst := + where Randomₓ g inst := (Bool.ofNat ∘ Subtype.val) <$> @BoundedRandom.randomR ℕ _ _ g inst 0 1 (Nat.zero_le _) instance : BoundedRandom Bool @@ -354,7 +351,7 @@ def Std.BitVec.randomR {n : ℕ} (x y : Std.BitVec n) (h : x ≤ y) : RandG g (x open Nat instance randomBitvec (n : ℕ) : Random (Std.BitVec n) - where Random _ inst := @Std.BitVec.random _ inst n + where Randomₓ _ inst := @Std.BitVec.random _ inst n #align random_bitvec randomBitvec instance boundedRandomBitvec (n : ℕ) : BoundedRandom (Std.BitVec n) diff --git a/Mathbin/Geometry/Euclidean/Circumcenter.lean b/Mathbin/Geometry/Euclidean/Circumcenter.lean index 8e6c230844..0aa321852c 100644 --- a/Mathbin/Geometry/Euclidean/Circumcenter.lean +++ b/Mathbin/Geometry/Euclidean/Circumcenter.lean @@ -725,7 +725,7 @@ theorem sum_centroidWeightsWithCircumcenter {n : ℕ} {fs : Finset (Fin (n + 1)) ∑ i, centroidWeightsWithCircumcenter fs i = 1 := by simp_rw [sum_points_with_circumcenter, centroid_weights_with_circumcenter, add_zero, ← - fs.sum_centroid_weights_eq_one_of_nonempty ℝ h, Set.sum_indicator_subset _ fs.subset_univ] + fs.sum_centroid_weights_eq_one_of_nonempty ℝ h, Finset.sum_indicator_subset _ fs.subset_univ] rcongr #align affine.simplex.sum_centroid_weights_with_circumcenter Affine.Simplex.sum_centroidWeightsWithCircumcenter -/ @@ -742,7 +742,7 @@ theorem centroid_eq_affineCombination_of_pointsWithCircumcenter {n : ℕ} (s : S simp_rw [centroid_def, affine_combination_apply, weighted_vsub_of_point_apply, sum_points_with_circumcenter, centroid_weights_with_circumcenter, points_with_circumcenter_point, zero_smul, add_zero, centroid_weights, - Set.sum_indicator_subset_of_eq_zero (Function.const (Fin (n + 1)) (card fs : ℝ)⁻¹) + Finset.sum_indicator_subset_of_eq_zero (Function.const (Fin (n + 1)) (card fs : ℝ)⁻¹) (fun i wi => wi • (s.points i -ᵥ Classical.choice AddTorsor.nonempty)) fs.subset_univ fun i => zero_smul ℝ _, Set.indicator_apply] diff --git a/Mathbin/Geometry/Manifold/ChartedSpace.lean b/Mathbin/Geometry/Manifold/ChartedSpace.lean index fb49b44432..7eab62d1a7 100644 --- a/Mathbin/Geometry/Manifold/ChartedSpace.lean +++ b/Mathbin/Geometry/Manifold/ChartedSpace.lean @@ -129,7 +129,7 @@ Note that, as is usual for equivs, the composition is from left to right, hence the arrow. -/ scoped[Manifold] infixr:100 " ≫ₕ " => PartialHomeomorph.trans -scoped[Manifold] infixr:100 " ≫ " => LocalEquiv.trans +scoped[Manifold] infixr:100 " ≫ " => PartialEquiv.trans open Set PartialHomeomorph @@ -856,26 +856,27 @@ charts that are only local equivs, and continuity properties for their compositi This is formalised in `charted_space_core`. -/ @[nolint has_nonempty_instance] structure ChartedSpaceCore (H : Type _) [TopologicalSpace H] (M : Type _) where - atlas : Set (LocalEquiv M H) - chartAt : M → LocalEquiv M H + atlas : Set (PartialEquiv M H) + chartAt : M → PartialEquiv M H mem_chart_source : ∀ x, x ∈ (chart_at x).source chart_mem_atlas : ∀ x, chart_at x ∈ atlas - open_source : ∀ e e' : LocalEquiv M H, e ∈ atlas → e' ∈ atlas → IsOpen (e.symm.trans e').source + open_source : ∀ e e' : PartialEquiv M H, e ∈ atlas → e' ∈ atlas → IsOpen (e.symm.trans e').source continuous_toFun : - ∀ e e' : LocalEquiv M H, + ∀ e e' : PartialEquiv M H, e ∈ atlas → e' ∈ atlas → ContinuousOn (e.symm.trans e') (e.symm.trans e').source #align charted_space_core ChartedSpaceCore -/ namespace ChartedSpaceCore -variable [TopologicalSpace H] (c : ChartedSpaceCore H M) {e : LocalEquiv M H} +variable [TopologicalSpace H] (c : ChartedSpaceCore H M) {e : PartialEquiv M H} #print ChartedSpaceCore.toTopologicalSpace /- /-- Topology generated by a set of charts on a Type. -/ protected def toTopologicalSpace : TopologicalSpace M := TopologicalSpace.generateFrom <| - ⋃ (e : LocalEquiv M H) (he : e ∈ c.atlas) (s : Set H) (s_open : IsOpen s), {e ⁻¹' s ∩ e.source} + ⋃ (e : PartialEquiv M H) (he : e ∈ c.atlas) (s : Set H) (s_open : IsOpen s), + {e ⁻¹' s ∩ e.source} #align charted_space_core.to_topological_space ChartedSpaceCore.toTopologicalSpace -/ @@ -894,8 +895,8 @@ theorem open_target (he : e ∈ c.atlas) : IsOpen e.target := by have E : e.target ∩ e.symm ⁻¹' e.source = e.target := subset.antisymm (inter_subset_left _ _) fun x hx => - ⟨hx, LocalEquiv.target_subset_preimage_source _ hx⟩ - simpa [LocalEquiv.trans_source, E] using c.open_source e e he he + ⟨hx, PartialEquiv.target_subset_preimage_source _ hx⟩ + simpa [PartialEquiv.trans_source, E] using c.open_source e e he he #align charted_space_core.open_target ChartedSpaceCore.open_target -/ @@ -903,7 +904,7 @@ theorem open_target (he : e ∈ c.atlas) : IsOpen e.target := /-- An element of the atlas in a charted space without topology becomes a local homeomorphism for the topology constructed from this atlas. The `local_homeomorph` version is given in this definition. -/ -protected def localHomeomorph (e : LocalEquiv M H) (he : e ∈ c.atlas) : +protected def localHomeomorph (e : PartialEquiv M H) (he : e ∈ c.atlas) : @PartialHomeomorph M H c.toTopologicalSpace _ := { e with open_source := by convert c.open_source' he @@ -932,7 +933,7 @@ protected def localHomeomorph (e : LocalEquiv M H) (he : e ∈ c.atlas) : e' ∘ e.symm ⁻¹' s ∩ (e.target ∩ e.symm ⁻¹' e'.source) = e.target ∩ (e' ∘ e.symm ⁻¹' s ∩ e.symm ⁻¹' e'.source) := by rw [← inter_assoc, ← inter_assoc]; congr 1; exact inter_comm _ _ - simpa [LocalEquiv.trans_source, preimage_inter, preimage_comp.symm, A] using this } + simpa [PartialEquiv.trans_source, preimage_inter, preimage_comp.symm, A] using this } #align charted_space_core.local_homeomorph ChartedSpaceCore.localHomeomorph -/ @@ -941,7 +942,7 @@ protected def localHomeomorph (e : LocalEquiv M H) (he : e ∈ c.atlas) : respect to the topology constructed from the atlas. -/ def toChartedSpace : @ChartedSpace H _ M c.toTopologicalSpace where - atlas := ⋃ (e : LocalEquiv M H) (he : e ∈ c.atlas), {c.PartialHomeomorph e he} + atlas := ⋃ (e : PartialEquiv M H) (he : e ∈ c.atlas), {c.PartialHomeomorph e he} chartAt x := c.PartialHomeomorph (c.chartAt x) (c.chart_mem_atlas x) mem_chart_source x := c.mem_chart_source x chart_mem_atlas x := by diff --git a/Mathbin/Geometry/Manifold/ContMdiff.lean b/Mathbin/Geometry/Manifold/ContMdiff.lean index b56ac31b7b..b10897d06e 100644 --- a/Mathbin/Geometry/Manifold/ContMdiff.lean +++ b/Mathbin/Geometry/Manifold/ContMdiff.lean @@ -424,8 +424,8 @@ theorem contMDiffWithinAt_iff_target : exact inter_mem self_mem_nhdsWithin (h.preimage_mem_nhds_within <| (chart_at _ _).open_source.mem_nhds <| mem_chart_source _ _) - simp_rw [Cont, ContDiffWithinAtProp, extChartAt, PartialHomeomorph.extend, LocalEquiv.coe_trans, - ModelWithCorners.toLocalEquiv_coe, PartialHomeomorph.coe_coe, modelWithCornersSelf_coe, + simp_rw [Cont, ContDiffWithinAtProp, extChartAt, PartialHomeomorph.extend, PartialEquiv.coe_trans, + ModelWithCorners.toPartialEquiv_coe, PartialHomeomorph.coe_coe, modelWithCornersSelf_coe, chartAt_self_eq, PartialHomeomorph.refl_apply, comp.left_id] #align cont_mdiff_within_at_iff_target contMDiffWithinAt_iff_target -/ @@ -671,8 +671,8 @@ theorem contMDiffOn_iff_target : by inhabit E' simp only [contMDiffOn_iff, ModelWithCorners.source_eq, chartAt_self_eq, - PartialHomeomorph.refl_localEquiv, LocalEquiv.refl_trans, extChartAt, PartialHomeomorph.extend, - Set.preimage_univ, Set.inter_univ, and_congr_right_iff] + PartialHomeomorph.refl_localEquiv, PartialEquiv.refl_trans, extChartAt, + PartialHomeomorph.extend, Set.preimage_univ, Set.inter_univ, and_congr_right_iff] intro h constructor · refine' fun h' y => ⟨_, fun x _ => h' x y⟩ @@ -1474,7 +1474,7 @@ theorem contMDiffOn_extend_symm (he : e ∈ maximalAtlas I M) : by have h2 := contMDiffOn_symm_of_mem_maximalAtlas he refine' h2.comp (cont_mdiff_on_model_symm.mono <| image_subset_range _ _) _ - simp_rw [image_subset_iff, LocalEquiv.restr_coe_symm, I.to_local_equiv_coe_symm, + simp_rw [image_subset_iff, PartialEquiv.restr_coe_symm, I.to_local_equiv_coe_symm, preimage_preimage, I.left_inv, preimage_id'] #align cont_mdiff_on_extend_symm contMDiffOn_extend_symm -/ @@ -2269,7 +2269,7 @@ theorem contMDiffWithinAt_pi_space : ∀ i, ContMDiffWithinAt I 𝓘(𝕜, Fi i) n (fun x => φ x i) s x := by simp only [contMDiffWithinAt_iff, continuousWithinAt_pi, contDiffWithinAt_pi, forall_and, - writtenInExtChartAt, extChartAt_model_space_eq_id, (· ∘ ·), LocalEquiv.refl_coe, id] + writtenInExtChartAt, extChartAt_model_space_eq_id, (· ∘ ·), PartialEquiv.refl_coe, id] #align cont_mdiff_within_at_pi_space contMDiffWithinAt_pi_space -/ diff --git a/Mathbin/Geometry/Manifold/ContMdiffMfderiv.lean b/Mathbin/Geometry/Manifold/ContMdiffMfderiv.lean index 9b283d783b..e626610d83 100644 --- a/Mathbin/Geometry/Manifold/ContMdiffMfderiv.lean +++ b/Mathbin/Geometry/Manifold/ContMdiffMfderiv.lean @@ -175,7 +175,7 @@ theorem ContMDiffAt.mfderiv {x₀ : N} (f : N → M → M') (g : N → M) (range J) (extChartAt J x₀ x₀) := by rw [contMDiffAt_iff] at hf hg - simp_rw [Function.comp, uncurry, extChartAt_prod, LocalEquiv.prod_coe_symm, + simp_rw [Function.comp, uncurry, extChartAt_prod, PartialEquiv.prod_coe_symm, ModelWithCorners.range_prod] at hf ⊢ refine' ContDiffWithinAt.fderivWithin _ hg.2 I.unique_diff hmn (mem_range_self _) _ · simp_rw [extChartAt_to_inv]; exact hf.2 @@ -245,12 +245,12 @@ theorem ContMDiffAt.mfderiv {x₀ : N} (f : N → M → M') (g : N → M) rw [(h2x₂.mdifferentiable_at le_rfl).mfderiv] have hI := (contDiffWithinAt_ext_coord_change I (g x₂) (g x₀) <| - LocalEquiv.mem_symm_trans_source _ hx₂ <| + PartialEquiv.mem_symm_trans_source _ hx₂ <| mem_extChartAt_source I (g x₂)).DifferentiableWithinAt le_top have hI' := (contDiffWithinAt_ext_coord_change I' (f x₀ (g x₀)) (f x₂ (g x₂)) <| - LocalEquiv.mem_symm_trans_source _ (mem_extChartAt_source I' (f x₂ (g x₂))) + PartialEquiv.mem_symm_trans_source _ (mem_extChartAt_source I' (f x₂ (g x₂))) h3x₂).DifferentiableWithinAt le_top have h3f := (h2x₂.mdifferentiable_at le_rfl).2 diff --git a/Mathbin/Geometry/Manifold/Diffeomorph.lean b/Mathbin/Geometry/Manifold/Diffeomorph.lean index ba18775de1..52f1109b10 100644 --- a/Mathbin/Geometry/Manifold/Diffeomorph.lean +++ b/Mathbin/Geometry/Manifold/Diffeomorph.lean @@ -645,7 +645,7 @@ variable (I) (e : E ≃ₘ[𝕜] E') /-- Apply a diffeomorphism (e.g., a continuous linear equivalence) to the model vector space. -/ def transDiffeomorph (I : ModelWithCorners 𝕜 E H) (e : E ≃ₘ[𝕜] E') : ModelWithCorners 𝕜 E' H where - toLocalEquiv := I.toLocalEquiv.trans e.toEquiv.toLocalEquiv + toPartialEquiv := I.toPartialEquiv.trans e.toEquiv.toPartialEquiv source_eq := by simp unique_diff' := by simp [range_comp e, I.unique_diff] continuous_toFun := e.Continuous.comp I.Continuous diff --git a/Mathbin/Geometry/Manifold/Instances/Sphere.lean b/Mathbin/Geometry/Manifold/Instances/Sphere.lean index 5871cb0ad5..80024f7b3a 100644 --- a/Mathbin/Geometry/Manifold/Instances/Sphere.lean +++ b/Mathbin/Geometry/Manifold/Instances/Sphere.lean @@ -508,8 +508,8 @@ instance {n : ℕ} [Fact (finrank ℝ E = n + 1)] : (cont_diff_stereo_inv_fun_aux.comp (ℝ ∙ (v : E))ᗮ.subtypeL.ContDiff).comp U.symm.cont_diff convert H₁.comp' (H₂.cont_diff_on : ContDiffOn ℝ ⊤ _ Set.univ) using 1 -- squeezed from `ext, simp [sphere_ext_iff, stereographic'_symm_apply, real_inner_comm]` - simp only [PartialHomeomorph.trans_toLocalEquiv, PartialHomeomorph.symm_toLocalEquiv, - LocalEquiv.trans_source, LocalEquiv.symm_source, stereographic'_target, + simp only [PartialHomeomorph.trans_toPartialEquiv, PartialHomeomorph.symm_toPartialEquiv, + PartialEquiv.trans_source, PartialEquiv.symm_source, stereographic'_target, stereographic'_source] simp only [modelWithCornersSelf_coe, modelWithCornersSelf_coe_symm, Set.preimage_id, Set.range_id, Set.inter_univ, Set.univ_inter, Set.compl_singleton_eq, Set.preimage_setOf_eq] diff --git a/Mathbin/Geometry/Manifold/SmoothManifoldWithCorners.lean b/Mathbin/Geometry/Manifold/SmoothManifoldWithCorners.lean index 2588a07ed5..375e1c53b2 100644 --- a/Mathbin/Geometry/Manifold/SmoothManifoldWithCorners.lean +++ b/Mathbin/Geometry/Manifold/SmoothManifoldWithCorners.lean @@ -136,7 +136,7 @@ define a smooth manifold with model space `H`, and model vector space `E`. @[ext, nolint has_nonempty_instance] structure ModelWithCorners (𝕜 : Type _) [NontriviallyNormedField 𝕜] (E : Type _) [NormedAddCommGroup E] [NormedSpace 𝕜 E] (H : Type _) [TopologicalSpace H] extends - LocalEquiv H E where + PartialEquiv H E where source_eq : source = univ unique_diff' : UniqueDiffOn 𝕜 to_local_equiv.target continuous_toFun : Continuous to_fun := by continuity @@ -151,7 +151,7 @@ attribute [simp, mfld_simps] ModelWithCorners.source_eq def modelWithCornersSelf (𝕜 : Type _) [NontriviallyNormedField 𝕜] (E : Type _) [NormedAddCommGroup E] [NormedSpace 𝕜 E] : ModelWithCorners 𝕜 E E where - toLocalEquiv := LocalEquiv.refl E + toPartialEquiv := PartialEquiv.refl E source_eq := rfl unique_diff' := uniqueDiffOn_univ continuous_toFun := continuous_id @@ -175,8 +175,8 @@ instance : CoeFun (ModelWithCorners 𝕜 E H) fun _ => H → E := #print ModelWithCorners.symm /- /-- The inverse to a model with corners, only registered as a local equiv. -/ -protected def symm : LocalEquiv E H := - I.toLocalEquiv.symm +protected def symm : PartialEquiv E H := + I.toPartialEquiv.symm #align model_with_corners.symm ModelWithCorners.symm -/ @@ -198,35 +198,35 @@ def Simps.symm_apply (𝕜 : Type _) [NontriviallyNormedField 𝕜] (E : Type _) -/ initialize_simps_projections ModelWithCorners (to_local_equiv_to_fun → apply, - to_local_equiv_inv_fun → symm_apply, toLocalEquiv_source → source, toLocalEquiv_target → target, - -toLocalEquiv) + to_local_equiv_inv_fun → symm_apply, toPartialEquiv_source → source, toPartialEquiv_target → + target, -toPartialEquiv) -#print ModelWithCorners.toLocalEquiv_coe /- +#print ModelWithCorners.toPartialEquiv_coe /- -- Register a few lemmas to make sure that `simp` puts expressions in normal form @[simp, mfld_simps] -theorem toLocalEquiv_coe : (I.toLocalEquiv : H → E) = I := +theorem toPartialEquiv_coe : (I.toPartialEquiv : H → E) = I := rfl -#align model_with_corners.to_local_equiv_coe ModelWithCorners.toLocalEquiv_coe +#align model_with_corners.to_local_equiv_coe ModelWithCorners.toPartialEquiv_coe -/ #print ModelWithCorners.mk_coe /- @[simp, mfld_simps] -theorem mk_coe (e : LocalEquiv H E) (a b c d) : +theorem mk_coe (e : PartialEquiv H E) (a b c d) : ((ModelWithCorners.mk e a b c d : ModelWithCorners 𝕜 E H) : H → E) = (e : H → E) := rfl #align model_with_corners.mk_coe ModelWithCorners.mk_coe -/ -#print ModelWithCorners.toLocalEquiv_coe_symm /- +#print ModelWithCorners.toPartialEquiv_coe_symm /- @[simp, mfld_simps] -theorem toLocalEquiv_coe_symm : (I.toLocalEquiv.symm : E → H) = I.symm := +theorem toPartialEquiv_coe_symm : (I.toPartialEquiv.symm : E → H) = I.symm := rfl -#align model_with_corners.to_local_equiv_coe_symm ModelWithCorners.toLocalEquiv_coe_symm +#align model_with_corners.to_local_equiv_coe_symm ModelWithCorners.toPartialEquiv_coe_symm -/ #print ModelWithCorners.mk_symm /- @[simp, mfld_simps] -theorem mk_symm (e : LocalEquiv H E) (a b c d) : +theorem mk_symm (e : PartialEquiv H E) (a b c d) : (ModelWithCorners.mk e a b c d : ModelWithCorners 𝕜 E H).symm = e.symm := rfl #align model_with_corners.mk_symm ModelWithCorners.mk_symm @@ -453,7 +453,7 @@ variable (𝕜 E) #print modelWithCornersSelf_localEquiv /- /-- In the trivial model with corners, the associated local equiv is the identity. -/ @[simp, mfld_simps] -theorem modelWithCornersSelf_localEquiv : 𝓘(𝕜, E).toLocalEquiv = LocalEquiv.refl E := +theorem modelWithCornersSelf_localEquiv : 𝓘(𝕜, E).toPartialEquiv = PartialEquiv.refl E := rfl #align model_with_corners_self_local_equiv modelWithCornersSelf_localEquiv -/ @@ -491,8 +491,8 @@ def ModelWithCorners.prod {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Ty {H' : Type w'} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') : ModelWithCorners 𝕜 (E × E') (ModelProd H H') := { - I.toLocalEquiv.Prod - I'.toLocalEquiv with + I.toPartialEquiv.Prod + I'.toPartialEquiv with toFun := fun x => (I x.1, I' x.2) invFun := fun x => (I.symm x.1, I'.symm x.2) source := {x | x.1 ∈ I.source ∧ x.2 ∈ I'.source} @@ -512,7 +512,7 @@ def ModelWithCorners.pi {𝕜 : Type u} [NontriviallyNormedField 𝕜] {ι : Typ [∀ i, TopologicalSpace (H i)] (I : ∀ i, ModelWithCorners 𝕜 (E i) (H i)) : ModelWithCorners 𝕜 (∀ i, E i) (ModelPi H) where - toLocalEquiv := LocalEquiv.pi fun i => (I i).toLocalEquiv + toPartialEquiv := PartialEquiv.pi fun i => (I i).toPartialEquiv source_eq := by simp only [Set.pi_univ, mfld_simps] unique_diff' := UniqueDiffOn.pi ι E _ _ fun i _ => (I i).unique_diff' continuous_toFun := continuous_pi fun i => (I i).Continuous.comp (continuous_apply i) @@ -538,12 +538,12 @@ variable {𝕜 : Type _} [NontriviallyNormedField 𝕜] {E : Type _} [NormedAddC [TopologicalSpace G] {G' : Type _} [TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} -#print modelWithCorners_prod_toLocalEquiv /- +#print modelWithCorners_prod_toPartialEquiv /- @[simp, mfld_simps] -theorem modelWithCorners_prod_toLocalEquiv : - (I.Prod J).toLocalEquiv = I.toLocalEquiv.Prod J.toLocalEquiv := +theorem modelWithCorners_prod_toPartialEquiv : + (I.Prod J).toPartialEquiv = I.toPartialEquiv.Prod J.toPartialEquiv := rfl -#align model_with_corners_prod_to_local_equiv modelWithCorners_prod_toLocalEquiv +#align model_with_corners_prod_to_local_equiv modelWithCorners_prod_toPartialEquiv -/ #print modelWithCorners_prod_coe /- @@ -743,7 +743,7 @@ theorem contDiffGroupoid_prod {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCor cases' he with he he_symm cases' he' with he' he'_symm simp only at he he_symm he' he'_symm - constructor <;> simp only [LocalEquiv.prod_source, PartialHomeomorph.prod_toLocalEquiv] + constructor <;> simp only [PartialEquiv.prod_source, PartialHomeomorph.prod_toLocalEquiv] · have h3 := ContDiffOn.prod_map he he' rw [← I.image_eq, ← I'.image_eq, Set.prod_image_image_eq] at h3 rw [← (I.prod I').image_eq] @@ -940,8 +940,8 @@ namespace PartialHomeomorph /-- Given a chart `f` on a manifold with corners, `f.extend I` is the extended chart to the model vector space. -/ @[simp, mfld_simps] -def extend : LocalEquiv M E := - f.toLocalEquiv ≫ I.toLocalEquiv +def extend : PartialEquiv M E := + f.toPartialEquiv ≫ I.toPartialEquiv #align local_homeomorph.extend PartialHomeomorph.extend -/ @@ -959,7 +959,7 @@ theorem extend_coe_symm : ⇑(f.extend I).symm = f.symm ∘ I.symm := #print PartialHomeomorph.extend_source /- theorem extend_source : (f.extend I).source = f.source := by - rw [extend, LocalEquiv.trans_source, I.source_eq, preimage_univ, inter_univ] + rw [extend, PartialEquiv.trans_source, I.source_eq, preimage_univ, inter_univ] #align local_homeomorph.extend_source PartialHomeomorph.extend_source -/ @@ -971,7 +971,7 @@ theorem isOpen_extend_source : IsOpen (f.extend I).source := by rw [extend_sourc #print PartialHomeomorph.extend_target /- theorem extend_target : (f.extend I).target = I.symm ⁻¹' f.target ∩ range I := by - simp_rw [extend, LocalEquiv.trans_target, I.target_eq, I.to_local_equiv_coe_symm, inter_comm] + simp_rw [extend, PartialEquiv.trans_target, I.target_eq, I.to_local_equiv_coe_symm, inter_comm] #align local_homeomorph.extend_target PartialHomeomorph.extend_target -/ @@ -1029,7 +1029,7 @@ theorem map_extend_nhds {x : M} (hy : x ∈ f.source) : theorem extend_target_mem_nhdsWithin {y : M} (hy : y ∈ f.source) : (f.extend I).target ∈ 𝓝[range I] f.extend I y := by - rw [← LocalEquiv.image_source_eq_target, ← map_extend_nhds f I hy] + rw [← PartialEquiv.image_source_eq_target, ← map_extend_nhds f I hy] exact image_mem_map (extend_source_mem_nhds _ _ hy) #align local_homeomorph.extend_target_mem_nhds_within PartialHomeomorph.extend_target_mem_nhdsWithin -/ @@ -1192,7 +1192,7 @@ theorem extend_symm_preimage_inter_range_eventuallyEq {s : Set M} {x : M} (hs : theorem extend_coord_change_source : ((f.extend I).symm ≫ f'.extend I).source = I '' (f.symm ≫ₕ f').source := by - simp_rw [LocalEquiv.trans_source, I.image_eq, extend_source, LocalEquiv.symm_source, + simp_rw [PartialEquiv.trans_source, I.image_eq, extend_source, PartialEquiv.symm_source, extend_target, inter_right_comm _ (range I)] rfl #align local_homeomorph.extend_coord_change_source PartialHomeomorph.extend_coord_change_source @@ -1275,7 +1275,7 @@ variable [ChartedSpace H M] [ChartedSpace H' M'] /-- The preferred extended chart on a manifold with corners around a point `x`, from a neighborhood of `x` to the model vector space. -/ @[simp, mfld_simps] -def extChartAt (x : M) : LocalEquiv M E := +def extChartAt (x : M) : PartialEquiv M E := (chartAt H x).extend I #align ext_chart_at extChartAt -/ @@ -1624,7 +1624,7 @@ theorem extChartAt_self_apply {x y : H} : extChartAt I x y = I y := #print extChartAt_model_space_eq_id /- /-- In the case of the manifold structure on a vector space, the extended charts are just the identity.-/ -theorem extChartAt_model_space_eq_id (x : E) : extChartAt 𝓘(𝕜, E) x = LocalEquiv.refl E := by +theorem extChartAt_model_space_eq_id (x : E) : extChartAt 𝓘(𝕜, E) x = PartialEquiv.refl E := by simp only [mfld_simps] #align ext_chart_at_model_space_eq_id extChartAt_model_space_eq_id -/ diff --git a/Mathbin/Geometry/Manifold/VectorBundle/Basic.lean b/Mathbin/Geometry/Manifold/VectorBundle/Basic.lean index b2e0861b2e..7327ba32b0 100644 --- a/Mathbin/Geometry/Manifold/VectorBundle/Basic.lean +++ b/Mathbin/Geometry/Manifold/VectorBundle/Basic.lean @@ -148,11 +148,11 @@ variable [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] #print FiberBundle.extChartAt /- protected theorem FiberBundle.extChartAt (x : TotalSpace F E) : extChartAt (IB.Prod 𝓘(𝕜, F)) x = - (trivializationAt F E x.proj).toLocalEquiv ≫ - (extChartAt IB x.proj).Prod (LocalEquiv.refl F) := + (trivializationAt F E x.proj).toPartialEquiv ≫ + (extChartAt IB x.proj).Prod (PartialEquiv.refl F) := by simp_rw [extChartAt, FiberBundle.chartedSpace_chartAt, extend] - simp only [LocalEquiv.trans_assoc, mfld_simps] + simp only [PartialEquiv.trans_assoc, mfld_simps] #align fiber_bundle.ext_chart_at FiberBundle.extChartAt -/ @@ -177,9 +177,9 @@ theorem contMDiffWithinAt_totalSpace (f : M → TotalSpace F E) {s : Set M} {x simp (config := { singlePass := true }) only [contMDiffWithinAt_iff_target] rw [and_and_and_comm, ← continuous_within_at_total_space, and_congr_right_iff] intro hf - simp_rw [modelWithCornersSelf_prod, FiberBundle.extChartAt, Function.comp, LocalEquiv.trans_apply, - LocalEquiv.prod_coe, LocalEquiv.refl_coe, extChartAt_self_apply, modelWithCornersSelf_coe, - id_def] + simp_rw [modelWithCornersSelf_prod, FiberBundle.extChartAt, Function.comp, + PartialEquiv.trans_apply, PartialEquiv.prod_coe, PartialEquiv.refl_coe, extChartAt_self_apply, + modelWithCornersSelf_coe, id_def] refine' (contMDiffWithinAt_prod_iff _).trans _ -- rw doesn't do this? have h1 : (fun x => (f x).proj) ⁻¹' (trivialization_at F E (f x₀).proj).baseSet ∈ 𝓝[s] x₀ := diff --git a/Mathbin/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean b/Mathbin/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean index 5df3011be5..81913a90c6 100644 --- a/Mathbin/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean +++ b/Mathbin/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean @@ -321,10 +321,10 @@ def smoothFiberwiseLinear : StructureGroupoid (B × F) · apply contMDiffOn_const · simp only [FiberwiseLinear.localHomeomorph, PartialHomeomorph.refl_localEquiv, - LocalEquiv.refl_source, univ_prod_univ] + PartialEquiv.refl_source, univ_prod_univ] · simp only [FiberwiseLinear.localHomeomorph, PartialHomeomorph.refl_apply, Prod.mk.eta, id.def, - ContinuousLinearEquiv.coe_refl', PartialHomeomorph.mk_coe, LocalEquiv.coe_mk] + ContinuousLinearEquiv.coe_refl', PartialHomeomorph.mk_coe, PartialEquiv.coe_mk] locality' := by -- the hard work has been extracted to `locality_aux₁` and `locality_aux₂` diff --git a/Mathbin/Geometry/Manifold/VectorBundle/Tangent.lean b/Mathbin/Geometry/Manifold/VectorBundle/Tangent.lean index d6d98335d2..5f357984df 100644 --- a/Mathbin/Geometry/Manifold/VectorBundle/Tangent.lean +++ b/Mathbin/Geometry/Manifold/VectorBundle/Tangent.lean @@ -204,13 +204,13 @@ protected theorem chartAt (p : TM) : #align tangent_bundle.chart_at TangentBundle.chartAt -/ -#print TangentBundle.chartAt_toLocalEquiv /- -theorem chartAt_toLocalEquiv (p : TM) : - (chartAt (ModelProd H E) p).toLocalEquiv = - (tangentBundleCore I M).toFiberBundleCore.localTrivAsLocalEquiv (achart H p.1) ≫ - (chartAt H p.1).toLocalEquiv.Prod (LocalEquiv.refl E) := +#print TangentBundle.chartAt_toPartialEquiv /- +theorem chartAt_toPartialEquiv (p : TM) : + (chartAt (ModelProd H E) p).toPartialEquiv = + (tangentBundleCore I M).toFiberBundleCore.localTrivAsPartialEquiv (achart H p.1) ≫ + (chartAt H p.1).toPartialEquiv.Prod (PartialEquiv.refl E) := rfl -#align tangent_bundle.chart_at_to_local_equiv TangentBundle.chartAt_toLocalEquiv +#align tangent_bundle.chart_at_to_local_equiv TangentBundle.chartAt_toPartialEquiv -/ #print TangentBundle.trivializationAt_eq_localTriv /- @@ -354,7 +354,7 @@ instance tangentBundleCore.isSmooth : (tangentBundleCore I M).IsSmooth I := rw [SmoothOn, contMDiffOn_iff_source_of_mem_maximalAtlas (subset_maximal_atlas I i.2), contMDiffOn_iff_contDiffOn] refine' ((contDiffOn_fderiv_coord_change I i j).congr fun x hx => _).mono _ - · rw [LocalEquiv.trans_source'] at hx + · rw [PartialEquiv.trans_source'] at hx simp_rw [Function.comp_apply, tangentBundleCore_coordChange, (i.1.extend I).right_inv hx.1] · exact (i.1.extend_image_source_inter j.1 I).Subset · apply inter_subset_left @@ -377,15 +377,16 @@ end TangentBundleInstances between a product type and a sigma type, a.k.a. `equiv.sigma_equiv_prod`. -/ @[simp, mfld_simps] theorem tangentBundle_model_space_chartAt (p : TangentBundle I H) : - (chartAt (ModelProd H E) p).toLocalEquiv = (TotalSpace.toProd H E).toLocalEquiv := + (chartAt (ModelProd H E) p).toPartialEquiv = (TotalSpace.toProd H E).toPartialEquiv := by ext x : 1 · ext; · rfl exact (tangentBundleCore I H).coordChange_self (achart _ x.1) x.1 (mem_achart_source H x.1) x.2 · intro x; ext; · rfl; apply hEq_of_eq exact (tangentBundleCore I H).coordChange_self (achart _ x.1) x.1 (mem_achart_source H x.1) x.2 - simp_rw [TangentBundle.chartAt, FiberBundleCore.localTriv, FiberBundleCore.localTrivAsLocalEquiv, - VectorBundleCore.toFiberBundleCore_baseSet, tangentBundleCore_baseSet] + simp_rw [TangentBundle.chartAt, FiberBundleCore.localTriv, + FiberBundleCore.localTrivAsPartialEquiv, VectorBundleCore.toFiberBundleCore_baseSet, + tangentBundleCore_baseSet] simp only [mfld_simps] #align tangent_bundle_model_space_chart_at tangentBundle_model_space_chartAt -/ @@ -405,7 +406,7 @@ theorem tangentBundle_model_space_coe_chartAt_symm (p : TangentBundle I H) : (TotalSpace.toProd H E).symm := by unfold_coes - simp_rw [PartialHomeomorph.symm_toLocalEquiv, tangentBundle_model_space_chartAt]; rfl + simp_rw [PartialHomeomorph.symm_toPartialEquiv, tangentBundle_model_space_chartAt]; rfl #align tangent_bundle_model_space_coe_chart_at_symm tangentBundle_model_space_coe_chartAt_symm -/ diff --git a/Mathbin/LinearAlgebra/AffineSpace/Combination.lean b/Mathbin/LinearAlgebra/AffineSpace/Combination.lean index 80ea59e39c..22b0bd1b23 100644 --- a/Mathbin/LinearAlgebra/AffineSpace/Combination.lean +++ b/Mathbin/LinearAlgebra/AffineSpace/Combination.lean @@ -196,7 +196,8 @@ theorem weightedVSubOfPoint_indicator_subset (w : ι → k) (p : ι → P) (b : by rw [weighted_vsub_of_point_apply, weighted_vsub_of_point_apply] exact - Set.sum_indicator_subset_of_eq_zero w (fun i wi => wi • (p i -ᵥ b : V)) h fun i => zero_smul k _ + Finset.sum_indicator_subset_of_eq_zero w (fun i wi => wi • (p i -ᵥ b : V)) h fun i => + zero_smul k _ #align finset.weighted_vsub_of_point_indicator_subset Finset.weightedVSubOfPoint_indicator_subset -/ @@ -1113,7 +1114,7 @@ theorem centroidWeightsIndicator_def : /-- The sum of the weights for the centroid indexed by a `fintype`. -/ theorem sum_centroidWeightsIndicator [Fintype ι] : ∑ i, s.centroidWeightsIndicator k i = ∑ i in s, s.centroidWeights k i := - (Set.sum_indicator_subset _ (subset_univ _)).symm + (Finset.sum_indicator_subset _ (subset_univ _)).symm #align finset.sum_centroid_weights_indicator Finset.sum_centroidWeightsIndicator -/ @@ -1337,7 +1338,7 @@ theorem eq_affineCombination_of_mem_affineSpan {p1 : P} {p : ι → P} let s' := insert i0 s let w' := Set.indicator (↑s) w have h' : ∑ i in s', w' i = 0 := by - rw [← h, Set.sum_indicator_subset _ (Finset.subset_insert i0 s)] + rw [← h, Finset.sum_indicator_subset _ (Finset.subset_insert i0 s)] have hs' : s'.weighted_vsub p w' = p1 -ᵥ p i0 := by rw [hs] diff --git a/Mathbin/LinearAlgebra/AffineSpace/Independent.lean b/Mathbin/LinearAlgebra/AffineSpace/Independent.lean index 11abdb9a2d..ee4185b362 100644 --- a/Mathbin/LinearAlgebra/AffineSpace/Independent.lean +++ b/Mathbin/LinearAlgebra/AffineSpace/Independent.lean @@ -88,7 +88,7 @@ theorem affineIndependent_iff_of_fintype [Fintype ι] (p : ι → P) : · exact fun h w hw hs i => h Finset.univ w hw hs i (Finset.mem_univ _) · intro h s w hw hs i hi rw [Finset.weightedVSub_indicator_subset _ _ (Finset.subset_univ s)] at hs - rw [Set.sum_indicator_subset _ (Finset.subset_univ s)] at hw + rw [Finset.sum_indicator_subset _ (Finset.subset_univ s)] at hw replace h := h ((↑s : Set ι).indicator w) hw hs i simpa [hi] using h #align affine_independent_iff_of_fintype affineIndependent_iff_of_fintype @@ -219,8 +219,8 @@ theorem affineIndependent_iff_indicator_eq_of_affineCombination_eq (p : ι → P ext i by_cases hi : i ∈ s1 ∪ s2 · rw [← sub_eq_zero] - rw [Set.sum_indicator_subset _ (Finset.subset_union_left s1 s2)] at hw1 - rw [Set.sum_indicator_subset _ (Finset.subset_union_right s1 s2)] at hw2 + rw [Finset.sum_indicator_subset _ (Finset.subset_union_left s1 s2)] at hw1 + rw [Finset.sum_indicator_subset _ (Finset.subset_union_right s1 s2)] at hw2 have hws : ∑ i in s1 ∪ s2, (Set.indicator (↑s1) w1 - Set.indicator (↑s2) w2) i = 0 := by simp [hw1, hw2] rw [Finset.affineCombination_indicator_subset _ _ (Finset.subset_union_left s1 s2), @@ -264,9 +264,9 @@ theorem affineIndependent_iff_eq_of_fintype_affineCombination_eq [Fintype ι] (p simpa only [Set.indicator_univ, Finset.coe_univ] using h _ _ w1 w2 hw1 hw2 hweq · intro h s1 s2 w1 w2 hw1 hw2 hweq have hw1' : ∑ i, (s1 : Set ι).indicator w1 i = 1 := by - rwa [Set.sum_indicator_subset _ (Finset.subset_univ s1)] at hw1 + rwa [Finset.sum_indicator_subset _ (Finset.subset_univ s1)] at hw1 have hw2' : ∑ i, (s2 : Set ι).indicator w2 i = 1 := by - rwa [Set.sum_indicator_subset _ (Finset.subset_univ s2)] at hw2 + rwa [Finset.sum_indicator_subset _ (Finset.subset_univ s2)] at hw2 rw [Finset.affineCombination_indicator_subset w1 p (Finset.subset_univ s1), Finset.affineCombination_indicator_subset w2 p (Finset.subset_univ s2)] at hweq exact h _ _ hw1' hw2' hweq diff --git a/Mathbin/Logic/Equiv/LocalEquiv.lean b/Mathbin/Logic/Equiv/LocalEquiv.lean index 4342bb10c2..074a8040f7 100644 --- a/Mathbin/Logic/Equiv/LocalEquiv.lean +++ b/Mathbin/Logic/Equiv/LocalEquiv.lean @@ -109,12 +109,12 @@ open Function Set variable {α : Type _} {β : Type _} {γ : Type _} {δ : Type _} -#print LocalEquiv /- +#print PartialEquiv /- /-- Local equivalence between subsets `source` and `target` of α and β respectively. The (global) maps `to_fun : α → β` and `inv_fun : β → α` map `source` to `target` and conversely, and are inverse to each other there. The values of `to_fun` outside of `source` and of `inv_fun` outside of `target` are irrelevant. -/ -structure LocalEquiv (α : Type _) (β : Type _) where +structure PartialEquiv (α : Type _) (β : Type _) where toFun : α → β invFun : β → α source : Set α @@ -123,20 +123,20 @@ structure LocalEquiv (α : Type _) (β : Type _) where map_target' : ∀ ⦃x⦄, x ∈ target → inv_fun x ∈ source left_inv' : ∀ ⦃x⦄, x ∈ source → inv_fun (to_fun x) = x right_inv' : ∀ ⦃x⦄, x ∈ target → to_fun (inv_fun x) = x -#align local_equiv LocalEquiv +#align local_equiv PartialEquiv -/ -namespace LocalEquiv +namespace PartialEquiv -variable (e : LocalEquiv α β) (e' : LocalEquiv β γ) +variable (e : PartialEquiv α β) (e' : PartialEquiv β γ) -instance [Inhabited α] [Inhabited β] : Inhabited (LocalEquiv α β) := +instance [Inhabited α] [Inhabited β] : Inhabited (PartialEquiv α β) := ⟨⟨const α default, const β default, ∅, ∅, mapsTo_empty _ _, mapsTo_empty _ _, eqOn_empty _ _, eqOn_empty _ _⟩⟩ -#print LocalEquiv.symm /- +#print PartialEquiv.symm /- /-- The inverse of a local equiv -/ -protected def symm : LocalEquiv β α where +protected def symm : PartialEquiv β α where toFun := e.invFun invFun := e.toFun source := e.target @@ -145,130 +145,131 @@ protected def symm : LocalEquiv β α where map_target' := e.map_source' left_inv' := e.right_inv' right_inv' := e.left_inv' -#align local_equiv.symm LocalEquiv.symm +#align local_equiv.symm PartialEquiv.symm -/ -instance : CoeFun (LocalEquiv α β) fun _ => α → β := - ⟨LocalEquiv.toFun⟩ +instance : CoeFun (PartialEquiv α β) fun _ => α → β := + ⟨PartialEquiv.toFun⟩ -#print LocalEquiv.Simps.symm_apply /- +#print PartialEquiv.Simps.symm_apply /- /-- See Note [custom simps projection] -/ -def Simps.symm_apply (e : LocalEquiv α β) : β → α := +def Simps.symm_apply (e : PartialEquiv α β) : β → α := e.symm -#align local_equiv.simps.symm_apply LocalEquiv.Simps.symm_apply +#align local_equiv.simps.symm_apply PartialEquiv.Simps.symm_apply -/ -initialize_simps_projections LocalEquiv (toFun → apply, invFun → symm_apply) +initialize_simps_projections PartialEquiv (toFun → apply, invFun → symm_apply) @[simp, mfld_simps] -theorem coe_mk (f : α → β) (g s t ml mr il ir) : (LocalEquiv.mk f g s t ml mr il ir : α → β) = f := +theorem coe_mk (f : α → β) (g s t ml mr il ir) : + (PartialEquiv.mk f g s t ml mr il ir : α → β) = f := rfl -#align local_equiv.coe_mk LocalEquiv.coe_mk +#align local_equiv.coe_mk PartialEquiv.coe_mk -#print LocalEquiv.coe_symm_mk /- +#print PartialEquiv.coe_symm_mk /- @[simp, mfld_simps] theorem coe_symm_mk (f : α → β) (g s t ml mr il ir) : - ((LocalEquiv.mk f g s t ml mr il ir).symm : β → α) = g := + ((PartialEquiv.mk f g s t ml mr il ir).symm : β → α) = g := rfl -#align local_equiv.coe_symm_mk LocalEquiv.coe_symm_mk +#align local_equiv.coe_symm_mk PartialEquiv.coe_symm_mk -/ @[simp, mfld_simps] theorem toFun_as_coe : e.toFun = e := rfl -#align local_equiv.to_fun_as_coe LocalEquiv.toFun_as_coe +#align local_equiv.to_fun_as_coe PartialEquiv.toFun_as_coe -#print LocalEquiv.invFun_as_coe /- +#print PartialEquiv.invFun_as_coe /- @[simp, mfld_simps] theorem invFun_as_coe : e.invFun = e.symm := rfl -#align local_equiv.inv_fun_as_coe LocalEquiv.invFun_as_coe +#align local_equiv.inv_fun_as_coe PartialEquiv.invFun_as_coe -/ -#print LocalEquiv.map_source /- +#print PartialEquiv.map_source /- @[simp, mfld_simps] theorem map_source {x : α} (h : x ∈ e.source) : e x ∈ e.target := e.map_source' h -#align local_equiv.map_source LocalEquiv.map_source +#align local_equiv.map_source PartialEquiv.map_source -/ -#print LocalEquiv.map_target /- +#print PartialEquiv.map_target /- @[simp, mfld_simps] theorem map_target {x : β} (h : x ∈ e.target) : e.symm x ∈ e.source := e.map_target' h -#align local_equiv.map_target LocalEquiv.map_target +#align local_equiv.map_target PartialEquiv.map_target -/ -#print LocalEquiv.left_inv /- +#print PartialEquiv.left_inv /- @[simp, mfld_simps] theorem left_inv {x : α} (h : x ∈ e.source) : e.symm (e x) = x := e.left_inv' h -#align local_equiv.left_inv LocalEquiv.left_inv +#align local_equiv.left_inv PartialEquiv.left_inv -/ -#print LocalEquiv.right_inv /- +#print PartialEquiv.right_inv /- @[simp, mfld_simps] theorem right_inv {x : β} (h : x ∈ e.target) : e (e.symm x) = x := e.right_inv' h -#align local_equiv.right_inv LocalEquiv.right_inv +#align local_equiv.right_inv PartialEquiv.right_inv -/ -#print LocalEquiv.eq_symm_apply /- +#print PartialEquiv.eq_symm_apply /- theorem eq_symm_apply {x : α} {y : β} (hx : x ∈ e.source) (hy : y ∈ e.target) : x = e.symm y ↔ e x = y := ⟨fun h => by rw [← e.right_inv hy, h], fun h => by rw [← e.left_inv hx, h]⟩ -#align local_equiv.eq_symm_apply LocalEquiv.eq_symm_apply +#align local_equiv.eq_symm_apply PartialEquiv.eq_symm_apply -/ -#print LocalEquiv.mapsTo /- +#print PartialEquiv.mapsTo /- protected theorem mapsTo : MapsTo e e.source e.target := fun x => e.map_source -#align local_equiv.maps_to LocalEquiv.mapsTo +#align local_equiv.maps_to PartialEquiv.mapsTo -/ -#print LocalEquiv.symm_mapsTo /- +#print PartialEquiv.symm_mapsTo /- theorem symm_mapsTo : MapsTo e.symm e.target e.source := e.symm.MapsTo -#align local_equiv.symm_maps_to LocalEquiv.symm_mapsTo +#align local_equiv.symm_maps_to PartialEquiv.symm_mapsTo -/ -#print LocalEquiv.leftInvOn /- +#print PartialEquiv.leftInvOn /- protected theorem leftInvOn : LeftInvOn e.symm e e.source := fun x => e.left_inv -#align local_equiv.left_inv_on LocalEquiv.leftInvOn +#align local_equiv.left_inv_on PartialEquiv.leftInvOn -/ -#print LocalEquiv.rightInvOn /- +#print PartialEquiv.rightInvOn /- protected theorem rightInvOn : RightInvOn e.symm e e.target := fun x => e.right_inv -#align local_equiv.right_inv_on LocalEquiv.rightInvOn +#align local_equiv.right_inv_on PartialEquiv.rightInvOn -/ -#print LocalEquiv.invOn /- +#print PartialEquiv.invOn /- protected theorem invOn : InvOn e.symm e e.source e.target := ⟨e.LeftInvOn, e.RightInvOn⟩ -#align local_equiv.inv_on LocalEquiv.invOn +#align local_equiv.inv_on PartialEquiv.invOn -/ -#print LocalEquiv.injOn /- +#print PartialEquiv.injOn /- protected theorem injOn : InjOn e e.source := e.LeftInvOn.InjOn -#align local_equiv.inj_on LocalEquiv.injOn +#align local_equiv.inj_on PartialEquiv.injOn -/ -#print LocalEquiv.bijOn /- +#print PartialEquiv.bijOn /- protected theorem bijOn : BijOn e e.source e.target := e.InvOn.BijOn e.MapsTo e.symm_mapsTo -#align local_equiv.bij_on LocalEquiv.bijOn +#align local_equiv.bij_on PartialEquiv.bijOn -/ -#print LocalEquiv.surjOn /- +#print PartialEquiv.surjOn /- protected theorem surjOn : SurjOn e e.source e.target := e.BijOn.SurjOn -#align local_equiv.surj_on LocalEquiv.surjOn +#align local_equiv.surj_on PartialEquiv.surjOn -/ -#print Equiv.toLocalEquiv /- +#print Equiv.toPartialEquiv /- /-- Associating a local_equiv to an equiv-/ @[simps (config := mfld_cfg)] -def Equiv.toLocalEquiv (e : α ≃ β) : LocalEquiv α β +def Equiv.toPartialEquiv (e : α ≃ β) : PartialEquiv α β where toFun := e invFun := e.symm @@ -278,20 +279,20 @@ def Equiv.toLocalEquiv (e : α ≃ β) : LocalEquiv α β map_target' y hy := mem_univ _ left_inv' x hx := e.left_inv x right_inv' x hx := e.right_inv x -#align equiv.to_local_equiv Equiv.toLocalEquiv +#align equiv.to_local_equiv Equiv.toPartialEquiv -/ -#print LocalEquiv.inhabitedOfEmpty /- -instance inhabitedOfEmpty [IsEmpty α] [IsEmpty β] : Inhabited (LocalEquiv α β) := - ⟨((Equiv.equivEmpty α).trans (Equiv.equivEmpty β).symm).toLocalEquiv⟩ -#align local_equiv.inhabited_of_empty LocalEquiv.inhabitedOfEmpty +#print PartialEquiv.inhabitedOfEmpty /- +instance inhabitedOfEmpty [IsEmpty α] [IsEmpty β] : Inhabited (PartialEquiv α β) := + ⟨((Equiv.equivEmpty α).trans (Equiv.equivEmpty β).symm).toPartialEquiv⟩ +#align local_equiv.inhabited_of_empty PartialEquiv.inhabitedOfEmpty -/ -#print LocalEquiv.copy /- +#print PartialEquiv.copy /- /-- Create a copy of a `local_equiv` providing better definitional equalities. -/ @[simps (config := { fullyApplied := false })] -def copy (e : LocalEquiv α β) (f : α → β) (hf : ⇑e = f) (g : β → α) (hg : ⇑e.symm = g) (s : Set α) - (hs : e.source = s) (t : Set β) (ht : e.target = t) : LocalEquiv α β +def copy (e : PartialEquiv α β) (f : α → β) (hf : ⇑e = f) (g : β → α) (hg : ⇑e.symm = g) (s : Set α) + (hs : e.source = s) (t : Set β) (ht : e.target = t) : PartialEquiv α β where toFun := f invFun := g @@ -301,17 +302,17 @@ def copy (e : LocalEquiv α β) (f : α → β) (hf : ⇑e = f) (g : β → α) map_target' y := hs ▸ ht ▸ hg ▸ e.map_target left_inv' x := hs ▸ hf ▸ hg ▸ e.left_inv right_inv' x := ht ▸ hf ▸ hg ▸ e.right_inv -#align local_equiv.copy LocalEquiv.copy +#align local_equiv.copy PartialEquiv.copy -/ -#print LocalEquiv.copy_eq /- -theorem copy_eq (e : LocalEquiv α β) (f : α → β) (hf : ⇑e = f) (g : β → α) (hg : ⇑e.symm = g) +#print PartialEquiv.copy_eq /- +theorem copy_eq (e : PartialEquiv α β) (f : α → β) (hf : ⇑e = f) (g : β → α) (hg : ⇑e.symm = g) (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t) : e.copy f hf g hg s hs t ht = e := by substs f g s t; cases e; rfl -#align local_equiv.copy_eq LocalEquiv.copy_eq +#align local_equiv.copy_eq PartialEquiv.copy_eq -/ -#print LocalEquiv.toEquiv /- +#print PartialEquiv.toEquiv /- /-- Associating to a local_equiv an equiv between the source and the target -/ protected def toEquiv : Equiv e.source e.target where @@ -319,48 +320,48 @@ protected def toEquiv : Equiv e.source e.target invFun y := ⟨e.symm y, e.map_target y.Mem⟩ left_inv := fun ⟨x, hx⟩ => Subtype.eq <| e.left_inv hx right_inv := fun ⟨y, hy⟩ => Subtype.eq <| e.right_inv hy -#align local_equiv.to_equiv LocalEquiv.toEquiv +#align local_equiv.to_equiv PartialEquiv.toEquiv -/ -#print LocalEquiv.symm_source /- +#print PartialEquiv.symm_source /- @[simp, mfld_simps] theorem symm_source : e.symm.source = e.target := rfl -#align local_equiv.symm_source LocalEquiv.symm_source +#align local_equiv.symm_source PartialEquiv.symm_source -/ -#print LocalEquiv.symm_target /- +#print PartialEquiv.symm_target /- @[simp, mfld_simps] theorem symm_target : e.symm.target = e.source := rfl -#align local_equiv.symm_target LocalEquiv.symm_target +#align local_equiv.symm_target PartialEquiv.symm_target -/ -#print LocalEquiv.symm_symm /- +#print PartialEquiv.symm_symm /- @[simp, mfld_simps] theorem symm_symm : e.symm.symm = e := by cases e; rfl -#align local_equiv.symm_symm LocalEquiv.symm_symm +#align local_equiv.symm_symm PartialEquiv.symm_symm -/ -#print LocalEquiv.image_source_eq_target /- +#print PartialEquiv.image_source_eq_target /- theorem image_source_eq_target : e '' e.source = e.target := e.BijOn.image_eq -#align local_equiv.image_source_eq_target LocalEquiv.image_source_eq_target +#align local_equiv.image_source_eq_target PartialEquiv.image_source_eq_target -/ -#print LocalEquiv.forall_mem_target /- +#print PartialEquiv.forall_mem_target /- theorem forall_mem_target {p : β → Prop} : (∀ y ∈ e.target, p y) ↔ ∀ x ∈ e.source, p (e x) := by rw [← image_source_eq_target, ball_image_iff] -#align local_equiv.forall_mem_target LocalEquiv.forall_mem_target +#align local_equiv.forall_mem_target PartialEquiv.forall_mem_target -/ -#print LocalEquiv.exists_mem_target /- +#print PartialEquiv.exists_mem_target /- theorem exists_mem_target {p : β → Prop} : (∃ y ∈ e.target, p y) ↔ ∃ x ∈ e.source, p (e x) := by rw [← image_source_eq_target, bex_image_iff] -#align local_equiv.exists_mem_target LocalEquiv.exists_mem_target +#align local_equiv.exists_mem_target PartialEquiv.exists_mem_target -/ -#print LocalEquiv.IsImage /- +#print PartialEquiv.IsImage /- /-- We say that `t : set β` is an image of `s : set α` under a local equivalence if any of the following equivalent conditions hold: @@ -370,54 +371,54 @@ any of the following equivalent conditions hold: -/ def IsImage (s : Set α) (t : Set β) : Prop := ∀ ⦃x⦄, x ∈ e.source → (e x ∈ t ↔ x ∈ s) -#align local_equiv.is_image LocalEquiv.IsImage +#align local_equiv.is_image PartialEquiv.IsImage -/ namespace IsImage variable {e} {s : Set α} {t : Set β} {x : α} {y : β} -#print LocalEquiv.IsImage.apply_mem_iff /- +#print PartialEquiv.IsImage.apply_mem_iff /- theorem apply_mem_iff (h : e.IsImage s t) (hx : x ∈ e.source) : e x ∈ t ↔ x ∈ s := h hx -#align local_equiv.is_image.apply_mem_iff LocalEquiv.IsImage.apply_mem_iff +#align local_equiv.is_image.apply_mem_iff PartialEquiv.IsImage.apply_mem_iff -/ -#print LocalEquiv.IsImage.symm_apply_mem_iff /- +#print PartialEquiv.IsImage.symm_apply_mem_iff /- theorem symm_apply_mem_iff (h : e.IsImage s t) : ∀ ⦃y⦄, y ∈ e.target → (e.symm y ∈ s ↔ y ∈ t) := e.forall_mem_target.mpr fun x hx => by rw [e.left_inv hx, h hx] -#align local_equiv.is_image.symm_apply_mem_iff LocalEquiv.IsImage.symm_apply_mem_iff +#align local_equiv.is_image.symm_apply_mem_iff PartialEquiv.IsImage.symm_apply_mem_iff -/ -#print LocalEquiv.IsImage.symm /- +#print PartialEquiv.IsImage.symm /- protected theorem symm (h : e.IsImage s t) : e.symm.IsImage t s := h.symm_apply_mem_iff -#align local_equiv.is_image.symm LocalEquiv.IsImage.symm +#align local_equiv.is_image.symm PartialEquiv.IsImage.symm -/ -#print LocalEquiv.IsImage.symm_iff /- +#print PartialEquiv.IsImage.symm_iff /- @[simp] theorem symm_iff : e.symm.IsImage t s ↔ e.IsImage s t := ⟨fun h => h.symm, fun h => h.symm⟩ -#align local_equiv.is_image.symm_iff LocalEquiv.IsImage.symm_iff +#align local_equiv.is_image.symm_iff PartialEquiv.IsImage.symm_iff -/ -#print LocalEquiv.IsImage.mapsTo /- +#print PartialEquiv.IsImage.mapsTo /- protected theorem mapsTo (h : e.IsImage s t) : MapsTo e (e.source ∩ s) (e.target ∩ t) := fun x hx => ⟨e.MapsTo hx.1, (h hx.1).2 hx.2⟩ -#align local_equiv.is_image.maps_to LocalEquiv.IsImage.mapsTo +#align local_equiv.is_image.maps_to PartialEquiv.IsImage.mapsTo -/ -#print LocalEquiv.IsImage.symm_mapsTo /- +#print PartialEquiv.IsImage.symm_mapsTo /- theorem symm_mapsTo (h : e.IsImage s t) : MapsTo e.symm (e.target ∩ t) (e.source ∩ s) := h.symm.MapsTo -#align local_equiv.is_image.symm_maps_to LocalEquiv.IsImage.symm_mapsTo +#align local_equiv.is_image.symm_maps_to PartialEquiv.IsImage.symm_mapsTo -/ -#print LocalEquiv.IsImage.restr /- +#print PartialEquiv.IsImage.restr /- /-- Restrict a `local_equiv` to a pair of corresponding sets. -/ @[simps (config := { fullyApplied := false })] -def restr (h : e.IsImage s t) : LocalEquiv α β +def restr (h : e.IsImage s t) : PartialEquiv α β where toFun := e invFun := e.symm @@ -427,80 +428,80 @@ def restr (h : e.IsImage s t) : LocalEquiv α β map_target' := h.symm_mapsTo left_inv' := e.LeftInvOn.mono (inter_subset_left _ _) right_inv' := e.RightInvOn.mono (inter_subset_left _ _) -#align local_equiv.is_image.restr LocalEquiv.IsImage.restr +#align local_equiv.is_image.restr PartialEquiv.IsImage.restr -/ -#print LocalEquiv.IsImage.image_eq /- +#print PartialEquiv.IsImage.image_eq /- theorem image_eq (h : e.IsImage s t) : e '' (e.source ∩ s) = e.target ∩ t := h.restr.image_source_eq_target -#align local_equiv.is_image.image_eq LocalEquiv.IsImage.image_eq +#align local_equiv.is_image.image_eq PartialEquiv.IsImage.image_eq -/ -#print LocalEquiv.IsImage.symm_image_eq /- +#print PartialEquiv.IsImage.symm_image_eq /- theorem symm_image_eq (h : e.IsImage s t) : e.symm '' (e.target ∩ t) = e.source ∩ s := h.symm.image_eq -#align local_equiv.is_image.symm_image_eq LocalEquiv.IsImage.symm_image_eq +#align local_equiv.is_image.symm_image_eq PartialEquiv.IsImage.symm_image_eq -/ -#print LocalEquiv.IsImage.iff_preimage_eq /- +#print PartialEquiv.IsImage.iff_preimage_eq /- theorem iff_preimage_eq : e.IsImage s t ↔ e.source ∩ e ⁻¹' t = e.source ∩ s := by simp only [is_image, Set.ext_iff, mem_inter_iff, and_congr_right_iff, mem_preimage] -#align local_equiv.is_image.iff_preimage_eq LocalEquiv.IsImage.iff_preimage_eq +#align local_equiv.is_image.iff_preimage_eq PartialEquiv.IsImage.iff_preimage_eq -/ alias ⟨preimage_eq, of_preimage_eq⟩ := iff_preimage_eq -#align local_equiv.is_image.preimage_eq LocalEquiv.IsImage.preimage_eq -#align local_equiv.is_image.of_preimage_eq LocalEquiv.IsImage.of_preimage_eq +#align local_equiv.is_image.preimage_eq PartialEquiv.IsImage.preimage_eq +#align local_equiv.is_image.of_preimage_eq PartialEquiv.IsImage.of_preimage_eq -#print LocalEquiv.IsImage.iff_symm_preimage_eq /- +#print PartialEquiv.IsImage.iff_symm_preimage_eq /- theorem iff_symm_preimage_eq : e.IsImage s t ↔ e.target ∩ e.symm ⁻¹' s = e.target ∩ t := symm_iff.symm.trans iff_preimage_eq -#align local_equiv.is_image.iff_symm_preimage_eq LocalEquiv.IsImage.iff_symm_preimage_eq +#align local_equiv.is_image.iff_symm_preimage_eq PartialEquiv.IsImage.iff_symm_preimage_eq -/ alias ⟨symm_preimage_eq, of_symm_preimage_eq⟩ := iff_symm_preimage_eq -#align local_equiv.is_image.symm_preimage_eq LocalEquiv.IsImage.symm_preimage_eq -#align local_equiv.is_image.of_symm_preimage_eq LocalEquiv.IsImage.of_symm_preimage_eq +#align local_equiv.is_image.symm_preimage_eq PartialEquiv.IsImage.symm_preimage_eq +#align local_equiv.is_image.of_symm_preimage_eq PartialEquiv.IsImage.of_symm_preimage_eq -#print LocalEquiv.IsImage.of_image_eq /- +#print PartialEquiv.IsImage.of_image_eq /- theorem of_image_eq (h : e '' (e.source ∩ s) = e.target ∩ t) : e.IsImage s t := of_symm_preimage_eq <| Eq.trans (of_symm_preimage_eq rfl).image_eq.symm h -#align local_equiv.is_image.of_image_eq LocalEquiv.IsImage.of_image_eq +#align local_equiv.is_image.of_image_eq PartialEquiv.IsImage.of_image_eq -/ -#print LocalEquiv.IsImage.of_symm_image_eq /- +#print PartialEquiv.IsImage.of_symm_image_eq /- theorem of_symm_image_eq (h : e.symm '' (e.target ∩ t) = e.source ∩ s) : e.IsImage s t := of_preimage_eq <| Eq.trans (of_preimage_eq rfl).symm_image_eq.symm h -#align local_equiv.is_image.of_symm_image_eq LocalEquiv.IsImage.of_symm_image_eq +#align local_equiv.is_image.of_symm_image_eq PartialEquiv.IsImage.of_symm_image_eq -/ -#print LocalEquiv.IsImage.compl /- +#print PartialEquiv.IsImage.compl /- protected theorem compl (h : e.IsImage s t) : e.IsImage (sᶜ) (tᶜ) := fun x hx => not_congr (h hx) -#align local_equiv.is_image.compl LocalEquiv.IsImage.compl +#align local_equiv.is_image.compl PartialEquiv.IsImage.compl -/ -#print LocalEquiv.IsImage.inter /- +#print PartialEquiv.IsImage.inter /- protected theorem inter {s' t'} (h : e.IsImage s t) (h' : e.IsImage s' t') : e.IsImage (s ∩ s') (t ∩ t') := fun x hx => and_congr (h hx) (h' hx) -#align local_equiv.is_image.inter LocalEquiv.IsImage.inter +#align local_equiv.is_image.inter PartialEquiv.IsImage.inter -/ -#print LocalEquiv.IsImage.union /- +#print PartialEquiv.IsImage.union /- protected theorem union {s' t'} (h : e.IsImage s t) (h' : e.IsImage s' t') : e.IsImage (s ∪ s') (t ∪ t') := fun x hx => or_congr (h hx) (h' hx) -#align local_equiv.is_image.union LocalEquiv.IsImage.union +#align local_equiv.is_image.union PartialEquiv.IsImage.union -/ -#print LocalEquiv.IsImage.diff /- +#print PartialEquiv.IsImage.diff /- protected theorem diff {s' t'} (h : e.IsImage s t) (h' : e.IsImage s' t') : e.IsImage (s \ s') (t \ t') := h.inter h'.compl -#align local_equiv.is_image.diff LocalEquiv.IsImage.diff +#align local_equiv.is_image.diff PartialEquiv.IsImage.diff -/ -#print LocalEquiv.IsImage.leftInvOn_piecewise /- -theorem leftInvOn_piecewise {e' : LocalEquiv α β} [∀ i, Decidable (i ∈ s)] [∀ i, Decidable (i ∈ t)] - (h : e.IsImage s t) (h' : e'.IsImage s t) : +#print PartialEquiv.IsImage.leftInvOn_piecewise /- +theorem leftInvOn_piecewise {e' : PartialEquiv α β} [∀ i, Decidable (i ∈ s)] + [∀ i, Decidable (i ∈ t)] (h : e.IsImage s t) (h' : e'.IsImage s t) : LeftInvOn (t.piecewise e.symm e'.symm) (s.piecewise e e') (s.ite e.source e'.source) := by rintro x (⟨he, hs⟩ | ⟨he, hs : x ∉ s⟩) @@ -508,18 +509,18 @@ theorem leftInvOn_piecewise {e' : LocalEquiv α β} [∀ i, Decidable (i ∈ s)] · rw [piecewise_eq_of_not_mem _ _ _ hs, piecewise_eq_of_not_mem _ _ _ ((h'.compl he).2 hs), e'.left_inv he] -#align local_equiv.is_image.left_inv_on_piecewise LocalEquiv.IsImage.leftInvOn_piecewise +#align local_equiv.is_image.left_inv_on_piecewise PartialEquiv.IsImage.leftInvOn_piecewise -/ -#print LocalEquiv.IsImage.inter_eq_of_inter_eq_of_eqOn /- -theorem inter_eq_of_inter_eq_of_eqOn {e' : LocalEquiv α β} (h : e.IsImage s t) (h' : e'.IsImage s t) - (hs : e.source ∩ s = e'.source ∩ s) (Heq : EqOn e e' (e.source ∩ s)) : +#print PartialEquiv.IsImage.inter_eq_of_inter_eq_of_eqOn /- +theorem inter_eq_of_inter_eq_of_eqOn {e' : PartialEquiv α β} (h : e.IsImage s t) + (h' : e'.IsImage s t) (hs : e.source ∩ s = e'.source ∩ s) (Heq : EqOn e e' (e.source ∩ s)) : e.target ∩ t = e'.target ∩ t := by rw [← h.image_eq, ← h'.image_eq, ← hs, Heq.image_eq] -#align local_equiv.is_image.inter_eq_of_inter_eq_of_eq_on LocalEquiv.IsImage.inter_eq_of_inter_eq_of_eqOn +#align local_equiv.is_image.inter_eq_of_inter_eq_of_eq_on PartialEquiv.IsImage.inter_eq_of_inter_eq_of_eqOn -/ -#print LocalEquiv.IsImage.symm_eq_on_of_inter_eq_of_eqOn /- -theorem symm_eq_on_of_inter_eq_of_eqOn {e' : LocalEquiv α β} (h : e.IsImage s t) +#print PartialEquiv.IsImage.symm_eq_on_of_inter_eq_of_eqOn /- +theorem symm_eq_on_of_inter_eq_of_eqOn {e' : PartialEquiv α β} (h : e.IsImage s t) (hs : e.source ∩ s = e'.source ∩ s) (Heq : EqOn e e' (e.source ∩ s)) : EqOn e.symm e'.symm (e.target ∩ t) := by @@ -527,118 +528,118 @@ theorem symm_eq_on_of_inter_eq_of_eqOn {e' : LocalEquiv α β} (h : e.IsImage s rintro y ⟨x, hx, rfl⟩ have hx' := hx; rw [hs] at hx' rw [e.left_inv hx.1, Heq hx, e'.left_inv hx'.1] -#align local_equiv.is_image.symm_eq_on_of_inter_eq_of_eq_on LocalEquiv.IsImage.symm_eq_on_of_inter_eq_of_eqOn +#align local_equiv.is_image.symm_eq_on_of_inter_eq_of_eq_on PartialEquiv.IsImage.symm_eq_on_of_inter_eq_of_eqOn -/ end IsImage -#print LocalEquiv.isImage_source_target /- +#print PartialEquiv.isImage_source_target /- theorem isImage_source_target : e.IsImage e.source e.target := fun x hx => by simp [hx] -#align local_equiv.is_image_source_target LocalEquiv.isImage_source_target +#align local_equiv.is_image_source_target PartialEquiv.isImage_source_target -/ -#print LocalEquiv.isImage_source_target_of_disjoint /- -theorem isImage_source_target_of_disjoint (e' : LocalEquiv α β) (hs : Disjoint e.source e'.source) +#print PartialEquiv.isImage_source_target_of_disjoint /- +theorem isImage_source_target_of_disjoint (e' : PartialEquiv α β) (hs : Disjoint e.source e'.source) (ht : Disjoint e.target e'.target) : e.IsImage e'.source e'.target := IsImage.of_image_eq <| by rw [hs.inter_eq, ht.inter_eq, image_empty] -#align local_equiv.is_image_source_target_of_disjoint LocalEquiv.isImage_source_target_of_disjoint +#align local_equiv.is_image_source_target_of_disjoint PartialEquiv.isImage_source_target_of_disjoint -/ -#print LocalEquiv.image_source_inter_eq' /- +#print PartialEquiv.image_source_inter_eq' /- theorem image_source_inter_eq' (s : Set α) : e '' (e.source ∩ s) = e.target ∩ e.symm ⁻¹' s := by rw [inter_comm, e.left_inv_on.image_inter', image_source_eq_target, inter_comm] -#align local_equiv.image_source_inter_eq' LocalEquiv.image_source_inter_eq' +#align local_equiv.image_source_inter_eq' PartialEquiv.image_source_inter_eq' -/ -#print LocalEquiv.image_source_inter_eq /- +#print PartialEquiv.image_source_inter_eq /- theorem image_source_inter_eq (s : Set α) : e '' (e.source ∩ s) = e.target ∩ e.symm ⁻¹' (e.source ∩ s) := by rw [inter_comm, e.left_inv_on.image_inter, image_source_eq_target, inter_comm] -#align local_equiv.image_source_inter_eq LocalEquiv.image_source_inter_eq +#align local_equiv.image_source_inter_eq PartialEquiv.image_source_inter_eq -/ -#print LocalEquiv.image_eq_target_inter_inv_preimage /- +#print PartialEquiv.image_eq_target_inter_inv_preimage /- theorem image_eq_target_inter_inv_preimage {s : Set α} (h : s ⊆ e.source) : e '' s = e.target ∩ e.symm ⁻¹' s := by rw [← e.image_source_inter_eq', inter_eq_self_of_subset_right h] -#align local_equiv.image_eq_target_inter_inv_preimage LocalEquiv.image_eq_target_inter_inv_preimage +#align local_equiv.image_eq_target_inter_inv_preimage PartialEquiv.image_eq_target_inter_inv_preimage -/ -#print LocalEquiv.symm_image_eq_source_inter_preimage /- +#print PartialEquiv.symm_image_eq_source_inter_preimage /- theorem symm_image_eq_source_inter_preimage {s : Set β} (h : s ⊆ e.target) : e.symm '' s = e.source ∩ e ⁻¹' s := e.symm.image_eq_target_inter_inv_preimage h -#align local_equiv.symm_image_eq_source_inter_preimage LocalEquiv.symm_image_eq_source_inter_preimage +#align local_equiv.symm_image_eq_source_inter_preimage PartialEquiv.symm_image_eq_source_inter_preimage -/ -#print LocalEquiv.symm_image_target_inter_eq /- +#print PartialEquiv.symm_image_target_inter_eq /- theorem symm_image_target_inter_eq (s : Set β) : e.symm '' (e.target ∩ s) = e.source ∩ e ⁻¹' (e.target ∩ s) := e.symm.image_source_inter_eq _ -#align local_equiv.symm_image_target_inter_eq LocalEquiv.symm_image_target_inter_eq +#align local_equiv.symm_image_target_inter_eq PartialEquiv.symm_image_target_inter_eq -/ -#print LocalEquiv.symm_image_target_inter_eq' /- +#print PartialEquiv.symm_image_target_inter_eq' /- theorem symm_image_target_inter_eq' (s : Set β) : e.symm '' (e.target ∩ s) = e.source ∩ e ⁻¹' s := e.symm.image_source_inter_eq' _ -#align local_equiv.symm_image_target_inter_eq' LocalEquiv.symm_image_target_inter_eq' +#align local_equiv.symm_image_target_inter_eq' PartialEquiv.symm_image_target_inter_eq' -/ -#print LocalEquiv.source_inter_preimage_inv_preimage /- +#print PartialEquiv.source_inter_preimage_inv_preimage /- theorem source_inter_preimage_inv_preimage (s : Set α) : e.source ∩ e ⁻¹' (e.symm ⁻¹' s) = e.source ∩ s := Set.ext fun x => and_congr_right_iff.2 fun hx => by simp only [mem_preimage, e.left_inv hx] -#align local_equiv.source_inter_preimage_inv_preimage LocalEquiv.source_inter_preimage_inv_preimage +#align local_equiv.source_inter_preimage_inv_preimage PartialEquiv.source_inter_preimage_inv_preimage -/ -#print LocalEquiv.source_inter_preimage_target_inter /- +#print PartialEquiv.source_inter_preimage_target_inter /- theorem source_inter_preimage_target_inter (s : Set β) : e.source ∩ e ⁻¹' (e.target ∩ s) = e.source ∩ e ⁻¹' s := ext fun x => ⟨fun hx => ⟨hx.1, hx.2.2⟩, fun hx => ⟨hx.1, e.map_source hx.1, hx.2⟩⟩ -#align local_equiv.source_inter_preimage_target_inter LocalEquiv.source_inter_preimage_target_inter +#align local_equiv.source_inter_preimage_target_inter PartialEquiv.source_inter_preimage_target_inter -/ -#print LocalEquiv.target_inter_inv_preimage_preimage /- +#print PartialEquiv.target_inter_inv_preimage_preimage /- theorem target_inter_inv_preimage_preimage (s : Set β) : e.target ∩ e.symm ⁻¹' (e ⁻¹' s) = e.target ∩ s := e.symm.source_inter_preimage_inv_preimage _ -#align local_equiv.target_inter_inv_preimage_preimage LocalEquiv.target_inter_inv_preimage_preimage +#align local_equiv.target_inter_inv_preimage_preimage PartialEquiv.target_inter_inv_preimage_preimage -/ -#print LocalEquiv.symm_image_image_of_subset_source /- +#print PartialEquiv.symm_image_image_of_subset_source /- theorem symm_image_image_of_subset_source {s : Set α} (h : s ⊆ e.source) : e.symm '' (e '' s) = s := (e.LeftInvOn.mono h).image_image -#align local_equiv.symm_image_image_of_subset_source LocalEquiv.symm_image_image_of_subset_source +#align local_equiv.symm_image_image_of_subset_source PartialEquiv.symm_image_image_of_subset_source -/ -#print LocalEquiv.image_symm_image_of_subset_target /- +#print PartialEquiv.image_symm_image_of_subset_target /- theorem image_symm_image_of_subset_target {s : Set β} (h : s ⊆ e.target) : e '' (e.symm '' s) = s := e.symm.symm_image_image_of_subset_source h -#align local_equiv.image_symm_image_of_subset_target LocalEquiv.image_symm_image_of_subset_target +#align local_equiv.image_symm_image_of_subset_target PartialEquiv.image_symm_image_of_subset_target -/ -#print LocalEquiv.source_subset_preimage_target /- +#print PartialEquiv.source_subset_preimage_target /- theorem source_subset_preimage_target : e.source ⊆ e ⁻¹' e.target := e.MapsTo -#align local_equiv.source_subset_preimage_target LocalEquiv.source_subset_preimage_target +#align local_equiv.source_subset_preimage_target PartialEquiv.source_subset_preimage_target -/ -#print LocalEquiv.symm_image_target_eq_source /- +#print PartialEquiv.symm_image_target_eq_source /- theorem symm_image_target_eq_source : e.symm '' e.target = e.source := e.symm.image_source_eq_target -#align local_equiv.symm_image_target_eq_source LocalEquiv.symm_image_target_eq_source +#align local_equiv.symm_image_target_eq_source PartialEquiv.symm_image_target_eq_source -/ -#print LocalEquiv.target_subset_preimage_source /- +#print PartialEquiv.target_subset_preimage_source /- theorem target_subset_preimage_source : e.target ⊆ e.symm ⁻¹' e.source := e.symm_mapsTo -#align local_equiv.target_subset_preimage_source LocalEquiv.target_subset_preimage_source +#align local_equiv.target_subset_preimage_source PartialEquiv.target_subset_preimage_source -/ -#print LocalEquiv.ext /- +#print PartialEquiv.ext /- /-- Two local equivs that have the same `source`, same `to_fun` and same `inv_fun`, coincide. -/ @[ext] -protected theorem ext {e e' : LocalEquiv α β} (h : ∀ x, e x = e' x) +protected theorem ext {e e' : PartialEquiv α β} (h : ∀ x, e x = e' x) (hsymm : ∀ x, e.symm x = e'.symm x) (hs : e.source = e'.source) : e = e' := by have A : (e : α → β) = e' := by ext x; exact h x @@ -648,109 +649,109 @@ protected theorem ext {e e' : LocalEquiv α β} (h : ∀ x, e x = e' x) rw [A, hs, I'] at I cases e <;> cases e' simp_all -#align local_equiv.ext LocalEquiv.ext +#align local_equiv.ext PartialEquiv.ext -/ -#print LocalEquiv.restr /- +#print PartialEquiv.restr /- /-- Restricting a local equivalence to e.source ∩ s -/ -protected def restr (s : Set α) : LocalEquiv α β := +protected def restr (s : Set α) : PartialEquiv α β := (@IsImage.of_symm_preimage_eq α β e s (e.symm ⁻¹' s) rfl).restr -#align local_equiv.restr LocalEquiv.restr +#align local_equiv.restr PartialEquiv.restr -/ -#print LocalEquiv.restr_coe /- +#print PartialEquiv.restr_coe /- @[simp, mfld_simps] theorem restr_coe (s : Set α) : (e.restr s : α → β) = e := rfl -#align local_equiv.restr_coe LocalEquiv.restr_coe +#align local_equiv.restr_coe PartialEquiv.restr_coe -/ -#print LocalEquiv.restr_coe_symm /- +#print PartialEquiv.restr_coe_symm /- @[simp, mfld_simps] theorem restr_coe_symm (s : Set α) : ((e.restr s).symm : β → α) = e.symm := rfl -#align local_equiv.restr_coe_symm LocalEquiv.restr_coe_symm +#align local_equiv.restr_coe_symm PartialEquiv.restr_coe_symm -/ -#print LocalEquiv.restr_source /- +#print PartialEquiv.restr_source /- @[simp, mfld_simps] theorem restr_source (s : Set α) : (e.restr s).source = e.source ∩ s := rfl -#align local_equiv.restr_source LocalEquiv.restr_source +#align local_equiv.restr_source PartialEquiv.restr_source -/ -#print LocalEquiv.restr_target /- +#print PartialEquiv.restr_target /- @[simp, mfld_simps] theorem restr_target (s : Set α) : (e.restr s).target = e.target ∩ e.symm ⁻¹' s := rfl -#align local_equiv.restr_target LocalEquiv.restr_target +#align local_equiv.restr_target PartialEquiv.restr_target -/ -#print LocalEquiv.restr_eq_of_source_subset /- -theorem restr_eq_of_source_subset {e : LocalEquiv α β} {s : Set α} (h : e.source ⊆ s) : +#print PartialEquiv.restr_eq_of_source_subset /- +theorem restr_eq_of_source_subset {e : PartialEquiv α β} {s : Set α} (h : e.source ⊆ s) : e.restr s = e := - LocalEquiv.ext (fun _ => rfl) (fun _ => rfl) (by simp [inter_eq_self_of_subset_left h]) -#align local_equiv.restr_eq_of_source_subset LocalEquiv.restr_eq_of_source_subset + PartialEquiv.ext (fun _ => rfl) (fun _ => rfl) (by simp [inter_eq_self_of_subset_left h]) +#align local_equiv.restr_eq_of_source_subset PartialEquiv.restr_eq_of_source_subset -/ -#print LocalEquiv.restr_univ /- +#print PartialEquiv.restr_univ /- @[simp, mfld_simps] -theorem restr_univ {e : LocalEquiv α β} : e.restr univ = e := +theorem restr_univ {e : PartialEquiv α β} : e.restr univ = e := restr_eq_of_source_subset (subset_univ _) -#align local_equiv.restr_univ LocalEquiv.restr_univ +#align local_equiv.restr_univ PartialEquiv.restr_univ -/ -#print LocalEquiv.refl /- +#print PartialEquiv.refl /- /-- The identity local equiv -/ -protected def refl (α : Type _) : LocalEquiv α α := - (Equiv.refl α).toLocalEquiv -#align local_equiv.refl LocalEquiv.refl +protected def refl (α : Type _) : PartialEquiv α α := + (Equiv.refl α).toPartialEquiv +#align local_equiv.refl PartialEquiv.refl -/ -#print LocalEquiv.refl_source /- +#print PartialEquiv.refl_source /- @[simp, mfld_simps] -theorem refl_source : (LocalEquiv.refl α).source = univ := +theorem refl_source : (PartialEquiv.refl α).source = univ := rfl -#align local_equiv.refl_source LocalEquiv.refl_source +#align local_equiv.refl_source PartialEquiv.refl_source -/ -#print LocalEquiv.refl_target /- +#print PartialEquiv.refl_target /- @[simp, mfld_simps] -theorem refl_target : (LocalEquiv.refl α).target = univ := +theorem refl_target : (PartialEquiv.refl α).target = univ := rfl -#align local_equiv.refl_target LocalEquiv.refl_target +#align local_equiv.refl_target PartialEquiv.refl_target -/ -#print LocalEquiv.refl_coe /- +#print PartialEquiv.refl_coe /- @[simp, mfld_simps] -theorem refl_coe : (LocalEquiv.refl α : α → α) = id := +theorem refl_coe : (PartialEquiv.refl α : α → α) = id := rfl -#align local_equiv.refl_coe LocalEquiv.refl_coe +#align local_equiv.refl_coe PartialEquiv.refl_coe -/ -#print LocalEquiv.refl_symm /- +#print PartialEquiv.refl_symm /- @[simp, mfld_simps] -theorem refl_symm : (LocalEquiv.refl α).symm = LocalEquiv.refl α := +theorem refl_symm : (PartialEquiv.refl α).symm = PartialEquiv.refl α := rfl -#align local_equiv.refl_symm LocalEquiv.refl_symm +#align local_equiv.refl_symm PartialEquiv.refl_symm -/ -#print LocalEquiv.refl_restr_source /- +#print PartialEquiv.refl_restr_source /- @[simp, mfld_simps] -theorem refl_restr_source (s : Set α) : ((LocalEquiv.refl α).restr s).source = s := by simp -#align local_equiv.refl_restr_source LocalEquiv.refl_restr_source +theorem refl_restr_source (s : Set α) : ((PartialEquiv.refl α).restr s).source = s := by simp +#align local_equiv.refl_restr_source PartialEquiv.refl_restr_source -/ -#print LocalEquiv.refl_restr_target /- +#print PartialEquiv.refl_restr_target /- @[simp, mfld_simps] -theorem refl_restr_target (s : Set α) : ((LocalEquiv.refl α).restr s).target = s := by +theorem refl_restr_target (s : Set α) : ((PartialEquiv.refl α).restr s).target = s := by change univ ∩ id ⁻¹' s = s; simp -#align local_equiv.refl_restr_target LocalEquiv.refl_restr_target +#align local_equiv.refl_restr_target PartialEquiv.refl_restr_target -/ -#print LocalEquiv.ofSet /- +#print PartialEquiv.ofSet /- /-- The identity local equiv on a set `s` -/ -def ofSet (s : Set α) : LocalEquiv α α where +def ofSet (s : Set α) : PartialEquiv α α where toFun := id invFun := id source := s @@ -759,41 +760,41 @@ def ofSet (s : Set α) : LocalEquiv α α where map_target' x hx := hx left_inv' x hx := rfl right_inv' x hx := rfl -#align local_equiv.of_set LocalEquiv.ofSet +#align local_equiv.of_set PartialEquiv.ofSet -/ -#print LocalEquiv.ofSet_source /- +#print PartialEquiv.ofSet_source /- @[simp, mfld_simps] -theorem ofSet_source (s : Set α) : (LocalEquiv.ofSet s).source = s := +theorem ofSet_source (s : Set α) : (PartialEquiv.ofSet s).source = s := rfl -#align local_equiv.of_set_source LocalEquiv.ofSet_source +#align local_equiv.of_set_source PartialEquiv.ofSet_source -/ -#print LocalEquiv.ofSet_target /- +#print PartialEquiv.ofSet_target /- @[simp, mfld_simps] -theorem ofSet_target (s : Set α) : (LocalEquiv.ofSet s).target = s := +theorem ofSet_target (s : Set α) : (PartialEquiv.ofSet s).target = s := rfl -#align local_equiv.of_set_target LocalEquiv.ofSet_target +#align local_equiv.of_set_target PartialEquiv.ofSet_target -/ -#print LocalEquiv.ofSet_coe /- +#print PartialEquiv.ofSet_coe /- @[simp, mfld_simps] -theorem ofSet_coe (s : Set α) : (LocalEquiv.ofSet s : α → α) = id := +theorem ofSet_coe (s : Set α) : (PartialEquiv.ofSet s : α → α) = id := rfl -#align local_equiv.of_set_coe LocalEquiv.ofSet_coe +#align local_equiv.of_set_coe PartialEquiv.ofSet_coe -/ -#print LocalEquiv.ofSet_symm /- +#print PartialEquiv.ofSet_symm /- @[simp, mfld_simps] -theorem ofSet_symm (s : Set α) : (LocalEquiv.ofSet s).symm = LocalEquiv.ofSet s := +theorem ofSet_symm (s : Set α) : (PartialEquiv.ofSet s).symm = PartialEquiv.ofSet s := rfl -#align local_equiv.of_set_symm LocalEquiv.ofSet_symm +#align local_equiv.of_set_symm PartialEquiv.ofSet_symm -/ -#print LocalEquiv.trans' /- +#print PartialEquiv.trans' /- /-- Composing two local equivs if the target of the first coincides with the source of the second. -/ -protected def trans' (e' : LocalEquiv β γ) (h : e.target = e'.source) : LocalEquiv α γ +protected def trans' (e' : PartialEquiv β γ) (h : e.target = e'.source) : PartialEquiv α γ where toFun := e' ∘ e invFun := e.symm ∘ e'.symm @@ -803,243 +804,245 @@ protected def trans' (e' : LocalEquiv β γ) (h : e.target = e'.source) : LocalE map_target' y hy := by simp [h, hy] left_inv' x hx := by simp [hx, h.symm] right_inv' y hy := by simp [hy, h] -#align local_equiv.trans' LocalEquiv.trans' +#align local_equiv.trans' PartialEquiv.trans' -/ -#print LocalEquiv.trans /- +#print PartialEquiv.trans /- /-- Composing two local equivs, by restricting to the maximal domain where their composition is well defined. -/ -protected def trans : LocalEquiv α γ := - LocalEquiv.trans' (e.symm.restr e'.source).symm (e'.restr e.target) (inter_comm _ _) -#align local_equiv.trans LocalEquiv.trans +protected def trans : PartialEquiv α γ := + PartialEquiv.trans' (e.symm.restr e'.source).symm (e'.restr e.target) (inter_comm _ _) +#align local_equiv.trans PartialEquiv.trans -/ -#print LocalEquiv.coe_trans /- +#print PartialEquiv.coe_trans /- @[simp, mfld_simps] theorem coe_trans : (e.trans e' : α → γ) = e' ∘ e := rfl -#align local_equiv.coe_trans LocalEquiv.coe_trans +#align local_equiv.coe_trans PartialEquiv.coe_trans -/ -#print LocalEquiv.coe_trans_symm /- +#print PartialEquiv.coe_trans_symm /- @[simp, mfld_simps] theorem coe_trans_symm : ((e.trans e').symm : γ → α) = e.symm ∘ e'.symm := rfl -#align local_equiv.coe_trans_symm LocalEquiv.coe_trans_symm +#align local_equiv.coe_trans_symm PartialEquiv.coe_trans_symm -/ -#print LocalEquiv.trans_apply /- +#print PartialEquiv.trans_apply /- theorem trans_apply {x : α} : (e.trans e') x = e' (e x) := rfl -#align local_equiv.trans_apply LocalEquiv.trans_apply +#align local_equiv.trans_apply PartialEquiv.trans_apply -/ -#print LocalEquiv.trans_symm_eq_symm_trans_symm /- +#print PartialEquiv.trans_symm_eq_symm_trans_symm /- theorem trans_symm_eq_symm_trans_symm : (e.trans e').symm = e'.symm.trans e.symm := by cases e <;> cases e' <;> rfl -#align local_equiv.trans_symm_eq_symm_trans_symm LocalEquiv.trans_symm_eq_symm_trans_symm +#align local_equiv.trans_symm_eq_symm_trans_symm PartialEquiv.trans_symm_eq_symm_trans_symm -/ -#print LocalEquiv.trans_source /- +#print PartialEquiv.trans_source /- @[simp, mfld_simps] theorem trans_source : (e.trans e').source = e.source ∩ e ⁻¹' e'.source := rfl -#align local_equiv.trans_source LocalEquiv.trans_source +#align local_equiv.trans_source PartialEquiv.trans_source -/ -#print LocalEquiv.trans_source' /- +#print PartialEquiv.trans_source' /- theorem trans_source' : (e.trans e').source = e.source ∩ e ⁻¹' (e.target ∩ e'.source) := by mfld_set_tac -#align local_equiv.trans_source' LocalEquiv.trans_source' +#align local_equiv.trans_source' PartialEquiv.trans_source' -/ -#print LocalEquiv.trans_source'' /- +#print PartialEquiv.trans_source'' /- theorem trans_source'' : (e.trans e').source = e.symm '' (e.target ∩ e'.source) := by rw [e.trans_source', e.symm_image_target_inter_eq] -#align local_equiv.trans_source'' LocalEquiv.trans_source'' +#align local_equiv.trans_source'' PartialEquiv.trans_source'' -/ -#print LocalEquiv.image_trans_source /- +#print PartialEquiv.image_trans_source /- theorem image_trans_source : e '' (e.trans e').source = e.target ∩ e'.source := (e.symm.restr e'.source).symm.image_source_eq_target -#align local_equiv.image_trans_source LocalEquiv.image_trans_source +#align local_equiv.image_trans_source PartialEquiv.image_trans_source -/ -#print LocalEquiv.trans_target /- +#print PartialEquiv.trans_target /- @[simp, mfld_simps] theorem trans_target : (e.trans e').target = e'.target ∩ e'.symm ⁻¹' e.target := rfl -#align local_equiv.trans_target LocalEquiv.trans_target +#align local_equiv.trans_target PartialEquiv.trans_target -/ -#print LocalEquiv.trans_target' /- +#print PartialEquiv.trans_target' /- theorem trans_target' : (e.trans e').target = e'.target ∩ e'.symm ⁻¹' (e'.source ∩ e.target) := trans_source' e'.symm e.symm -#align local_equiv.trans_target' LocalEquiv.trans_target' +#align local_equiv.trans_target' PartialEquiv.trans_target' -/ -#print LocalEquiv.trans_target'' /- +#print PartialEquiv.trans_target'' /- theorem trans_target'' : (e.trans e').target = e' '' (e'.source ∩ e.target) := trans_source'' e'.symm e.symm -#align local_equiv.trans_target'' LocalEquiv.trans_target'' +#align local_equiv.trans_target'' PartialEquiv.trans_target'' -/ -#print LocalEquiv.inv_image_trans_target /- +#print PartialEquiv.inv_image_trans_target /- theorem inv_image_trans_target : e'.symm '' (e.trans e').target = e'.source ∩ e.target := image_trans_source e'.symm e.symm -#align local_equiv.inv_image_trans_target LocalEquiv.inv_image_trans_target +#align local_equiv.inv_image_trans_target PartialEquiv.inv_image_trans_target -/ -#print LocalEquiv.trans_assoc /- -theorem trans_assoc (e'' : LocalEquiv γ δ) : (e.trans e').trans e'' = e.trans (e'.trans e'') := - LocalEquiv.ext (fun x => rfl) (fun x => rfl) +#print PartialEquiv.trans_assoc /- +theorem trans_assoc (e'' : PartialEquiv γ δ) : (e.trans e').trans e'' = e.trans (e'.trans e'') := + PartialEquiv.ext (fun x => rfl) (fun x => rfl) (by simp [trans_source, @preimage_comp α β γ, inter_assoc]) -#align local_equiv.trans_assoc LocalEquiv.trans_assoc +#align local_equiv.trans_assoc PartialEquiv.trans_assoc -/ -#print LocalEquiv.trans_refl /- +#print PartialEquiv.trans_refl /- @[simp, mfld_simps] -theorem trans_refl : e.trans (LocalEquiv.refl β) = e := - LocalEquiv.ext (fun x => rfl) (fun x => rfl) (by simp [trans_source]) -#align local_equiv.trans_refl LocalEquiv.trans_refl +theorem trans_refl : e.trans (PartialEquiv.refl β) = e := + PartialEquiv.ext (fun x => rfl) (fun x => rfl) (by simp [trans_source]) +#align local_equiv.trans_refl PartialEquiv.trans_refl -/ -#print LocalEquiv.refl_trans /- +#print PartialEquiv.refl_trans /- @[simp, mfld_simps] -theorem refl_trans : (LocalEquiv.refl α).trans e = e := - LocalEquiv.ext (fun x => rfl) (fun x => rfl) (by simp [trans_source, preimage_id]) -#align local_equiv.refl_trans LocalEquiv.refl_trans +theorem refl_trans : (PartialEquiv.refl α).trans e = e := + PartialEquiv.ext (fun x => rfl) (fun x => rfl) (by simp [trans_source, preimage_id]) +#align local_equiv.refl_trans PartialEquiv.refl_trans -/ -#print LocalEquiv.trans_refl_restr /- -theorem trans_refl_restr (s : Set β) : e.trans ((LocalEquiv.refl β).restr s) = e.restr (e ⁻¹' s) := - LocalEquiv.ext (fun x => rfl) (fun x => rfl) (by simp [trans_source]) -#align local_equiv.trans_refl_restr LocalEquiv.trans_refl_restr +#print PartialEquiv.trans_refl_restr /- +theorem trans_refl_restr (s : Set β) : + e.trans ((PartialEquiv.refl β).restr s) = e.restr (e ⁻¹' s) := + PartialEquiv.ext (fun x => rfl) (fun x => rfl) (by simp [trans_source]) +#align local_equiv.trans_refl_restr PartialEquiv.trans_refl_restr -/ -#print LocalEquiv.trans_refl_restr' /- +#print PartialEquiv.trans_refl_restr' /- theorem trans_refl_restr' (s : Set β) : - e.trans ((LocalEquiv.refl β).restr s) = e.restr (e.source ∩ e ⁻¹' s) := - (LocalEquiv.ext (fun x => rfl) fun x => rfl) <| by simp [trans_source]; + e.trans ((PartialEquiv.refl β).restr s) = e.restr (e.source ∩ e ⁻¹' s) := + (PartialEquiv.ext (fun x => rfl) fun x => rfl) <| by simp [trans_source]; rw [← inter_assoc, inter_self] -#align local_equiv.trans_refl_restr' LocalEquiv.trans_refl_restr' +#align local_equiv.trans_refl_restr' PartialEquiv.trans_refl_restr' -/ -#print LocalEquiv.restr_trans /- +#print PartialEquiv.restr_trans /- theorem restr_trans (s : Set α) : (e.restr s).trans e' = (e.trans e').restr s := - (LocalEquiv.ext (fun x => rfl) fun x => rfl) <| by simp [trans_source, inter_comm]; + (PartialEquiv.ext (fun x => rfl) fun x => rfl) <| by simp [trans_source, inter_comm]; rwa [inter_assoc] -#align local_equiv.restr_trans LocalEquiv.restr_trans +#align local_equiv.restr_trans PartialEquiv.restr_trans -/ -#print LocalEquiv.mem_symm_trans_source /- +#print PartialEquiv.mem_symm_trans_source /- /-- A lemma commonly useful when `e` and `e'` are charts of a manifold. -/ -theorem mem_symm_trans_source {e' : LocalEquiv α γ} {x : α} (he : x ∈ e.source) +theorem mem_symm_trans_source {e' : PartialEquiv α γ} {x : α} (he : x ∈ e.source) (he' : x ∈ e'.source) : e x ∈ (e.symm.trans e').source := - ⟨e.MapsTo he, by rwa [mem_preimage, LocalEquiv.symm_symm, e.left_inv he]⟩ -#align local_equiv.mem_symm_trans_source LocalEquiv.mem_symm_trans_source + ⟨e.MapsTo he, by rwa [mem_preimage, PartialEquiv.symm_symm, e.left_inv he]⟩ +#align local_equiv.mem_symm_trans_source PartialEquiv.mem_symm_trans_source -/ -#print LocalEquiv.transEquiv /- +#print PartialEquiv.transEquiv /- /-- Postcompose a local equivalence with an equivalence. We modify the source and target to have better definitional behavior. -/ @[simps] -def transEquiv (e' : β ≃ γ) : LocalEquiv α γ := - (e.trans e'.toLocalEquiv).copy _ rfl _ rfl e.source (inter_univ _) (e'.symm ⁻¹' e.target) +def transEquiv (e' : β ≃ γ) : PartialEquiv α γ := + (e.trans e'.toPartialEquiv).copy _ rfl _ rfl e.source (inter_univ _) (e'.symm ⁻¹' e.target) (univ_inter _) -#align local_equiv.trans_equiv LocalEquiv.transEquiv +#align local_equiv.trans_equiv PartialEquiv.transEquiv -/ -#print LocalEquiv.transEquiv_eq_trans /- -theorem transEquiv_eq_trans (e' : β ≃ γ) : e.transEquiv e' = e.trans e'.toLocalEquiv := +#print PartialEquiv.transEquiv_eq_trans /- +theorem transEquiv_eq_trans (e' : β ≃ γ) : e.transEquiv e' = e.trans e'.toPartialEquiv := copy_eq _ _ _ _ _ _ _ _ _ -#align local_equiv.trans_equiv_eq_trans LocalEquiv.transEquiv_eq_trans +#align local_equiv.trans_equiv_eq_trans PartialEquiv.transEquiv_eq_trans -/ -#print Equiv.transLocalEquiv /- +#print Equiv.transPartialEquiv /- /-- Precompose a local equivalence with an equivalence. We modify the source and target to have better definitional behavior. -/ @[simps] -def Equiv.transLocalEquiv (e : α ≃ β) : LocalEquiv α γ := - (e.toLocalEquiv.trans e').copy _ rfl _ rfl (e ⁻¹' e'.source) (univ_inter _) e'.target +def Equiv.transPartialEquiv (e : α ≃ β) : PartialEquiv α γ := + (e.toPartialEquiv.trans e').copy _ rfl _ rfl (e ⁻¹' e'.source) (univ_inter _) e'.target (inter_univ _) -#align equiv.trans_local_equiv Equiv.transLocalEquiv +#align equiv.trans_local_equiv Equiv.transPartialEquiv -/ -#print Equiv.transLocalEquiv_eq_trans /- -theorem Equiv.transLocalEquiv_eq_trans (e : α ≃ β) : - e.transLocalEquiv e' = e.toLocalEquiv.trans e' := +#print Equiv.transPartialEquiv_eq_trans /- +theorem Equiv.transPartialEquiv_eq_trans (e : α ≃ β) : + e.transPartialEquiv e' = e.toPartialEquiv.trans e' := copy_eq _ _ _ _ _ _ _ _ _ -#align equiv.trans_local_equiv_eq_trans Equiv.transLocalEquiv_eq_trans +#align equiv.trans_local_equiv_eq_trans Equiv.transPartialEquiv_eq_trans -/ -#print LocalEquiv.EqOnSource /- +#print PartialEquiv.EqOnSource /- /-- `eq_on_source e e'` means that `e` and `e'` have the same source, and coincide there. Then `e` and `e'` should really be considered the same local equiv. -/ -def EqOnSource (e e' : LocalEquiv α β) : Prop := +def EqOnSource (e e' : PartialEquiv α β) : Prop := e.source = e'.source ∧ e.source.EqOn e e' -#align local_equiv.eq_on_source LocalEquiv.EqOnSource +#align local_equiv.eq_on_source PartialEquiv.EqOnSource -/ -#print LocalEquiv.eqOnSourceSetoid /- +#print PartialEquiv.eqOnSourceSetoid /- /-- `eq_on_source` is an equivalence relation -/ -instance eqOnSourceSetoid : Setoid (LocalEquiv α β) +instance eqOnSourceSetoid : Setoid (PartialEquiv α β) where R := EqOnSource iseqv := ⟨fun e => by simp [eq_on_source], fun e e' h => by simp [eq_on_source, h.1.symm]; exact fun x hx => (h.2 hx).symm, fun e e' e'' h h' => ⟨by rwa [← h'.1, ← h.1], fun x hx => by rw [← h'.2, h.2 hx]; rwa [← h.1]⟩⟩ -#align local_equiv.eq_on_source_setoid LocalEquiv.eqOnSourceSetoid +#align local_equiv.eq_on_source_setoid PartialEquiv.eqOnSourceSetoid -/ -#print LocalEquiv.eqOnSource_refl /- +#print PartialEquiv.eqOnSource_refl /- theorem eqOnSource_refl : e ≈ e := Setoid.refl _ -#align local_equiv.eq_on_source_refl LocalEquiv.eqOnSource_refl +#align local_equiv.eq_on_source_refl PartialEquiv.eqOnSource_refl -/ -#print LocalEquiv.EqOnSource.source_eq /- +#print PartialEquiv.EqOnSource.source_eq /- /-- Two equivalent local equivs have the same source -/ -theorem EqOnSource.source_eq {e e' : LocalEquiv α β} (h : e ≈ e') : e.source = e'.source := +theorem EqOnSource.source_eq {e e' : PartialEquiv α β} (h : e ≈ e') : e.source = e'.source := h.1 -#align local_equiv.eq_on_source.source_eq LocalEquiv.EqOnSource.source_eq +#align local_equiv.eq_on_source.source_eq PartialEquiv.EqOnSource.source_eq -/ -#print LocalEquiv.EqOnSource.eqOn /- +#print PartialEquiv.EqOnSource.eqOn /- /-- Two equivalent local equivs coincide on the source -/ -theorem EqOnSource.eqOn {e e' : LocalEquiv α β} (h : e ≈ e') : e.source.EqOn e e' := +theorem EqOnSource.eqOn {e e' : PartialEquiv α β} (h : e ≈ e') : e.source.EqOn e e' := h.2 -#align local_equiv.eq_on_source.eq_on LocalEquiv.EqOnSource.eqOn +#align local_equiv.eq_on_source.eq_on PartialEquiv.EqOnSource.eqOn -/ -#print LocalEquiv.EqOnSource.target_eq /- +#print PartialEquiv.EqOnSource.target_eq /- /-- Two equivalent local equivs have the same target -/ -theorem EqOnSource.target_eq {e e' : LocalEquiv α β} (h : e ≈ e') : e.target = e'.target := by +theorem EqOnSource.target_eq {e e' : PartialEquiv α β} (h : e ≈ e') : e.target = e'.target := by simp only [← image_source_eq_target, ← h.source_eq, h.2.image_eq] -#align local_equiv.eq_on_source.target_eq LocalEquiv.EqOnSource.target_eq +#align local_equiv.eq_on_source.target_eq PartialEquiv.EqOnSource.target_eq -/ -#print LocalEquiv.EqOnSource.symm' /- +#print PartialEquiv.EqOnSource.symm' /- /-- If two local equivs are equivalent, so are their inverses. -/ -theorem EqOnSource.symm' {e e' : LocalEquiv α β} (h : e ≈ e') : e.symm ≈ e'.symm := +theorem EqOnSource.symm' {e e' : PartialEquiv α β} (h : e ≈ e') : e.symm ≈ e'.symm := by refine' ⟨h.target_eq, eq_on_of_left_inv_on_of_right_inv_on e.left_inv_on _ _⟩ <;> simp only [symm_source, h.target_eq, h.source_eq, e'.symm_maps_to] exact e'.right_inv_on.congr_right e'.symm_maps_to (h.source_eq ▸ h.eq_on.symm) -#align local_equiv.eq_on_source.symm' LocalEquiv.EqOnSource.symm' +#align local_equiv.eq_on_source.symm' PartialEquiv.EqOnSource.symm' -/ -#print LocalEquiv.EqOnSource.symm_eqOn /- +#print PartialEquiv.EqOnSource.symm_eqOn /- /-- Two equivalent local equivs have coinciding inverses on the target -/ -theorem EqOnSource.symm_eqOn {e e' : LocalEquiv α β} (h : e ≈ e') : EqOn e.symm e'.symm e.target := +theorem EqOnSource.symm_eqOn {e e' : PartialEquiv α β} (h : e ≈ e') : + EqOn e.symm e'.symm e.target := h.symm'.EqOn -#align local_equiv.eq_on_source.symm_eq_on LocalEquiv.EqOnSource.symm_eqOn +#align local_equiv.eq_on_source.symm_eq_on PartialEquiv.EqOnSource.symm_eqOn -/ -#print LocalEquiv.EqOnSource.trans' /- +#print PartialEquiv.EqOnSource.trans' /- /-- Composition of local equivs respects equivalence -/ -theorem EqOnSource.trans' {e e' : LocalEquiv α β} {f f' : LocalEquiv β γ} (he : e ≈ e') +theorem EqOnSource.trans' {e e' : PartialEquiv α β} {f f' : PartialEquiv β γ} (he : e ≈ e') (hf : f ≈ f') : e.trans f ≈ e'.trans f' := by constructor @@ -1048,70 +1051,70 @@ theorem EqOnSource.trans' {e e' : LocalEquiv α β} {f f' : LocalEquiv β γ} (h · intro x hx rw [trans_source] at hx simp [(he.2 hx.1).symm, hf.2 hx.2] -#align local_equiv.eq_on_source.trans' LocalEquiv.EqOnSource.trans' +#align local_equiv.eq_on_source.trans' PartialEquiv.EqOnSource.trans' -/ -#print LocalEquiv.EqOnSource.restr /- +#print PartialEquiv.EqOnSource.restr /- /-- Restriction of local equivs respects equivalence -/ -theorem EqOnSource.restr {e e' : LocalEquiv α β} (he : e ≈ e') (s : Set α) : +theorem EqOnSource.restr {e e' : PartialEquiv α β} (he : e ≈ e') (s : Set α) : e.restr s ≈ e'.restr s := by constructor · simp [he.1] · intro x hx simp only [mem_inter_iff, restr_source] at hx exact he.2 hx.1 -#align local_equiv.eq_on_source.restr LocalEquiv.EqOnSource.restr +#align local_equiv.eq_on_source.restr PartialEquiv.EqOnSource.restr -/ -#print LocalEquiv.EqOnSource.source_inter_preimage_eq /- +#print PartialEquiv.EqOnSource.source_inter_preimage_eq /- /-- Preimages are respected by equivalence -/ -theorem EqOnSource.source_inter_preimage_eq {e e' : LocalEquiv α β} (he : e ≈ e') (s : Set β) : +theorem EqOnSource.source_inter_preimage_eq {e e' : PartialEquiv α β} (he : e ≈ e') (s : Set β) : e.source ∩ e ⁻¹' s = e'.source ∩ e' ⁻¹' s := by rw [he.eq_on.inter_preimage_eq, he.source_eq] -#align local_equiv.eq_on_source.source_inter_preimage_eq LocalEquiv.EqOnSource.source_inter_preimage_eq +#align local_equiv.eq_on_source.source_inter_preimage_eq PartialEquiv.EqOnSource.source_inter_preimage_eq -/ -#print LocalEquiv.trans_self_symm /- +#print PartialEquiv.trans_self_symm /- /-- Composition of a local equiv and its inverse is equivalent to the restriction of the identity to the source -/ -theorem trans_self_symm : e.trans e.symm ≈ LocalEquiv.ofSet e.source := +theorem trans_self_symm : e.trans e.symm ≈ PartialEquiv.ofSet e.source := by have A : (e.trans e.symm).source = e.source := by mfld_set_tac refine' ⟨by simp [A], fun x hx => _⟩ rw [A] at hx simp only [hx, mfld_simps] -#align local_equiv.trans_self_symm LocalEquiv.trans_self_symm +#align local_equiv.trans_self_symm PartialEquiv.trans_self_symm -/ -#print LocalEquiv.trans_symm_self /- +#print PartialEquiv.trans_symm_self /- /-- Composition of the inverse of a local equiv and this local equiv is equivalent to the restriction of the identity to the target -/ -theorem trans_symm_self : e.symm.trans e ≈ LocalEquiv.ofSet e.target := +theorem trans_symm_self : e.symm.trans e ≈ PartialEquiv.ofSet e.target := trans_self_symm e.symm -#align local_equiv.trans_symm_self LocalEquiv.trans_symm_self +#align local_equiv.trans_symm_self PartialEquiv.trans_symm_self -/ -#print LocalEquiv.eq_of_eqOnSource_univ /- +#print PartialEquiv.eq_of_eqOnSource_univ /- /-- Two equivalent local equivs are equal when the source and target are univ -/ -theorem eq_of_eqOnSource_univ (e e' : LocalEquiv α β) (h : e ≈ e') (s : e.source = univ) +theorem eq_of_eqOnSource_univ (e e' : PartialEquiv α β) (h : e ≈ e') (s : e.source = univ) (t : e.target = univ) : e = e' := by - apply LocalEquiv.ext (fun x => _) (fun x => _) h.1 + apply PartialEquiv.ext (fun x => _) (fun x => _) h.1 · apply h.2 rw [s] exact mem_univ _ · apply h.symm'.2 rw [symm_source, t] exact mem_univ _ -#align local_equiv.eq_of_eq_on_source_univ LocalEquiv.eq_of_eqOnSource_univ +#align local_equiv.eq_of_eq_on_source_univ PartialEquiv.eq_of_eqOnSource_univ -/ section Prod /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -#print LocalEquiv.prod /- +#print PartialEquiv.prod /- /-- The product of two local equivs, as a local equiv on the product. -/ -def prod (e : LocalEquiv α β) (e' : LocalEquiv γ δ) : LocalEquiv (α × γ) (β × δ) +def prod (e : PartialEquiv α β) (e' : PartialEquiv γ δ) : PartialEquiv (α × γ) (β × δ) where source := e.source ×ˢ e'.source target := e.target ×ˢ e'.target @@ -1121,76 +1124,77 @@ def prod (e : LocalEquiv α β) (e' : LocalEquiv γ δ) : LocalEquiv (α × γ) map_target' p hp := by simp at hp ; simp [map_target, hp] left_inv' p hp := by simp at hp ; simp [hp] right_inv' p hp := by simp at hp ; simp [hp] -#align local_equiv.prod LocalEquiv.prod +#align local_equiv.prod PartialEquiv.prod -/ /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -#print LocalEquiv.prod_source /- +#print PartialEquiv.prod_source /- @[simp, mfld_simps] -theorem prod_source (e : LocalEquiv α β) (e' : LocalEquiv γ δ) : +theorem prod_source (e : PartialEquiv α β) (e' : PartialEquiv γ δ) : (e.Prod e').source = e.source ×ˢ e'.source := rfl -#align local_equiv.prod_source LocalEquiv.prod_source +#align local_equiv.prod_source PartialEquiv.prod_source -/ /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -#print LocalEquiv.prod_target /- +#print PartialEquiv.prod_target /- @[simp, mfld_simps] -theorem prod_target (e : LocalEquiv α β) (e' : LocalEquiv γ δ) : +theorem prod_target (e : PartialEquiv α β) (e' : PartialEquiv γ δ) : (e.Prod e').target = e.target ×ˢ e'.target := rfl -#align local_equiv.prod_target LocalEquiv.prod_target +#align local_equiv.prod_target PartialEquiv.prod_target -/ -#print LocalEquiv.prod_coe /- +#print PartialEquiv.prod_coe /- @[simp, mfld_simps] -theorem prod_coe (e : LocalEquiv α β) (e' : LocalEquiv γ δ) : +theorem prod_coe (e : PartialEquiv α β) (e' : PartialEquiv γ δ) : (e.Prod e' : α × γ → β × δ) = fun p => (e p.1, e' p.2) := rfl -#align local_equiv.prod_coe LocalEquiv.prod_coe +#align local_equiv.prod_coe PartialEquiv.prod_coe -/ -#print LocalEquiv.prod_coe_symm /- -theorem prod_coe_symm (e : LocalEquiv α β) (e' : LocalEquiv γ δ) : +#print PartialEquiv.prod_coe_symm /- +theorem prod_coe_symm (e : PartialEquiv α β) (e' : PartialEquiv γ δ) : ((e.Prod e').symm : β × δ → α × γ) = fun p => (e.symm p.1, e'.symm p.2) := rfl -#align local_equiv.prod_coe_symm LocalEquiv.prod_coe_symm +#align local_equiv.prod_coe_symm PartialEquiv.prod_coe_symm -/ -#print LocalEquiv.prod_symm /- +#print PartialEquiv.prod_symm /- @[simp, mfld_simps] -theorem prod_symm (e : LocalEquiv α β) (e' : LocalEquiv γ δ) : +theorem prod_symm (e : PartialEquiv α β) (e' : PartialEquiv γ δ) : (e.Prod e').symm = e.symm.Prod e'.symm := by ext x <;> simp [prod_coe_symm] -#align local_equiv.prod_symm LocalEquiv.prod_symm +#align local_equiv.prod_symm PartialEquiv.prod_symm -/ -#print LocalEquiv.refl_prod_refl /- +#print PartialEquiv.refl_prod_refl /- @[simp, mfld_simps] -theorem refl_prod_refl : (LocalEquiv.refl α).Prod (LocalEquiv.refl β) = LocalEquiv.refl (α × β) := - by ext1 ⟨x, y⟩; · rfl; · rintro ⟨x, y⟩; rfl; exact univ_prod_univ -#align local_equiv.refl_prod_refl LocalEquiv.refl_prod_refl +theorem refl_prod_refl : + (PartialEquiv.refl α).Prod (PartialEquiv.refl β) = PartialEquiv.refl (α × β) := by ext1 ⟨x, y⟩; + · rfl; · rintro ⟨x, y⟩; rfl; exact univ_prod_univ +#align local_equiv.refl_prod_refl PartialEquiv.refl_prod_refl -/ -#print LocalEquiv.prod_trans /- +#print PartialEquiv.prod_trans /- @[simp, mfld_simps] -theorem prod_trans {η : Type _} {ε : Type _} (e : LocalEquiv α β) (f : LocalEquiv β γ) - (e' : LocalEquiv δ η) (f' : LocalEquiv η ε) : +theorem prod_trans {η : Type _} {ε : Type _} (e : PartialEquiv α β) (f : PartialEquiv β γ) + (e' : PartialEquiv δ η) (f' : PartialEquiv η ε) : (e.Prod e').trans (f.Prod f') = (e.trans f).Prod (e'.trans f') := by ext x <;> simp [ext_iff] <;> tauto -#align local_equiv.prod_trans LocalEquiv.prod_trans +#align local_equiv.prod_trans PartialEquiv.prod_trans -/ end Prod -#print LocalEquiv.piecewise /- +#print PartialEquiv.piecewise /- /-- Combine two `local_equiv`s using `set.piecewise`. The source of the new `local_equiv` is `s.ite e.source e'.source = e.source ∩ s ∪ e'.source \ s`, and similarly for target. The function sends `e.source ∩ s` to `e.target ∩ t` using `e` and `e'.source \ s` to `e'.target \ t` using `e'`, and similarly for the inverse function. The definition assumes `e.is_image s t` and `e'.is_image s t`. -/ @[simps (config := { fullyApplied := false })] -def piecewise (e e' : LocalEquiv α β) (s : Set α) (t : Set β) [∀ x, Decidable (x ∈ s)] - [∀ y, Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t) : LocalEquiv α β +def piecewise (e e' : PartialEquiv α β) (s : Set α) (t : Set β) [∀ x, Decidable (x ∈ s)] + [∀ y, Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t) : PartialEquiv α β where toFun := s.piecewise e e' invFun := t.piecewise e.symm e'.symm @@ -1200,50 +1204,50 @@ def piecewise (e e' : LocalEquiv α β) (s : Set α) (t : Set β) [∀ x, Decida map_target' := H.symm.MapsTo.piecewise_ite H'.symm.compl.MapsTo left_inv' := H.leftInvOn_piecewise H' right_inv' := H.symm.leftInvOn_piecewise H'.symm -#align local_equiv.piecewise LocalEquiv.piecewise +#align local_equiv.piecewise PartialEquiv.piecewise -/ -#print LocalEquiv.symm_piecewise /- -theorem symm_piecewise (e e' : LocalEquiv α β) {s : Set α} {t : Set β} [∀ x, Decidable (x ∈ s)] +#print PartialEquiv.symm_piecewise /- +theorem symm_piecewise (e e' : PartialEquiv α β) {s : Set α} {t : Set β} [∀ x, Decidable (x ∈ s)] [∀ y, Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t) : (e.piecewise e' s t H H').symm = e.symm.piecewise e'.symm t s H.symm H'.symm := rfl -#align local_equiv.symm_piecewise LocalEquiv.symm_piecewise +#align local_equiv.symm_piecewise PartialEquiv.symm_piecewise -/ -#print LocalEquiv.disjointUnion /- +#print PartialEquiv.disjointUnion /- /-- Combine two `local_equiv`s with disjoint sources and disjoint targets. We reuse `local_equiv.piecewise`, then override `source` and `target` to ensure better definitional equalities. -/ @[simps (config := { fullyApplied := false })] -def disjointUnion (e e' : LocalEquiv α β) (hs : Disjoint e.source e'.source) +def disjointUnion (e e' : PartialEquiv α β) (hs : Disjoint e.source e'.source) (ht : Disjoint e.target e'.target) [∀ x, Decidable (x ∈ e.source)] - [∀ y, Decidable (y ∈ e.target)] : LocalEquiv α β := + [∀ y, Decidable (y ∈ e.target)] : PartialEquiv α β := (e.piecewise e' e.source e.target e.isImage_source_target <| e'.isImage_source_target_of_disjoint _ hs.symm ht.symm).copy _ rfl _ rfl (e.source ∪ e'.source) (ite_left _ _) (e.target ∪ e'.target) (ite_left _ _) -#align local_equiv.disjoint_union LocalEquiv.disjointUnion +#align local_equiv.disjoint_union PartialEquiv.disjointUnion -/ -#print LocalEquiv.disjointUnion_eq_piecewise /- -theorem disjointUnion_eq_piecewise (e e' : LocalEquiv α β) (hs : Disjoint e.source e'.source) +#print PartialEquiv.disjointUnion_eq_piecewise /- +theorem disjointUnion_eq_piecewise (e e' : PartialEquiv α β) (hs : Disjoint e.source e'.source) (ht : Disjoint e.target e'.target) [∀ x, Decidable (x ∈ e.source)] [∀ y, Decidable (y ∈ e.target)] : e.disjointUnion e' hs ht = e.piecewise e' e.source e.target e.isImage_source_target (e'.isImage_source_target_of_disjoint _ hs.symm ht.symm) := copy_eq _ _ _ _ _ _ _ _ _ -#align local_equiv.disjoint_union_eq_piecewise LocalEquiv.disjointUnion_eq_piecewise +#align local_equiv.disjoint_union_eq_piecewise PartialEquiv.disjointUnion_eq_piecewise -/ section Pi -variable {ι : Type _} {αi βi : ι → Type _} (ei : ∀ i, LocalEquiv (αi i) (βi i)) +variable {ι : Type _} {αi βi : ι → Type _} (ei : ∀ i, PartialEquiv (αi i) (βi i)) -#print LocalEquiv.pi /- +#print PartialEquiv.pi /- /-- The product of a family of local equivs, as a local equiv on the pi type. -/ @[simps (config := mfld_cfg)] -protected def pi : LocalEquiv (∀ i, αi i) (∀ i, βi i) +protected def pi : PartialEquiv (∀ i, αi i) (∀ i, βi i) where toFun f i := ei i (f i) invFun f i := (ei i).symm (f i) @@ -1253,22 +1257,23 @@ protected def pi : LocalEquiv (∀ i, αi i) (∀ i, βi i) map_target' f hf i hi := (ei i).map_target (hf i hi) left_inv' f hf := funext fun i => (ei i).left_inv (hf i trivial) right_inv' f hf := funext fun i => (ei i).right_inv (hf i trivial) -#align local_equiv.pi LocalEquiv.pi +#align local_equiv.pi PartialEquiv.pi -/ end Pi -end LocalEquiv +end PartialEquiv namespace Set -#print Set.BijOn.toLocalEquiv /- +#print Set.BijOn.toPartialEquiv /- -- All arguments are explicit to avoid missing information in the pretty printer output /-- A bijection between two sets `s : set α` and `t : set β` provides a local equivalence between `α` and `β`. -/ @[simps (config := { fullyApplied := false })] -noncomputable def BijOn.toLocalEquiv [Nonempty α] (f : α → β) (s : Set α) (t : Set β) - (hf : BijOn f s t) : LocalEquiv α β where +noncomputable def BijOn.toPartialEquiv [Nonempty α] (f : α → β) (s : Set α) (t : Set β) + (hf : BijOn f s t) : PartialEquiv α β + where toFun := f invFun := invFunOn f s source := s @@ -1277,16 +1282,16 @@ noncomputable def BijOn.toLocalEquiv [Nonempty α] (f : α → β) (s : Set α) map_target' := hf.SurjOn.mapsTo_invFunOn left_inv' := hf.invOn_invFunOn.1 right_inv' := hf.invOn_invFunOn.2 -#align set.bij_on.to_local_equiv Set.BijOn.toLocalEquiv +#align set.bij_on.to_local_equiv Set.BijOn.toPartialEquiv -/ -#print Set.InjOn.toLocalEquiv /- +#print Set.InjOn.toPartialEquiv /- /-- A map injective on a subset of its domain provides a local equivalence. -/ @[simp, mfld_simps] -noncomputable def InjOn.toLocalEquiv [Nonempty α] (f : α → β) (s : Set α) (hf : InjOn f s) : - LocalEquiv α β := - hf.bijOn_image.toLocalEquiv f s (f '' s) -#align set.inj_on.to_local_equiv Set.InjOn.toLocalEquiv +noncomputable def InjOn.toPartialEquiv [Nonempty α] (f : α → β) (s : Set α) (hf : InjOn f s) : + PartialEquiv α β := + hf.bijOn_image.toPartialEquiv f s (f '' s) +#align set.inj_on.to_local_equiv Set.InjOn.toPartialEquiv -/ end Set @@ -1297,26 +1302,27 @@ namespace Equiv equiv to that of the equiv. -/ variable (e : α ≃ β) (e' : β ≃ γ) -#print Equiv.refl_toLocalEquiv /- +#print Equiv.refl_toPartialEquiv /- @[simp, mfld_simps] -theorem refl_toLocalEquiv : (Equiv.refl α).toLocalEquiv = LocalEquiv.refl α := +theorem refl_toPartialEquiv : (Equiv.refl α).toPartialEquiv = PartialEquiv.refl α := rfl -#align equiv.refl_to_local_equiv Equiv.refl_toLocalEquiv +#align equiv.refl_to_local_equiv Equiv.refl_toPartialEquiv -/ -#print Equiv.symm_toLocalEquiv /- +#print Equiv.symm_toPartialEquiv /- @[simp, mfld_simps] -theorem symm_toLocalEquiv : e.symm.toLocalEquiv = e.toLocalEquiv.symm := +theorem symm_toPartialEquiv : e.symm.toPartialEquiv = e.toPartialEquiv.symm := rfl -#align equiv.symm_to_local_equiv Equiv.symm_toLocalEquiv +#align equiv.symm_to_local_equiv Equiv.symm_toPartialEquiv -/ -#print Equiv.trans_toLocalEquiv /- +#print Equiv.trans_toPartialEquiv /- @[simp, mfld_simps] -theorem trans_toLocalEquiv : (e.trans e').toLocalEquiv = e.toLocalEquiv.trans e'.toLocalEquiv := - LocalEquiv.ext (fun x => rfl) (fun x => rfl) - (by simp [LocalEquiv.trans_source, Equiv.toLocalEquiv]) -#align equiv.trans_to_local_equiv Equiv.trans_toLocalEquiv +theorem trans_toPartialEquiv : + (e.trans e').toPartialEquiv = e.toPartialEquiv.trans e'.toPartialEquiv := + PartialEquiv.ext (fun x => rfl) (fun x => rfl) + (by simp [PartialEquiv.trans_source, Equiv.toPartialEquiv]) +#align equiv.trans_to_local_equiv Equiv.trans_toPartialEquiv -/ end Equiv diff --git a/Mathbin/MeasureTheory/Function/Jacobian.lean b/Mathbin/MeasureTheory/Function/Jacobian.lean index 10c96ea543..389e342bf0 100644 --- a/Mathbin/MeasureTheory/Function/Jacobian.lean +++ b/Mathbin/MeasureTheory/Function/Jacobian.lean @@ -1407,7 +1407,7 @@ theorem integral_target_eq_integral_abs_det_fderiv_smul [CompleteSpace F] {f : PartialHomeomorph E E} (hf' : ∀ x ∈ f.source, HasFDerivAt f (f' x) x) (g : E → F) : ∫ x in f.target, g x ∂μ = ∫ x in f.source, |(f' x).det| • g (f x) ∂μ := by - have : f '' f.source = f.target := LocalEquiv.image_source_eq_target f.to_local_equiv + have : f '' f.source = f.target := PartialEquiv.image_source_eq_target f.to_local_equiv rw [← this] apply integral_image_eq_integral_abs_det_fderiv_smul μ f.open_source.measurable_set _ f.inj_on intro x hx diff --git a/Mathbin/MeasureTheory/Function/UniformIntegrable.lean b/Mathbin/MeasureTheory/Function/UniformIntegrable.lean index c7253d33fa..43a50834b9 100644 --- a/Mathbin/MeasureTheory/Function/UniformIntegrable.lean +++ b/Mathbin/MeasureTheory/Function/UniformIntegrable.lean @@ -1123,7 +1123,7 @@ theorem uniformIntegrable_average_real (hp : 1 ≤ p) {f : ℕ → α → ℝ} ( (ae_strongly_measurable_const : ae_strongly_measurable (fun x => (↑n : ℝ)⁻¹) μ) · obtain ⟨δ, hδ₁, hδ₂⟩ := hf₂ hε refine' ⟨δ, hδ₁, fun n s hs hle => _⟩ - simp_rw [div_eq_mul_inv, Finset.sum_mul, Set.indicator_finset_sum] + simp_rw [div_eq_mul_inv, Finset.sum_mul, Finset.indicator_sum] refine' le_trans (snorm_sum_le (fun i hi => ((hf₁ i).mul_const (↑n)⁻¹).indicator hs) hp) _ have : ∀ i, s.indicator (f i * (↑n)⁻¹) = (↑n : ℝ)⁻¹ • s.indicator (f i) := by diff --git a/Mathbin/Probability/Martingale/Upcrossing.lean b/Mathbin/Probability/Martingale/Upcrossing.lean index 3aafbb41f1..da6ef97fe5 100644 --- a/Mathbin/Probability/Martingale/Upcrossing.lean +++ b/Mathbin/Probability/Martingale/Upcrossing.lean @@ -475,7 +475,7 @@ theorem upcrossingStrat_nonneg : 0 ≤ upcrossingStrat a b f N n ω := #print MeasureTheory.upcrossingStrat_le_one /- theorem upcrossingStrat_le_one : upcrossingStrat a b f N n ω ≤ 1 := by - rw [upcrossing_strat, ← Set.indicator_finset_biUnion_apply] + rw [upcrossing_strat, ← Finset.indicator_biUnion_apply] · exact Set.indicator_le_self' (fun _ _ => zero_le_one) _ · intro i hi j hj hij rw [Set.Ico_disjoint_Ico] diff --git a/Mathbin/Topology/Algebra/InfiniteSum/Basic.lean b/Mathbin/Topology/Algebra/InfiniteSum/Basic.lean index 0a68081fbf..1be7c6e530 100644 --- a/Mathbin/Topology/Algebra/InfiniteSum/Basic.lean +++ b/Mathbin/Topology/Algebra/InfiniteSum/Basic.lean @@ -434,7 +434,7 @@ theorem hasSum_sum_disjoint {ι} (s : Finset ι) {t : ι → Set β} {a : ι → HasSum (f ∘ coe : (⋃ i ∈ s, t i) → α) (∑ i in s, a i) := by simp_rw [hasSum_subtype_iff_indicator] at * - rw [Set.indicator_finset_biUnion _ _ hs] + rw [Finset.indicator_biUnion _ _ hs] exact hasSum_sum hf #align has_sum_sum_disjoint hasSum_sum_disjoint -/ diff --git a/Mathbin/Topology/Covering.lean b/Mathbin/Topology/Covering.lean index 74fd2ea854..469ba6955e 100644 --- a/Mathbin/Topology/Covering.lean +++ b/Mathbin/Topology/Covering.lean @@ -65,7 +65,7 @@ theorem toTrivialization_apply {x : E} {I : Type _} [TopologicalSpace I] let h := Classical.choose_spec h.2 let he := e.mk_proj_snd' h Subtype.ext - ((e.toLocalEquiv.eq_symm_apply (e.mem_source.mpr h) + ((e.toPartialEquiv.eq_symm_apply (e.mem_source.mpr h) (by rwa [he, e.mem_target, e.coe_fst (e.mem_source.mpr h)])).mpr he.symm).symm #align is_evenly_covered.to_trivialization_apply IsEvenlyCovered.toTrivialization_apply diff --git a/Mathbin/Topology/FiberBundle/Basic.lean b/Mathbin/Topology/FiberBundle/Basic.lean index 18b4b521aa..fab7f9297f 100644 --- a/Mathbin/Topology/FiberBundle/Basic.lean +++ b/Mathbin/Topology/FiberBundle/Basic.lean @@ -531,7 +531,7 @@ theorem mem_trivChange_source (i j : ι) (p : B × F) : -/ /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -#print FiberBundleCore.localTrivAsLocalEquiv /- +#print FiberBundleCore.localTrivAsPartialEquiv /- /-- Associate to a trivialization index `i : ι` the corresponding trivialization, i.e., a bijection between `proj ⁻¹ (base_set i)` and `base_set i × F`. As the fiber above `x` is `F` but read in the chart with index `index_at x`, the trivialization in the fiber above x is by definition the @@ -540,7 +540,7 @@ The local trivialization will ultimately be a local homeomorphism. For now, we o local equiv version, denoted with a prime. In further developments, avoid this auxiliary version, and use `Z.local_triv` instead. -/ -def localTrivAsLocalEquiv (i : ι) : LocalEquiv Z.TotalSpace (B × F) +def localTrivAsPartialEquiv (i : ι) : PartialEquiv Z.TotalSpace (B × F) where source := Z.proj ⁻¹' Z.baseSet i target := Z.baseSet i ×ˢ univ @@ -563,47 +563,47 @@ def localTrivAsLocalEquiv (i : ι) : LocalEquiv Z.TotalSpace (B × F) rw [Z.coord_change_comp, Z.coord_change_self] · exact hx · simp only [hx, mem_inter_iff, and_self_iff, mem_base_set_at] -#align fiber_bundle_core.local_triv_as_local_equiv FiberBundleCore.localTrivAsLocalEquiv +#align fiber_bundle_core.local_triv_as_local_equiv FiberBundleCore.localTrivAsPartialEquiv -/ variable (i : ι) -#print FiberBundleCore.mem_localTrivAsLocalEquiv_source /- -theorem mem_localTrivAsLocalEquiv_source (p : Z.TotalSpace) : - p ∈ (Z.localTrivAsLocalEquiv i).source ↔ p.1 ∈ Z.baseSet i := +#print FiberBundleCore.mem_localTrivAsPartialEquiv_source /- +theorem mem_localTrivAsPartialEquiv_source (p : Z.TotalSpace) : + p ∈ (Z.localTrivAsPartialEquiv i).source ↔ p.1 ∈ Z.baseSet i := Iff.rfl -#align fiber_bundle_core.mem_local_triv_as_local_equiv_source FiberBundleCore.mem_localTrivAsLocalEquiv_source +#align fiber_bundle_core.mem_local_triv_as_local_equiv_source FiberBundleCore.mem_localTrivAsPartialEquiv_source -/ -#print FiberBundleCore.mem_localTrivAsLocalEquiv_target /- -theorem mem_localTrivAsLocalEquiv_target (p : B × F) : - p ∈ (Z.localTrivAsLocalEquiv i).target ↔ p.1 ∈ Z.baseSet i := by erw [mem_prod]; +#print FiberBundleCore.mem_localTrivAsPartialEquiv_target /- +theorem mem_localTrivAsPartialEquiv_target (p : B × F) : + p ∈ (Z.localTrivAsPartialEquiv i).target ↔ p.1 ∈ Z.baseSet i := by erw [mem_prod]; simp only [and_true_iff, mem_univ] -#align fiber_bundle_core.mem_local_triv_as_local_equiv_target FiberBundleCore.mem_localTrivAsLocalEquiv_target +#align fiber_bundle_core.mem_local_triv_as_local_equiv_target FiberBundleCore.mem_localTrivAsPartialEquiv_target -/ -#print FiberBundleCore.localTrivAsLocalEquiv_apply /- -theorem localTrivAsLocalEquiv_apply (p : Z.TotalSpace) : - (Z.localTrivAsLocalEquiv i) p = ⟨p.1, Z.coordChange (Z.indexAt p.1) i p.1 p.2⟩ := +#print FiberBundleCore.localTrivAsPartialEquiv_apply /- +theorem localTrivAsPartialEquiv_apply (p : Z.TotalSpace) : + (Z.localTrivAsPartialEquiv i) p = ⟨p.1, Z.coordChange (Z.indexAt p.1) i p.1 p.2⟩ := rfl -#align fiber_bundle_core.local_triv_as_local_equiv_apply FiberBundleCore.localTrivAsLocalEquiv_apply +#align fiber_bundle_core.local_triv_as_local_equiv_apply FiberBundleCore.localTrivAsPartialEquiv_apply -/ -#print FiberBundleCore.localTrivAsLocalEquiv_trans /- +#print FiberBundleCore.localTrivAsPartialEquiv_trans /- /-- The composition of two local trivializations is the trivialization change Z.triv_change i j. -/ -theorem localTrivAsLocalEquiv_trans (i j : ι) : - (Z.localTrivAsLocalEquiv i).symm.trans (Z.localTrivAsLocalEquiv j) ≈ - (Z.trivChange i j).toLocalEquiv := +theorem localTrivAsPartialEquiv_trans (i j : ι) : + (Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j) ≈ + (Z.trivChange i j).toPartialEquiv := by constructor · ext x; simp only [mem_local_triv_as_local_equiv_target, mfld_simps]; rfl · rintro ⟨x, v⟩ hx - simp only [triv_change, local_triv_as_local_equiv, LocalEquiv.symm, true_and_iff, - Prod.mk.inj_iff, prod_mk_mem_set_prod_eq, LocalEquiv.trans_source, mem_inter_iff, - and_true_iff, mem_preimage, proj, mem_univ, LocalEquiv.coe_mk, eq_self_iff_true, - LocalEquiv.coe_trans, total_space.proj] at hx ⊢ + simp only [triv_change, local_triv_as_local_equiv, PartialEquiv.symm, true_and_iff, + Prod.mk.inj_iff, prod_mk_mem_set_prod_eq, PartialEquiv.trans_source, mem_inter_iff, + and_true_iff, mem_preimage, proj, mem_univ, PartialEquiv.coe_mk, eq_self_iff_true, + PartialEquiv.coe_trans, total_space.proj] at hx ⊢ simp only [Z.coord_change_comp, hx, mem_inter_iff, and_self_iff, mem_base_set_at] -#align fiber_bundle_core.local_triv_as_local_equiv_trans FiberBundleCore.localTrivAsLocalEquiv_trans +#align fiber_bundle_core.local_triv_as_local_equiv_trans FiberBundleCore.localTrivAsPartialEquiv_trans -/ #print FiberBundleCore.toTopologicalSpace /- @@ -619,7 +619,7 @@ variable (b : B) (a : F) /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ #print FiberBundleCore.open_source' /- -theorem open_source' (i : ι) : IsOpen (Z.localTrivAsLocalEquiv i).source := +theorem open_source' (i : ι) : IsOpen (Z.localTrivAsPartialEquiv i).source := by apply TopologicalSpace.GenerateOpen.basic simp only [exists_prop, mem_Union, mem_singleton_iff] @@ -659,7 +659,7 @@ def localTriv (i : ι) : Trivialization F Z.proj t = (local_triv_as_local_equiv Z j).source ∩ local_triv_as_local_equiv Z j ⁻¹' s := ht rw [ts] - simp only [LocalEquiv.right_inv, preimage_inter, LocalEquiv.left_inv] + simp only [PartialEquiv.right_inv, preimage_inter, PartialEquiv.left_inv] let e := Z.local_triv_as_local_equiv i let e' := Z.local_triv_as_local_equiv j let f := e.symm.trans e' @@ -670,10 +670,10 @@ def localTriv (i : ι) : Trivialization F Z.proj (continuousOn_open_iff (Z.triv_change i j).open_source).1 (Z.triv_change i j).ContinuousOn _ s_open convert this using 1 - dsimp [LocalEquiv.trans_source] + dsimp [PartialEquiv.trans_source] rw [← preimage_comp, inter_assoc] rfl - toLocalEquiv := Z.localTrivAsLocalEquiv i + toPartialEquiv := Z.localTrivAsPartialEquiv i #align fiber_bundle_core.local_triv FiberBundleCore.localTriv -/ @@ -715,35 +715,35 @@ theorem continuous_const_section (v : F) #align fiber_bundle_core.continuous_const_section FiberBundleCore.continuous_const_section -/ -#print FiberBundleCore.localTrivAsLocalEquiv_coe /- +#print FiberBundleCore.localTrivAsPartialEquiv_coe /- @[simp, mfld_simps] -theorem localTrivAsLocalEquiv_coe : ⇑(Z.localTrivAsLocalEquiv i) = Z.localTriv i := +theorem localTrivAsPartialEquiv_coe : ⇑(Z.localTrivAsPartialEquiv i) = Z.localTriv i := rfl -#align fiber_bundle_core.local_triv_as_local_equiv_coe FiberBundleCore.localTrivAsLocalEquiv_coe +#align fiber_bundle_core.local_triv_as_local_equiv_coe FiberBundleCore.localTrivAsPartialEquiv_coe -/ -#print FiberBundleCore.localTrivAsLocalEquiv_source /- +#print FiberBundleCore.localTrivAsPartialEquiv_source /- @[simp, mfld_simps] -theorem localTrivAsLocalEquiv_source : - (Z.localTrivAsLocalEquiv i).source = (Z.localTriv i).source := +theorem localTrivAsPartialEquiv_source : + (Z.localTrivAsPartialEquiv i).source = (Z.localTriv i).source := rfl -#align fiber_bundle_core.local_triv_as_local_equiv_source FiberBundleCore.localTrivAsLocalEquiv_source +#align fiber_bundle_core.local_triv_as_local_equiv_source FiberBundleCore.localTrivAsPartialEquiv_source -/ -#print FiberBundleCore.localTrivAsLocalEquiv_target /- +#print FiberBundleCore.localTrivAsPartialEquiv_target /- @[simp, mfld_simps] -theorem localTrivAsLocalEquiv_target : - (Z.localTrivAsLocalEquiv i).target = (Z.localTriv i).target := +theorem localTrivAsPartialEquiv_target : + (Z.localTrivAsPartialEquiv i).target = (Z.localTriv i).target := rfl -#align fiber_bundle_core.local_triv_as_local_equiv_target FiberBundleCore.localTrivAsLocalEquiv_target +#align fiber_bundle_core.local_triv_as_local_equiv_target FiberBundleCore.localTrivAsPartialEquiv_target -/ -#print FiberBundleCore.localTrivAsLocalEquiv_symm /- +#print FiberBundleCore.localTrivAsPartialEquiv_symm /- @[simp, mfld_simps] -theorem localTrivAsLocalEquiv_symm : - (Z.localTrivAsLocalEquiv i).symm = (Z.localTriv i).toLocalEquiv.symm := +theorem localTrivAsPartialEquiv_symm : + (Z.localTrivAsPartialEquiv i).symm = (Z.localTriv i).toPartialEquiv.symm := rfl -#align fiber_bundle_core.local_triv_as_local_equiv_symm FiberBundleCore.localTrivAsLocalEquiv_symm +#align fiber_bundle_core.local_triv_as_local_equiv_symm FiberBundleCore.localTrivAsPartialEquiv_symm -/ #print FiberBundleCore.baseSet_at /- @@ -926,7 +926,7 @@ structure FiberPrebundle where pretrivialization_mem_atlas : ∀ x : B, pretrivialization_at x ∈ pretrivialization_atlas continuous_triv_change : ∀ (e) (_ : e ∈ pretrivialization_atlas) (e') (_ : e' ∈ pretrivialization_atlas), - ContinuousOn (e ∘ e'.toLocalEquiv.symm) (e'.target ∩ e'.toLocalEquiv.symm ⁻¹' e.source) + ContinuousOn (e ∘ e'.toPartialEquiv.symm) (e'.target ∩ e'.toPartialEquiv.symm ⁻¹' e.source) totalSpace_mk_inducing : ∀ b : B, Inducing (pretrivialization_at b ∘ TotalSpace.mk b) #align fiber_prebundle FiberPrebundle -/ @@ -945,7 +945,7 @@ def totalSpaceTopology (a : FiberPrebundle F E) : TopologicalSpace (TotalSpace F #print FiberPrebundle.continuous_symm_of_mem_pretrivializationAtlas /- theorem continuous_symm_of_mem_pretrivializationAtlas (he : e ∈ a.pretrivializationAtlas) : - @ContinuousOn _ _ _ a.totalSpaceTopology e.toLocalEquiv.symm e.target := + @ContinuousOn _ _ _ a.totalSpaceTopology e.toPartialEquiv.symm e.target := by refine' id fun z H => @@ -970,7 +970,7 @@ theorem isOpen_source (e : Pretrivialization F (π F E)) : is_open[a.totalSpaceT #print FiberPrebundle.isOpen_target_of_mem_pretrivializationAtlas_inter /- theorem isOpen_target_of_mem_pretrivializationAtlas_inter (e e' : Pretrivialization F (π F E)) (he' : e' ∈ a.pretrivializationAtlas) : - IsOpen (e'.toLocalEquiv.target ∩ e'.toLocalEquiv.symm ⁻¹' e.source) := + IsOpen (e'.toPartialEquiv.target ∩ e'.toPartialEquiv.symm ⁻¹' e.source) := by letI := a.total_space_topology obtain ⟨u, hu1, hu2⟩ := @@ -1100,7 +1100,7 @@ theorem continuousOn_of_comp_right {X : Type _} [TopologicalSpace X] {f : TotalS {s : Set B} (hs : IsOpen s) (hf : ∀ b ∈ s, - ContinuousOn (f ∘ (a.pretrivializationAt b).toLocalEquiv.symm) + ContinuousOn (f ∘ (a.pretrivializationAt b).toPartialEquiv.symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ (Set.univ : Set F))) : @ContinuousOn _ _ a.totalSpaceTopology _ f (π F E ⁻¹' s) := by diff --git a/Mathbin/Topology/FiberBundle/Constructions.lean b/Mathbin/Topology/FiberBundle/Constructions.lean index dabdebdc02..944087a0be 100644 --- a/Mathbin/Topology/FiberBundle/Constructions.lean +++ b/Mathbin/Topology/FiberBundle/Constructions.lean @@ -298,7 +298,7 @@ theorem baseSet_prod : (prod e₁ e₂).baseSet = e₁.baseSet ∩ e₂.baseSet #print Trivialization.prod_symm_apply /- theorem prod_symm_apply (x : B) (w₁ : F₁) (w₂ : F₂) : - (prod e₁ e₂).toLocalEquiv.symm (x, w₁, w₂) = ⟨x, e₁.symm x w₁, e₂.symm x w₂⟩ := + (prod e₁ e₂).toPartialEquiv.symm (x, w₁, w₂) = ⟨x, e₁.symm x w₁, e₂.symm x w₂⟩ := rfl #align trivialization.prod_symm_apply Trivialization.prod_symm_apply -/ diff --git a/Mathbin/Topology/FiberBundle/Trivialization.lean b/Mathbin/Topology/FiberBundle/Trivialization.lean index 9aa1fa3761..6ce56d104e 100644 --- a/Mathbin/Topology/FiberBundle/Trivialization.lean +++ b/Mathbin/Topology/FiberBundle/Trivialization.lean @@ -69,7 +69,7 @@ have a topology on both the fiber and the base space. Through the construction `topological_fiber_prebundle F proj` it will be possible to promote a `pretrivialization F proj` to a `trivialization F proj`. -/ @[ext, nolint has_nonempty_instance] -structure Pretrivialization (proj : Z → B) extends LocalEquiv Z (B × F) where +structure Pretrivialization (proj : Z → B) extends PartialEquiv Z (B × F) where open_target : IsOpen target baseSet : Set B open_baseSet : IsOpen base_set @@ -88,7 +88,7 @@ variable {F} (e : Pretrivialization F proj) {x : Z} #print Pretrivialization.coe_coe /- @[simp, mfld_simps] -theorem coe_coe : ⇑e.toLocalEquiv = e := +theorem coe_coe : ⇑e.toPartialEquiv = e := rfl #align pretrivialization.coe_coe Pretrivialization.coe_coe -/ @@ -131,7 +131,7 @@ theorem mk_proj_snd' (ex : proj x ∈ e.baseSet) : (proj x, (e x).2) = e x := #print Pretrivialization.setSymm /- /-- Composition of inverse and coercion from the subtype of the target. -/ def setSymm : e.target → Z := - e.target.restrict e.toLocalEquiv.symm + e.target.restrict e.toPartialEquiv.symm #align pretrivialization.set_symm Pretrivialization.setSymm -/ @@ -142,7 +142,7 @@ theorem mem_target {x : B × F} : x ∈ e.target ↔ x.1 ∈ e.baseSet := by -/ #print Pretrivialization.proj_symm_apply /- -theorem proj_symm_apply {x : B × F} (hx : x ∈ e.target) : proj (e.toLocalEquiv.symm x) = x.1 := +theorem proj_symm_apply {x : B × F} (hx : x ∈ e.target) : proj (e.toPartialEquiv.symm x) = x.1 := by have := (e.coe_fst (e.to_local_equiv.map_target hx)).symm rwa [← e.coe_coe, e.to_local_equiv.right_inv hx] at this @@ -151,7 +151,7 @@ theorem proj_symm_apply {x : B × F} (hx : x ∈ e.target) : proj (e.toLocalEqui #print Pretrivialization.proj_symm_apply' /- theorem proj_symm_apply' {b : B} {x : F} (hx : b ∈ e.baseSet) : - proj (e.toLocalEquiv.symm (b, x)) = b := + proj (e.toPartialEquiv.symm (b, x)) = b := e.proj_symm_apply (e.mem_target.2 hx) #align pretrivialization.proj_symm_apply' Pretrivialization.proj_symm_apply' -/ @@ -159,34 +159,34 @@ theorem proj_symm_apply' {b : B} {x : F} (hx : b ∈ e.baseSet) : #print Pretrivialization.proj_surjOn_baseSet /- theorem proj_surjOn_baseSet [Nonempty F] : Set.SurjOn proj e.source e.baseSet := fun b hb => let ⟨y⟩ := ‹Nonempty F› - ⟨e.toLocalEquiv.symm (b, y), e.toLocalEquiv.map_target <| e.mem_target.2 hb, + ⟨e.toPartialEquiv.symm (b, y), e.toPartialEquiv.map_target <| e.mem_target.2 hb, e.proj_symm_apply' hb⟩ #align pretrivialization.proj_surj_on_base_set Pretrivialization.proj_surjOn_baseSet -/ #print Pretrivialization.apply_symm_apply /- -theorem apply_symm_apply {x : B × F} (hx : x ∈ e.target) : e (e.toLocalEquiv.symm x) = x := - e.toLocalEquiv.right_inv hx +theorem apply_symm_apply {x : B × F} (hx : x ∈ e.target) : e (e.toPartialEquiv.symm x) = x := + e.toPartialEquiv.right_inv hx #align pretrivialization.apply_symm_apply Pretrivialization.apply_symm_apply -/ #print Pretrivialization.apply_symm_apply' /- theorem apply_symm_apply' {b : B} {x : F} (hx : b ∈ e.baseSet) : - e (e.toLocalEquiv.symm (b, x)) = (b, x) := + e (e.toPartialEquiv.symm (b, x)) = (b, x) := e.apply_symm_apply (e.mem_target.2 hx) #align pretrivialization.apply_symm_apply' Pretrivialization.apply_symm_apply' -/ #print Pretrivialization.symm_apply_apply /- -theorem symm_apply_apply {x : Z} (hx : x ∈ e.source) : e.toLocalEquiv.symm (e x) = x := - e.toLocalEquiv.left_inv hx +theorem symm_apply_apply {x : Z} (hx : x ∈ e.source) : e.toPartialEquiv.symm (e x) = x := + e.toPartialEquiv.left_inv hx #align pretrivialization.symm_apply_apply Pretrivialization.symm_apply_apply -/ #print Pretrivialization.symm_apply_mk_proj /- @[simp, mfld_simps] theorem symm_apply_mk_proj {x : Z} (ex : x ∈ e.source) : - e.toLocalEquiv.symm (proj x, (e x).2) = x := by + e.toPartialEquiv.symm (proj x, (e x).2) = x := by rw [← e.coe_fst ex, Prod.mk.eta, ← e.coe_coe, e.to_local_equiv.left_inv ex] #align pretrivialization.symm_apply_mk_proj Pretrivialization.symm_apply_mk_proj -/ @@ -194,10 +194,10 @@ theorem symm_apply_mk_proj {x : Z} (ex : x ∈ e.source) : #print Pretrivialization.preimage_symm_proj_baseSet /- @[simp, mfld_simps] theorem preimage_symm_proj_baseSet : - e.toLocalEquiv.symm ⁻¹' (proj ⁻¹' e.baseSet) ∩ e.target = e.target := + e.toPartialEquiv.symm ⁻¹' (proj ⁻¹' e.baseSet) ∩ e.target = e.target := by refine' inter_eq_right_iff_subset.mpr fun x hx => _ - simp only [mem_preimage, LocalEquiv.invFun_as_coe, e.proj_symm_apply hx] + simp only [mem_preimage, PartialEquiv.invFun_as_coe, e.proj_symm_apply hx] exact e.mem_target.mp hx #align pretrivialization.preimage_symm_proj_base_set Pretrivialization.preimage_symm_proj_baseSet -/ @@ -207,7 +207,7 @@ theorem preimage_symm_proj_baseSet : #print Pretrivialization.preimage_symm_proj_inter /- @[simp, mfld_simps] theorem preimage_symm_proj_inter (s : Set B) : - e.toLocalEquiv.symm ⁻¹' (proj ⁻¹' s) ∩ e.baseSet ×ˢ univ = (s ∩ e.baseSet) ×ˢ univ := + e.toPartialEquiv.symm ⁻¹' (proj ⁻¹' s) ∩ e.baseSet ×ˢ univ = (s ∩ e.baseSet) ×ˢ univ := by ext ⟨x, y⟩ suffices x ∈ e.base_set → (proj (e.to_local_equiv.symm (x, y)) ∈ s ↔ x ∈ s) by @@ -220,7 +220,7 @@ theorem preimage_symm_proj_inter (s : Set B) : /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ #print Pretrivialization.target_inter_preimage_symm_source_eq /- theorem target_inter_preimage_symm_source_eq (e f : Pretrivialization F proj) : - f.target ∩ f.toLocalEquiv.symm ⁻¹' e.source = (e.baseSet ∩ f.baseSet) ×ˢ univ := by + f.target ∩ f.toPartialEquiv.symm ⁻¹' e.source = (e.baseSet ∩ f.baseSet) ×ˢ univ := by rw [inter_comm, f.target_eq, e.source_eq, f.preimage_symm_proj_inter] #align pretrivialization.target_inter_preimage_symm_source_eq Pretrivialization.target_inter_preimage_symm_source_eq -/ @@ -228,23 +228,24 @@ theorem target_inter_preimage_symm_source_eq (e f : Pretrivialization F proj) : /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ #print Pretrivialization.trans_source /- theorem trans_source (e f : Pretrivialization F proj) : - (f.toLocalEquiv.symm.trans e.toLocalEquiv).source = (e.baseSet ∩ f.baseSet) ×ˢ univ := by - rw [LocalEquiv.trans_source, LocalEquiv.symm_source, e.target_inter_preimage_symm_source_eq] + (f.toPartialEquiv.symm.trans e.toPartialEquiv).source = (e.baseSet ∩ f.baseSet) ×ˢ univ := by + rw [PartialEquiv.trans_source, PartialEquiv.symm_source, e.target_inter_preimage_symm_source_eq] #align pretrivialization.trans_source Pretrivialization.trans_source -/ #print Pretrivialization.symm_trans_symm /- theorem symm_trans_symm (e e' : Pretrivialization F proj) : - (e.toLocalEquiv.symm.trans e'.toLocalEquiv).symm = e'.toLocalEquiv.symm.trans e.toLocalEquiv := - by rw [LocalEquiv.trans_symm_eq_symm_trans_symm, LocalEquiv.symm_symm] + (e.toPartialEquiv.symm.trans e'.toPartialEquiv).symm = + e'.toPartialEquiv.symm.trans e.toPartialEquiv := + by rw [PartialEquiv.trans_symm_eq_symm_trans_symm, PartialEquiv.symm_symm] #align pretrivialization.symm_trans_symm Pretrivialization.symm_trans_symm -/ /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ #print Pretrivialization.symm_trans_source_eq /- theorem symm_trans_source_eq (e e' : Pretrivialization F proj) : - (e.toLocalEquiv.symm.trans e'.toLocalEquiv).source = (e.baseSet ∩ e'.baseSet) ×ˢ univ := by - rw [LocalEquiv.trans_source, e'.source_eq, LocalEquiv.symm_source, e.target_eq, inter_comm, + (e.toPartialEquiv.symm.trans e'.toPartialEquiv).source = (e.baseSet ∩ e'.baseSet) ×ˢ univ := by + rw [PartialEquiv.trans_source, e'.source_eq, PartialEquiv.symm_source, e.target_eq, inter_comm, e.preimage_symm_proj_inter, inter_comm] #align pretrivialization.symm_trans_source_eq Pretrivialization.symm_trans_source_eq -/ @@ -252,8 +253,8 @@ theorem symm_trans_source_eq (e e' : Pretrivialization F proj) : /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ #print Pretrivialization.symm_trans_target_eq /- theorem symm_trans_target_eq (e e' : Pretrivialization F proj) : - (e.toLocalEquiv.symm.trans e'.toLocalEquiv).target = (e.baseSet ∩ e'.baseSet) ×ˢ univ := by - rw [← LocalEquiv.symm_source, symm_trans_symm, symm_trans_source_eq, inter_comm] + (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] #align pretrivialization.symm_trans_target_eq Pretrivialization.symm_trans_target_eq -/ @@ -281,7 +282,7 @@ theorem mk_mem_target {x : B} {y : F} : (x, y) ∈ e'.target ↔ x ∈ e'.baseSe #print Pretrivialization.symm_coe_proj /- theorem symm_coe_proj {x : B} {y : F} (e' : Pretrivialization F (π F E)) (h : x ∈ e'.baseSet) : - (e'.toLocalEquiv.symm (x, y)).1 = x := + (e'.toPartialEquiv.symm (x, y)).1 = x := e'.proj_symm_apply' h #align pretrivialization.symm_coe_proj Pretrivialization.symm_coe_proj -/ @@ -295,14 +296,14 @@ variable [∀ x, Zero (E x)] `B × F → total_space F E` of `e` on `e.base_set`. It is defined to be `0` outside `e.base_set`. -/ protected noncomputable def symm (e : Pretrivialization F (π F E)) (b : B) (y : F) : E b := if hb : b ∈ e.baseSet then - cast (congr_arg E (e.proj_symm_apply' hb)) (e.toLocalEquiv.symm (b, y)).2 + cast (congr_arg E (e.proj_symm_apply' hb)) (e.toPartialEquiv.symm (b, y)).2 else 0 #align pretrivialization.symm Pretrivialization.symm -/ #print Pretrivialization.symm_apply /- theorem symm_apply (e : Pretrivialization F (π F E)) {b : B} (hb : b ∈ e.baseSet) (y : F) : - e.symm b y = cast (congr_arg E (e.symm_coe_proj hb)) (e.toLocalEquiv.symm (b, y)).2 := + e.symm b y = cast (congr_arg E (e.symm_coe_proj hb)) (e.toPartialEquiv.symm (b, y)).2 := dif_pos hb #align pretrivialization.symm_apply Pretrivialization.symm_apply -/ @@ -323,7 +324,7 @@ theorem coe_symm_of_not_mem (e : Pretrivialization F (π F E)) {b : B} (hb : b #print Pretrivialization.mk_symm /- theorem mk_symm (e : Pretrivialization F (π F E)) {b : B} (hb : b ∈ e.baseSet) (y : F) : - TotalSpace.mk b (e.symm b y) = e.toLocalEquiv.symm (b, y) := by + TotalSpace.mk b (e.symm b y) = e.toPartialEquiv.symm (b, y) := by rw [e.symm_apply hb, total_space.mk_cast, total_space.eta] #align pretrivialization.mk_symm Pretrivialization.mk_symm -/ @@ -510,7 +511,7 @@ theorem symm_apply_mk_proj (ex : x ∈ e.source) : e.toPartialHomeomorph.symm (p /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ #print Trivialization.symm_trans_source_eq /- theorem symm_trans_source_eq (e e' : Trivialization F proj) : - (e.toLocalEquiv.symm.trans e'.toLocalEquiv).source = (e.baseSet ∩ e'.baseSet) ×ˢ univ := + (e.toPartialEquiv.symm.trans e'.toPartialEquiv).source = (e.baseSet ∩ e'.baseSet) ×ˢ univ := Pretrivialization.symm_trans_source_eq e.toPretrivialization e' #align trivialization.symm_trans_source_eq Trivialization.symm_trans_source_eq -/ @@ -518,7 +519,7 @@ theorem symm_trans_source_eq (e e' : Trivialization F proj) : /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ #print Trivialization.symm_trans_target_eq /- theorem symm_trans_target_eq (e e' : Trivialization F proj) : - (e.toLocalEquiv.symm.trans e'.toLocalEquiv).target = (e.baseSet ∩ e'.baseSet) ×ˢ univ := + (e.toPartialEquiv.symm.trans e'.toPartialEquiv).target = (e.baseSet ∩ e'.baseSet) ×ˢ univ := Pretrivialization.symm_trans_target_eq e.toPretrivialization e' #align trivialization.symm_trans_target_eq Trivialization.symm_trans_target_eq -/ @@ -664,11 +665,11 @@ protected def compHomeomorph {Z' : Type _} [TopologicalSpace Z'] (h : Z' ≃ₜ trivialization of `Z` containing `z`. -/ theorem continuousAt_of_comp_right {X : Type _} [TopologicalSpace X] {f : Z → X} {z : Z} (e : Trivialization F proj) (he : proj z ∈ e.baseSet) - (hf : ContinuousAt (f ∘ e.toLocalEquiv.symm) (e z)) : ContinuousAt f z := + (hf : ContinuousAt (f ∘ e.toPartialEquiv.symm) (e z)) : ContinuousAt f z := by have hez : z ∈ e.to_local_equiv.symm.target := by - rw [LocalEquiv.symm_target, e.mem_source] + rw [PartialEquiv.symm_target, e.mem_source] exact he rwa [e.to_local_homeomorph.symm.continuous_at_iff_continuous_at_comp_right hez, PartialHomeomorph.symm_symm] @@ -725,7 +726,7 @@ theorem mk_mem_target {y : F} : (b, y) ∈ e'.target ↔ b ∈ e'.baseSet := #print Trivialization.symm_apply_apply /- theorem symm_apply_apply {x : TotalSpace F E} (hx : x ∈ e'.source) : e'.toPartialHomeomorph.symm (e' x) = x := - e'.toLocalEquiv.left_inv hx + e'.toPartialEquiv.left_inv hx #align trivialization.symm_apply_apply Trivialization.symm_apply_apply -/ diff --git a/Mathbin/Topology/LocalHomeomorph.lean b/Mathbin/Topology/LocalHomeomorph.lean index 3bff2df1dc..c2384a17aa 100644 --- a/Mathbin/Topology/LocalHomeomorph.lean +++ b/Mathbin/Topology/LocalHomeomorph.lean @@ -61,7 +61,7 @@ variable {α : Type _} {β : Type _} {γ : Type _} {δ : Type _} [TopologicalSpa /-- local homeomorphisms, defined on open subsets of the space -/ @[nolint has_nonempty_instance] structure PartialHomeomorph (α : Type _) (β : Type _) [TopologicalSpace α] - [TopologicalSpace β] extends LocalEquiv α β where + [TopologicalSpace β] extends PartialEquiv α β where open_source : IsOpen source open_target : IsOpen target continuous_toFun : ContinuousOn to_fun source @@ -79,7 +79,7 @@ instance : CoeFun (PartialHomeomorph α β) fun _ => α → β := #print PartialHomeomorph.symm /- /-- The inverse of a local homeomorphism -/ protected def symm : PartialHomeomorph β α := - { e.toLocalEquiv.symm with + { e.toPartialEquiv.symm with open_source := e.open_target open_target := e.open_source continuous_toFun := e.continuous_invFun @@ -103,8 +103,8 @@ def Simps.symm_apply (e : PartialHomeomorph α β) : β → α := -/ initialize_simps_projections PartialHomeomorph (to_local_equiv_to_fun → apply, - to_local_equiv_inv_fun → symm_apply, toLocalEquiv_source → source, toLocalEquiv_target → target, - -toLocalEquiv) + to_local_equiv_inv_fun → symm_apply, toPartialEquiv_source → source, toPartialEquiv_target → + target, -toPartialEquiv) #print PartialHomeomorph.continuousOn /- protected theorem continuousOn : ContinuousOn e e.source := @@ -120,23 +120,24 @@ theorem continuousOn_symm : ContinuousOn e.symm e.target := #print PartialHomeomorph.mk_coe /- @[simp, mfld_simps] -theorem mk_coe (e : LocalEquiv α β) (a b c d) : (PartialHomeomorph.mk e a b c d : α → β) = e := +theorem mk_coe (e : PartialEquiv α β) (a b c d) : (PartialHomeomorph.mk e a b c d : α → β) = e := rfl #align local_homeomorph.mk_coe PartialHomeomorph.mk_coe -/ #print PartialHomeomorph.mk_coe_symm /- @[simp, mfld_simps] -theorem mk_coe_symm (e : LocalEquiv α β) (a b c d) : +theorem mk_coe_symm (e : PartialEquiv α β) (a b c d) : ((PartialHomeomorph.mk e a b c d).symm : β → α) = e.symm := rfl #align local_homeomorph.mk_coe_symm PartialHomeomorph.mk_coe_symm -/ -#print PartialHomeomorph.toLocalEquiv_injective /- -theorem toLocalEquiv_injective : Injective (toLocalEquiv : PartialHomeomorph α β → LocalEquiv α β) +#print PartialHomeomorph.toPartialEquiv_injective /- +theorem toPartialEquiv_injective : + Injective (toLocalEquiv : PartialHomeomorph α β → PartialEquiv α β) | ⟨e, h₁, h₂, h₃, h₄⟩, ⟨e', h₁', h₂', h₃', h₄'⟩, rfl => rfl -#align local_homeomorph.to_local_equiv_injective PartialHomeomorph.toLocalEquiv_injective +#align local_homeomorph.to_local_equiv_injective PartialHomeomorph.toPartialEquiv_injective -/ #print PartialHomeomorph.toFun_eq_coe /- @@ -157,14 +158,14 @@ theorem invFun_eq_coe (e : PartialHomeomorph α β) : e.invFun = e.symm := #print PartialHomeomorph.coe_coe /- @[simp, mfld_simps] -theorem coe_coe : (e.toLocalEquiv : α → β) = e := +theorem coe_coe : (e.toPartialEquiv : α → β) = e := rfl #align local_homeomorph.coe_coe PartialHomeomorph.coe_coe -/ #print PartialHomeomorph.coe_coe_symm /- @[simp, mfld_simps] -theorem coe_coe_symm : (e.toLocalEquiv.symm : β → α) = e.symm := +theorem coe_coe_symm : (e.toPartialEquiv.symm : β → α) = e.symm := rfl #align local_homeomorph.coe_coe_symm PartialHomeomorph.coe_coe_symm -/ @@ -200,7 +201,7 @@ theorem right_inv {x : β} (h : x ∈ e.target) : e (e.symm x) = x := #print PartialHomeomorph.eq_symm_apply /- theorem eq_symm_apply {x : α} {y : β} (hx : x ∈ e.source) (hy : y ∈ e.target) : x = e.symm y ↔ e x = y := - e.toLocalEquiv.eq_symm_apply hx hy + e.toPartialEquiv.eq_symm_apply hx hy #align local_homeomorph.eq_symm_apply PartialHomeomorph.eq_symm_apply -/ @@ -253,7 +254,7 @@ protected theorem surjOn : SurjOn e e.source e.target := /-- A homeomorphism induces a local homeomorphism on the whole space -/ @[simps (config := { mfld_cfg with simpRhs := true })] def Homeomorph.toPartialHomeomorph (e : α ≃ₜ β) : PartialHomeomorph α β := - { e.toEquiv.toLocalEquiv with + { e.toEquiv.toPartialEquiv with open_source := isOpen_univ open_target := isOpen_univ continuous_toFun := by erw [← continuous_iff_continuousOn_univ]; exact e.continuous_to_fun @@ -263,9 +264,9 @@ def Homeomorph.toPartialHomeomorph (e : α ≃ₜ β) : PartialHomeomorph α β #print PartialHomeomorph.replaceEquiv /- /-- Replace `to_local_equiv` field to provide better definitional equalities. -/ -def replaceEquiv (e : PartialHomeomorph α β) (e' : LocalEquiv α β) (h : e.toLocalEquiv = e') : +def replaceEquiv (e : PartialHomeomorph α β) (e' : PartialEquiv α β) (h : e.toPartialEquiv = e') : PartialHomeomorph α β where - toLocalEquiv := e' + toPartialEquiv := e' open_source := h ▸ e.open_source open_target := h ▸ e.open_target continuous_toFun := h ▸ e.continuous_toFun @@ -274,8 +275,8 @@ def replaceEquiv (e : PartialHomeomorph α β) (e' : LocalEquiv α β) (h : e.to -/ #print PartialHomeomorph.replaceEquiv_eq_self /- -theorem replaceEquiv_eq_self (e : PartialHomeomorph α β) (e' : LocalEquiv α β) - (h : e.toLocalEquiv = e') : e.replaceEquiv e' h = e := by cases e; subst e'; rfl +theorem replaceEquiv_eq_self (e : PartialHomeomorph α β) (e' : PartialEquiv α β) + (h : e.toPartialEquiv = e') : e.replaceEquiv e' h = e := by cases e; subst e'; rfl #align local_homeomorph.replace_equiv_eq_self PartialHomeomorph.replaceEquiv_eq_self -/ @@ -286,8 +287,8 @@ theorem source_preimage_target : e.source ⊆ e ⁻¹' e.target := -/ #print PartialHomeomorph.eq_of_localEquiv_eq /- -theorem eq_of_localEquiv_eq {e e' : PartialHomeomorph α β} (h : e.toLocalEquiv = e'.toLocalEquiv) : - e = e' := by cases e; cases e'; cases h; rfl +theorem eq_of_localEquiv_eq {e e' : PartialHomeomorph α β} + (h : e.toPartialEquiv = e'.toPartialEquiv) : e = e' := by cases e; cases e'; cases h; rfl #align local_homeomorph.eq_of_local_equiv_eq PartialHomeomorph.eq_of_localEquiv_eq -/ @@ -343,20 +344,20 @@ theorem nhdsWithin_target_inter {x} (hx : x ∈ e.target) (s : Set β) : 𝓝[e. #print PartialHomeomorph.image_eq_target_inter_inv_preimage /- theorem image_eq_target_inter_inv_preimage {s : Set α} (h : s ⊆ e.source) : e '' s = e.target ∩ e.symm ⁻¹' s := - e.toLocalEquiv.image_eq_target_inter_inv_preimage h + e.toPartialEquiv.image_eq_target_inter_inv_preimage h #align local_homeomorph.image_eq_target_inter_inv_preimage PartialHomeomorph.image_eq_target_inter_inv_preimage -/ #print PartialHomeomorph.image_source_inter_eq' /- theorem image_source_inter_eq' (s : Set α) : e '' (e.source ∩ s) = e.target ∩ e.symm ⁻¹' s := - e.toLocalEquiv.image_source_inter_eq' s + e.toPartialEquiv.image_source_inter_eq' s #align local_homeomorph.image_source_inter_eq' PartialHomeomorph.image_source_inter_eq' -/ #print PartialHomeomorph.image_source_inter_eq /- theorem image_source_inter_eq (s : Set α) : e '' (e.source ∩ s) = e.target ∩ e.symm ⁻¹' (e.source ∩ s) := - e.toLocalEquiv.image_source_inter_eq s + e.toPartialEquiv.image_source_inter_eq s #align local_homeomorph.image_source_inter_eq PartialHomeomorph.image_source_inter_eq -/ @@ -377,7 +378,7 @@ theorem symm_image_target_inter_eq (s : Set β) : #print PartialHomeomorph.source_inter_preimage_inv_preimage /- theorem source_inter_preimage_inv_preimage (s : Set α) : e.source ∩ e ⁻¹' (e.symm ⁻¹' s) = e.source ∩ s := - e.toLocalEquiv.source_inter_preimage_inv_preimage s + e.toPartialEquiv.source_inter_preimage_inv_preimage s #align local_homeomorph.source_inter_preimage_inv_preimage PartialHomeomorph.source_inter_preimage_inv_preimage -/ @@ -391,13 +392,13 @@ theorem target_inter_inv_preimage_preimage (s : Set β) : #print PartialHomeomorph.source_inter_preimage_target_inter /- theorem source_inter_preimage_target_inter (s : Set β) : e.source ∩ e ⁻¹' (e.target ∩ s) = e.source ∩ e ⁻¹' s := - e.toLocalEquiv.source_inter_preimage_target_inter s + e.toPartialEquiv.source_inter_preimage_target_inter s #align local_homeomorph.source_inter_preimage_target_inter PartialHomeomorph.source_inter_preimage_target_inter -/ #print PartialHomeomorph.image_source_eq_target /- theorem image_source_eq_target (e : PartialHomeomorph α β) : e '' e.source = e.target := - e.toLocalEquiv.image_source_eq_target + e.toPartialEquiv.image_source_eq_target #align local_homeomorph.image_source_eq_target PartialHomeomorph.image_source_eq_target -/ @@ -415,7 +416,7 @@ called `eq_on_source`. -/ @[ext] protected theorem ext (e' : PartialHomeomorph α β) (h : ∀ x, e x = e' x) (hinv : ∀ x, e.symm x = e'.symm x) (hs : e.source = e'.source) : e = e' := - eq_of_localEquiv_eq (LocalEquiv.ext h hinv hs) + eq_of_localEquiv_eq (PartialEquiv.ext h hinv hs) #align local_homeomorph.ext PartialHomeomorph.ext -/ @@ -426,11 +427,11 @@ protected theorem ext_iff {e e' : PartialHomeomorph α β} : #align local_homeomorph.ext_iff PartialHomeomorph.ext_iff -/ -#print PartialHomeomorph.symm_toLocalEquiv /- +#print PartialHomeomorph.symm_toPartialEquiv /- @[simp, mfld_simps] -theorem symm_toLocalEquiv : e.symm.toLocalEquiv = e.toLocalEquiv.symm := +theorem symm_toPartialEquiv : e.symm.toPartialEquiv = e.toPartialEquiv.symm := rfl -#align local_homeomorph.symm_to_local_equiv PartialHomeomorph.symm_toLocalEquiv +#align local_homeomorph.symm_to_local_equiv PartialHomeomorph.symm_toPartialEquiv -/ #print PartialHomeomorph.symm_source /- @@ -608,10 +609,10 @@ namespace IsImage variable {e} {s : Set α} {t : Set β} {x : α} {y : β} -#print PartialHomeomorph.IsImage.toLocalEquiv /- -theorem toLocalEquiv (h : e.IsImage s t) : e.toLocalEquiv.IsImage s t := +#print PartialHomeomorph.IsImage.toPartialEquiv /- +theorem toPartialEquiv (h : e.IsImage s t) : e.toPartialEquiv.IsImage s t := h -#align local_homeomorph.is_image.to_local_equiv PartialHomeomorph.IsImage.toLocalEquiv +#align local_homeomorph.is_image.to_local_equiv PartialHomeomorph.IsImage.toPartialEquiv -/ #print PartialHomeomorph.IsImage.apply_mem_iff /- @@ -622,7 +623,7 @@ theorem apply_mem_iff (h : e.IsImage s t) (hx : x ∈ e.source) : e x ∈ t ↔ #print PartialHomeomorph.IsImage.symm /- protected theorem symm (h : e.IsImage s t) : e.symm.IsImage t s := - h.toLocalEquiv.symm + h.toPartialEquiv.symm #align local_homeomorph.is_image.symm PartialHomeomorph.IsImage.symm -/ @@ -641,7 +642,7 @@ theorem symm_iff : e.symm.IsImage t s ↔ e.IsImage s t := #print PartialHomeomorph.IsImage.mapsTo /- protected theorem mapsTo (h : e.IsImage s t) : MapsTo e (e.source ∩ s) (e.target ∩ t) := - h.toLocalEquiv.MapsTo + h.toPartialEquiv.MapsTo #align local_homeomorph.is_image.maps_to PartialHomeomorph.IsImage.mapsTo -/ @@ -653,7 +654,7 @@ theorem symm_mapsTo (h : e.IsImage s t) : MapsTo e.symm (e.target ∩ t) (e.sour #print PartialHomeomorph.IsImage.image_eq /- theorem image_eq (h : e.IsImage s t) : e '' (e.source ∩ s) = e.target ∩ t := - h.toLocalEquiv.image_eq + h.toPartialEquiv.image_eq #align local_homeomorph.is_image.image_eq PartialHomeomorph.IsImage.image_eq -/ @@ -665,7 +666,7 @@ theorem symm_image_eq (h : e.IsImage s t) : e.symm '' (e.target ∩ t) = e.sourc #print PartialHomeomorph.IsImage.iff_preimage_eq /- theorem iff_preimage_eq : e.IsImage s t ↔ e.source ∩ e ⁻¹' t = e.source ∩ s := - LocalEquiv.IsImage.iff_preimage_eq + PartialEquiv.IsImage.iff_preimage_eq #align local_homeomorph.is_image.iff_preimage_eq PartialHomeomorph.IsImage.iff_preimage_eq -/ @@ -706,13 +707,13 @@ alias ⟨preimage_eq', of_preimage_eq'⟩ := iff_preimage_eq' #print PartialHomeomorph.IsImage.of_image_eq /- theorem of_image_eq (h : e '' (e.source ∩ s) = e.target ∩ t) : e.IsImage s t := - LocalEquiv.IsImage.of_image_eq h + PartialEquiv.IsImage.of_image_eq h #align local_homeomorph.is_image.of_image_eq PartialHomeomorph.IsImage.of_image_eq -/ #print PartialHomeomorph.IsImage.of_symm_image_eq /- theorem of_symm_image_eq (h : e.symm '' (e.target ∩ t) = e.source ∩ s) : e.IsImage s t := - LocalEquiv.IsImage.of_symm_image_eq h + PartialEquiv.IsImage.of_symm_image_eq h #align local_homeomorph.is_image.of_symm_image_eq PartialHomeomorph.IsImage.of_symm_image_eq -/ @@ -744,7 +745,7 @@ protected theorem diff {s' t'} (h : e.IsImage s t) (h' : e.IsImage s' t') : theorem leftInvOn_piecewise {e' : PartialHomeomorph α β} [∀ i, Decidable (i ∈ s)] [∀ i, Decidable (i ∈ t)] (h : e.IsImage s t) (h' : e'.IsImage s t) : LeftInvOn (t.piecewise e.symm e'.symm) (s.piecewise e e') (s.ite e.source e'.source) := - h.toLocalEquiv.leftInvOn_piecewise h' + h.toPartialEquiv.leftInvOn_piecewise h' #align local_homeomorph.is_image.left_inv_on_piecewise PartialHomeomorph.IsImage.leftInvOn_piecewise -/ @@ -752,7 +753,7 @@ theorem leftInvOn_piecewise {e' : PartialHomeomorph α β} [∀ i, Decidable (i theorem inter_eq_of_inter_eq_of_eqOn {e' : PartialHomeomorph α β} (h : e.IsImage s t) (h' : e'.IsImage s t) (hs : e.source ∩ s = e'.source ∩ s) (Heq : EqOn e e' (e.source ∩ s)) : e.target ∩ t = e'.target ∩ t := - h.toLocalEquiv.inter_eq_of_inter_eq_of_eqOn h' hs Heq + h.toPartialEquiv.inter_eq_of_inter_eq_of_eqOn h' hs Heq #align local_homeomorph.is_image.inter_eq_of_inter_eq_of_eq_on PartialHomeomorph.IsImage.inter_eq_of_inter_eq_of_eqOn -/ @@ -760,7 +761,7 @@ theorem inter_eq_of_inter_eq_of_eqOn {e' : PartialHomeomorph α β} (h : e.IsIma theorem symm_eqOn_of_inter_eq_of_eqOn {e' : PartialHomeomorph α β} (h : e.IsImage s t) (hs : e.source ∩ s = e'.source ∩ s) (Heq : EqOn e e' (e.source ∩ s)) : EqOn e.symm e'.symm (e.target ∩ t) := - h.toLocalEquiv.symm_eq_on_of_inter_eq_of_eqOn hs Heq + h.toPartialEquiv.symm_eq_on_of_inter_eq_of_eqOn hs Heq #align local_homeomorph.is_image.symm_eq_on_of_inter_eq_of_eq_on PartialHomeomorph.IsImage.symm_eqOn_of_inter_eq_of_eqOn -/ @@ -797,10 +798,10 @@ theorem isOpen_iff (h : e.IsImage s t) : IsOpen (e.source ∩ s) ↔ IsOpen (e.t #print PartialHomeomorph.IsImage.restr /- /-- Restrict a `local_homeomorph` to a pair of corresponding open sets. -/ -@[simps toLocalEquiv] +@[simps toPartialEquiv] def restr (h : e.IsImage s t) (hs : IsOpen (e.source ∩ s)) : PartialHomeomorph α β where - toLocalEquiv := h.toLocalEquiv.restr + toPartialEquiv := h.toPartialEquiv.restr open_source := hs open_target := h.isOpen_iff.1 hs continuous_toFun := e.ContinuousOn.mono (inter_subset_left _ _) @@ -812,7 +813,7 @@ end IsImage #print PartialHomeomorph.isImage_source_target /- theorem isImage_source_target : e.IsImage e.source e.target := - e.toLocalEquiv.isImage_source_target + e.toPartialEquiv.isImage_source_target #align local_homeomorph.is_image_source_target PartialHomeomorph.isImage_source_target -/ @@ -820,7 +821,7 @@ theorem isImage_source_target : e.IsImage e.source e.target := theorem isImage_source_target_of_disjoint (e' : PartialHomeomorph α β) (hs : Disjoint e.source e'.source) (ht : Disjoint e.target e'.target) : e.IsImage e'.source e'.target := - e.toLocalEquiv.isImage_source_target_of_disjoint e'.toLocalEquiv hs ht + e.toPartialEquiv.isImage_source_target_of_disjoint e'.toPartialEquiv hs ht #align local_homeomorph.is_image_source_target_of_disjoint PartialHomeomorph.isImage_source_target_of_disjoint -/ @@ -871,10 +872,10 @@ theorem image_isOpen_of_isOpen' {s : Set α} (hs : IsOpen s) : IsOpen (e '' (e.s #print PartialHomeomorph.ofContinuousOpenRestrict /- /-- A `local_equiv` with continuous open forward map and an open source is a `local_homeomorph`. -/ -def ofContinuousOpenRestrict (e : LocalEquiv α β) (hc : ContinuousOn e e.source) +def ofContinuousOpenRestrict (e : PartialEquiv α β) (hc : ContinuousOn e e.source) (ho : IsOpenMap (e.source.restrict e)) (hs : IsOpen e.source) : PartialHomeomorph α β where - toLocalEquiv := e + toPartialEquiv := e open_source := hs open_target := by simpa only [range_restrict, e.image_source_eq_target] using ho.is_open_range continuous_toFun := hc @@ -884,7 +885,7 @@ def ofContinuousOpenRestrict (e : LocalEquiv α β) (hc : ContinuousOn e e.sourc #print PartialHomeomorph.ofContinuousOpen /- /-- A `local_equiv` with continuous open forward map and an open source is a `local_homeomorph`. -/ -def ofContinuousOpen (e : LocalEquiv α β) (hc : ContinuousOn e e.source) (ho : IsOpenMap e) +def ofContinuousOpen (e : PartialEquiv α β) (hc : ContinuousOn e e.source) (ho : IsOpenMap e) (hs : IsOpen e.source) : PartialHomeomorph α β := ofContinuousOpenRestrict e hc (ho.restrict hs) hs #align local_homeomorph.of_continuous_open PartialHomeomorph.ofContinuousOpen @@ -900,12 +901,12 @@ protected def restrOpen (s : Set α) (hs : IsOpen s) : PartialHomeomorph α β : #align local_homeomorph.restr_open PartialHomeomorph.restrOpen -/ -#print PartialHomeomorph.restrOpen_toLocalEquiv /- +#print PartialHomeomorph.restrOpen_toPartialEquiv /- @[simp, mfld_simps] -theorem restrOpen_toLocalEquiv (s : Set α) (hs : IsOpen s) : - (e.restrOpen s hs).toLocalEquiv = e.toLocalEquiv.restr s := +theorem restrOpen_toPartialEquiv (s : Set α) (hs : IsOpen s) : + (e.restrOpen s hs).toPartialEquiv = e.toPartialEquiv.restr s := rfl -#align local_homeomorph.restr_open_to_local_equiv PartialHomeomorph.restrOpen_toLocalEquiv +#align local_homeomorph.restr_open_to_local_equiv PartialHomeomorph.restrOpen_toPartialEquiv -/ #print PartialHomeomorph.restrOpen_source /- @@ -926,12 +927,12 @@ protected def restr (s : Set α) : PartialHomeomorph α β := #align local_homeomorph.restr PartialHomeomorph.restr -/ -#print PartialHomeomorph.restr_toLocalEquiv /- +#print PartialHomeomorph.restr_toPartialEquiv /- @[simp, mfld_simps] -theorem restr_toLocalEquiv (s : Set α) : - (e.restr s).toLocalEquiv = e.toLocalEquiv.restr (interior s) := +theorem restr_toPartialEquiv (s : Set α) : + (e.restr s).toPartialEquiv = e.toPartialEquiv.restr (interior s) := rfl -#align local_homeomorph.restr_to_local_equiv PartialHomeomorph.restr_toLocalEquiv +#align local_homeomorph.restr_to_local_equiv PartialHomeomorph.restr_toPartialEquiv -/ #print PartialHomeomorph.restr_source' /- @@ -940,11 +941,11 @@ theorem restr_source' (s : Set α) (hs : IsOpen s) : (e.restr s).source = e.sour #align local_homeomorph.restr_source' PartialHomeomorph.restr_source' -/ -#print PartialHomeomorph.restr_toLocalEquiv' /- -theorem restr_toLocalEquiv' (s : Set α) (hs : IsOpen s) : - (e.restr s).toLocalEquiv = e.toLocalEquiv.restr s := by +#print PartialHomeomorph.restr_toPartialEquiv' /- +theorem restr_toPartialEquiv' (s : Set α) (hs : IsOpen s) : + (e.restr s).toPartialEquiv = e.toPartialEquiv.restr s := by rw [e.restr_to_local_equiv, hs.interior_eq] -#align local_homeomorph.restr_to_local_equiv' PartialHomeomorph.restr_toLocalEquiv' +#align local_homeomorph.restr_to_local_equiv' PartialHomeomorph.restr_toPartialEquiv' -/ #print PartialHomeomorph.restr_eq_of_source_subset /- @@ -952,7 +953,7 @@ theorem restr_eq_of_source_subset {e : PartialHomeomorph α β} {s : Set α} (h e.restr s = e := by apply eq_of_local_equiv_eq rw [restr_to_local_equiv] - apply LocalEquiv.restr_eq_of_source_subset + apply PartialEquiv.restr_eq_of_source_subset exact interior_maximal h e.open_source #align local_homeomorph.restr_eq_of_source_subset PartialHomeomorph.restr_eq_of_source_subset -/ @@ -982,7 +983,7 @@ protected def refl (α : Type _) [TopologicalSpace α] : PartialHomeomorph α α #print PartialHomeomorph.refl_localEquiv /- @[simp, mfld_simps] -theorem refl_localEquiv : (PartialHomeomorph.refl α).toLocalEquiv = LocalEquiv.refl α := +theorem refl_localEquiv : (PartialHomeomorph.refl α).toPartialEquiv = PartialEquiv.refl α := rfl #align local_homeomorph.refl_local_equiv PartialHomeomorph.refl_localEquiv -/ @@ -1002,7 +1003,7 @@ variable {s : Set α} (hs : IsOpen s) /-- The identity local equiv on a set `s` -/ @[simps (config := mfld_cfg) apply, simps (config := { attrs := [] }) source target] def ofSet (s : Set α) (hs : IsOpen s) : PartialHomeomorph α α := - { LocalEquiv.ofSet s with + { PartialEquiv.ofSet s with open_source := hs open_target := hs continuous_toFun := continuous_id.ContinuousOn @@ -1010,11 +1011,11 @@ def ofSet (s : Set α) (hs : IsOpen s) : PartialHomeomorph α α := #align local_homeomorph.of_set PartialHomeomorph.ofSet -/ -#print PartialHomeomorph.ofSet_toLocalEquiv /- +#print PartialHomeomorph.ofSet_toPartialEquiv /- @[simp, mfld_simps] -theorem ofSet_toLocalEquiv : (ofSet s hs).toLocalEquiv = LocalEquiv.ofSet s := +theorem ofSet_toPartialEquiv : (ofSet s hs).toPartialEquiv = PartialEquiv.ofSet s := rfl -#align local_homeomorph.of_set_to_local_equiv PartialHomeomorph.ofSet_toLocalEquiv +#align local_homeomorph.of_set_to_local_equiv PartialHomeomorph.ofSet_toPartialEquiv -/ #print PartialHomeomorph.ofSet_symm /- @@ -1037,7 +1038,7 @@ end the second coincide. -/ protected def trans' (h : e.target = e'.source) : PartialHomeomorph α γ := { - LocalEquiv.trans' e.toLocalEquiv e'.toLocalEquiv + PartialEquiv.trans' e.toPartialEquiv e'.toPartialEquiv h with open_source := e.open_source open_target := e'.open_target @@ -1061,11 +1062,12 @@ protected def trans : PartialHomeomorph α γ := #align local_homeomorph.trans PartialHomeomorph.trans -/ -#print PartialHomeomorph.trans_toLocalEquiv /- +#print PartialHomeomorph.trans_toPartialEquiv /- @[simp, mfld_simps] -theorem trans_toLocalEquiv : (e.trans e').toLocalEquiv = e.toLocalEquiv.trans e'.toLocalEquiv := +theorem trans_toPartialEquiv : + (e.trans e').toPartialEquiv = e.toPartialEquiv.trans e'.toPartialEquiv := rfl -#align local_homeomorph.trans_to_local_equiv PartialHomeomorph.trans_toLocalEquiv +#align local_homeomorph.trans_to_local_equiv PartialHomeomorph.trans_toPartialEquiv -/ #print PartialHomeomorph.coe_trans /- @@ -1098,25 +1100,25 @@ theorem trans_symm_eq_symm_trans_symm : (e.trans e').symm = e'.symm.trans e.symm /- This could be considered as a simp lemma, but there are many situations where it makes something simple into something more complicated. -/ theorem trans_source : (e.trans e').source = e.source ∩ e ⁻¹' e'.source := - LocalEquiv.trans_source e.toLocalEquiv e'.toLocalEquiv + PartialEquiv.trans_source e.toPartialEquiv e'.toPartialEquiv #align local_homeomorph.trans_source PartialHomeomorph.trans_source -/ #print PartialHomeomorph.trans_source' /- theorem trans_source' : (e.trans e').source = e.source ∩ e ⁻¹' (e.target ∩ e'.source) := - LocalEquiv.trans_source' e.toLocalEquiv e'.toLocalEquiv + PartialEquiv.trans_source' e.toPartialEquiv e'.toPartialEquiv #align local_homeomorph.trans_source' PartialHomeomorph.trans_source' -/ #print PartialHomeomorph.trans_source'' /- theorem trans_source'' : (e.trans e').source = e.symm '' (e.target ∩ e'.source) := - LocalEquiv.trans_source'' e.toLocalEquiv e'.toLocalEquiv + PartialEquiv.trans_source'' e.toPartialEquiv e'.toPartialEquiv #align local_homeomorph.trans_source'' PartialHomeomorph.trans_source'' -/ #print PartialHomeomorph.image_trans_source /- theorem image_trans_source : e '' (e.trans e').source = e.target ∩ e'.source := - LocalEquiv.image_trans_source e.toLocalEquiv e'.toLocalEquiv + PartialEquiv.image_trans_source e.toPartialEquiv e'.toPartialEquiv #align local_homeomorph.image_trans_source PartialHomeomorph.image_trans_source -/ @@ -1147,28 +1149,29 @@ theorem inv_image_trans_target : e'.symm '' (e.trans e').target = e'.source ∩ #print PartialHomeomorph.trans_assoc /- theorem trans_assoc (e'' : PartialHomeomorph γ δ) : (e.trans e').trans e'' = e.trans (e'.trans e'') := - eq_of_localEquiv_eq <| LocalEquiv.trans_assoc e.toLocalEquiv e'.toLocalEquiv e''.toLocalEquiv + eq_of_localEquiv_eq <| + PartialEquiv.trans_assoc e.toPartialEquiv e'.toPartialEquiv e''.toPartialEquiv #align local_homeomorph.trans_assoc PartialHomeomorph.trans_assoc -/ #print PartialHomeomorph.trans_refl /- @[simp, mfld_simps] theorem trans_refl : e.trans (PartialHomeomorph.refl β) = e := - eq_of_localEquiv_eq <| LocalEquiv.trans_refl e.toLocalEquiv + eq_of_localEquiv_eq <| PartialEquiv.trans_refl e.toPartialEquiv #align local_homeomorph.trans_refl PartialHomeomorph.trans_refl -/ #print PartialHomeomorph.refl_trans /- @[simp, mfld_simps] theorem refl_trans : (PartialHomeomorph.refl α).trans e = e := - eq_of_localEquiv_eq <| LocalEquiv.refl_trans e.toLocalEquiv + eq_of_localEquiv_eq <| PartialEquiv.refl_trans e.toPartialEquiv #align local_homeomorph.refl_trans PartialHomeomorph.refl_trans -/ #print PartialHomeomorph.trans_ofSet /- theorem trans_ofSet {s : Set β} (hs : IsOpen s) : e.trans (ofSet s hs) = e.restr (e ⁻¹' s) := (PartialHomeomorph.ext _ _ (fun x => rfl) fun x => rfl) <| by - simp [LocalEquiv.trans_source, (e.preimage_interior _).symm, hs.interior_eq] + simp [PartialEquiv.trans_source, (e.preimage_interior _).symm, hs.interior_eq] #align local_homeomorph.trans_of_set PartialHomeomorph.trans_ofSet -/ @@ -1181,7 +1184,7 @@ theorem trans_of_set' {s : Set β} (hs : IsOpen s) : #print PartialHomeomorph.ofSet_trans /- theorem ofSet_trans {s : Set α} (hs : IsOpen s) : (ofSet s hs).trans e = e.restr s := (PartialHomeomorph.ext _ _ (fun x => rfl) fun x => rfl) <| by - simp [LocalEquiv.trans_source, hs.interior_eq, inter_comm] + simp [PartialEquiv.trans_source, hs.interior_eq, inter_comm] #align local_homeomorph.of_set_trans PartialHomeomorph.ofSet_trans -/ @@ -1203,7 +1206,7 @@ theorem ofSet_trans_ofSet {s : Set α} (hs : IsOpen s) {s' : Set α} (hs' : IsOp #print PartialHomeomorph.restr_trans /- theorem restr_trans (s : Set α) : (e.restr s).trans e' = (e.trans e').restr s := - eq_of_localEquiv_eq <| LocalEquiv.restr_trans e.toLocalEquiv e'.toLocalEquiv (interior s) + eq_of_localEquiv_eq <| PartialEquiv.restr_trans e.toPartialEquiv e'.toPartialEquiv (interior s) #align local_homeomorph.restr_trans PartialHomeomorph.restr_trans -/ @@ -1213,7 +1216,7 @@ We modify the source and target to have better definitional behavior. -/ @[simps (config := { fullyApplied := false })] def transHomeomorph (e' : β ≃ₜ γ) : PartialHomeomorph α γ where - toLocalEquiv := e.toLocalEquiv.transEquiv e'.toEquiv + toPartialEquiv := e.toPartialEquiv.transEquiv e'.toEquiv open_source := e.open_source open_target := e.open_target.Preimage e'.symm.Continuous continuous_toFun := e'.Continuous.comp_continuousOn e.ContinuousOn @@ -1224,7 +1227,7 @@ def transHomeomorph (e' : β ≃ₜ γ) : PartialHomeomorph α γ #print PartialHomeomorph.transHomeomorph_eq_trans /- theorem transHomeomorph_eq_trans (e' : β ≃ₜ γ) : e.transHomeomorph e' = e.trans e'.toPartialHomeomorph := - toLocalEquiv_injective <| LocalEquiv.transEquiv_eq_trans _ _ + toPartialEquiv_injective <| PartialEquiv.transEquiv_eq_trans _ _ #align local_homeomorph.trans_equiv_eq_trans PartialHomeomorph.transHomeomorph_eq_trans -/ @@ -1234,7 +1237,7 @@ We modify the source and target to have better definitional behavior. -/ @[simps (config := { fullyApplied := false })] def Homeomorph.transPartialHomeomorph (e : α ≃ₜ β) : PartialHomeomorph α γ where - toLocalEquiv := e.toEquiv.transLocalEquiv e'.toLocalEquiv + toPartialEquiv := e.toEquiv.transPartialEquiv e'.toPartialEquiv open_source := e'.open_source.Preimage e.Continuous open_target := e'.open_target continuous_toFun := e'.ContinuousOn.comp e.Continuous.ContinuousOn fun x h => h @@ -1245,7 +1248,7 @@ def Homeomorph.transPartialHomeomorph (e : α ≃ₜ β) : PartialHomeomorph α #print Homeomorph.transPartialHomeomorph_eq_trans /- theorem Homeomorph.transPartialHomeomorph_eq_trans (e : α ≃ₜ β) : e.transPartialHomeomorph e' = e.toPartialHomeomorph.trans e' := - toLocalEquiv_injective <| Equiv.transLocalEquiv_eq_trans _ _ + toPartialEquiv_injective <| Equiv.transPartialEquiv_eq_trans _ _ #align homeomorph.trans_local_homeomorph_eq_trans Homeomorph.transPartialHomeomorph_eq_trans -/ @@ -1259,7 +1262,7 @@ def EqOnSource (e e' : PartialHomeomorph α β) : Prop := #print PartialHomeomorph.eqOnSource_iff /- theorem eqOnSource_iff (e e' : PartialHomeomorph α β) : - EqOnSource e e' ↔ LocalEquiv.EqOnSource e.toLocalEquiv e'.toLocalEquiv := + EqOnSource e e' ↔ PartialEquiv.EqOnSource e.toPartialEquiv e'.toPartialEquiv := Iff.rfl #align local_homeomorph.eq_on_source_iff PartialHomeomorph.eqOnSource_iff -/ @@ -1269,9 +1272,10 @@ instance : Setoid (PartialHomeomorph α β) where R := EqOnSource iseqv := - ⟨fun e => (@LocalEquiv.eqOnSourceSetoid α β).iseqv.1 e.toLocalEquiv, fun e e' h => - (@LocalEquiv.eqOnSourceSetoid α β).iseqv.2.1 ((eqOnSource_iff e e').1 h), fun e e' e'' h h' => - (@LocalEquiv.eqOnSourceSetoid α β).iseqv.2.2 ((eqOnSource_iff e e').1 h) + ⟨fun e => (@PartialEquiv.eqOnSourceSetoid α β).iseqv.1 e.toPartialEquiv, fun e e' h => + (@PartialEquiv.eqOnSourceSetoid α β).iseqv.2.1 ((eqOnSource_iff e e').1 h), + fun e e' e'' h h' => + (@PartialEquiv.eqOnSourceSetoid α β).iseqv.2.2 ((eqOnSource_iff e e').1 h) ((eqOnSource_iff e' e'').1 h')⟩ #print PartialHomeomorph.eqOnSource_refl /- @@ -1283,7 +1287,7 @@ theorem eqOnSource_refl : e ≈ e := #print PartialHomeomorph.EqOnSource.symm' /- /-- If two local homeomorphisms are equivalent, so are their inverses -/ theorem EqOnSource.symm' {e e' : PartialHomeomorph α β} (h : e ≈ e') : e.symm ≈ e'.symm := - LocalEquiv.EqOnSource.symm' h + PartialEquiv.EqOnSource.symm' h #align local_homeomorph.eq_on_source.symm' PartialHomeomorph.EqOnSource.symm' -/ @@ -1320,7 +1324,7 @@ theorem EqOnSource.symm_eqOn_target {e e' : PartialHomeomorph α β} (h : e ≈ /-- Composition of local homeomorphisms respects equivalence -/ theorem EqOnSource.trans' {e e' : PartialHomeomorph α β} {f f' : PartialHomeomorph β γ} (he : e ≈ e') (hf : f ≈ f') : e.trans f ≈ e'.trans f' := - LocalEquiv.EqOnSource.trans' he hf + PartialEquiv.EqOnSource.trans' he hf #align local_homeomorph.eq_on_source.trans' PartialHomeomorph.EqOnSource.trans' -/ @@ -1328,7 +1332,7 @@ theorem EqOnSource.trans' {e e' : PartialHomeomorph α β} {f f' : PartialHomeom /-- Restriction of local homeomorphisms respects equivalence -/ theorem EqOnSource.restr {e e' : PartialHomeomorph α β} (he : e ≈ e') (s : Set α) : e.restr s ≈ e'.restr s := - LocalEquiv.EqOnSource.restr he _ + PartialEquiv.EqOnSource.restr he _ #align local_homeomorph.eq_on_source.restr PartialHomeomorph.EqOnSource.restr -/ @@ -1349,7 +1353,7 @@ theorem Set.EqOn.restr_eqOn_source {e e' : PartialHomeomorph α β} /-- Composition of a local homeomorphism and its inverse is equivalent to the restriction of the identity to the source -/ theorem trans_self_symm : e.trans e.symm ≈ PartialHomeomorph.ofSet e.source e.open_source := - LocalEquiv.trans_self_symm _ + PartialEquiv.trans_self_symm _ #align local_homeomorph.trans_self_symm PartialHomeomorph.trans_self_symm -/ @@ -1362,7 +1366,7 @@ theorem trans_symm_self : e.symm.trans e ≈ PartialHomeomorph.ofSet e.target e. #print PartialHomeomorph.eq_of_eqOnSource_univ /- theorem eq_of_eqOnSource_univ {e e' : PartialHomeomorph α β} (h : e ≈ e') (s : e.source = univ) (t : e.target = univ) : e = e' := - eq_of_localEquiv_eq <| LocalEquiv.eq_of_eqOnSource_univ _ _ h s t + eq_of_localEquiv_eq <| PartialEquiv.eq_of_eqOnSource_univ _ _ h s t #align local_homeomorph.eq_of_eq_on_source_univ PartialHomeomorph.eq_of_eqOnSource_univ -/ @@ -1370,7 +1374,7 @@ section Prod #print PartialHomeomorph.prod /- /-- The product of two local homeomorphisms, as a local homeomorphism on the product space. -/ -@[simps (config := mfld_cfg) toLocalEquiv apply, +@[simps (config := mfld_cfg) toPartialEquiv apply, simps (config := { attrs := [] }) source target symm_apply] def prod (e : PartialHomeomorph α β) (e' : PartialHomeomorph γ δ) : PartialHomeomorph (α × γ) (β × δ) @@ -1379,7 +1383,7 @@ def prod (e : PartialHomeomorph α β) (e' : PartialHomeomorph γ δ) : open_target := e.open_target.Prod e'.open_target continuous_toFun := e.ContinuousOn.Prod_map e'.ContinuousOn continuous_invFun := e.continuousOn_symm.Prod_map e'.continuousOn_symm - toLocalEquiv := e.toLocalEquiv.Prod e'.toLocalEquiv + toPartialEquiv := e.toPartialEquiv.Prod e'.toPartialEquiv #align local_homeomorph.prod PartialHomeomorph.prod -/ @@ -1405,7 +1409,7 @@ theorem prod_trans {η : Type _} {ε : Type _} [TopologicalSpace η] [Topologica (e : PartialHomeomorph α β) (f : PartialHomeomorph β γ) (e' : PartialHomeomorph δ η) (f' : PartialHomeomorph η ε) : (e.Prod e').trans (f.Prod f') = (e.trans f).Prod (e'.trans f') := PartialHomeomorph.eq_of_localEquiv_eq <| by - dsimp only [trans_to_local_equiv, prod_to_local_equiv] <;> apply LocalEquiv.prod_trans + dsimp only [trans_to_local_equiv, prod_to_local_equiv] <;> apply PartialEquiv.prod_trans #align local_homeomorph.prod_trans PartialHomeomorph.prod_trans -/ @@ -1444,13 +1448,13 @@ are inverse of each other on the new `source` and `target`, the definition assum and `t` are related both by `e.is_image` and `e'.is_image`. To ensure that the new maps are continuous on `source`/`target`, it also assumes that `e.source` and `e'.source` meet `frontier s` on the same set and `e x = e' x` on this intersection. -/ -@[simps (config := { fullyApplied := false }) toLocalEquiv apply] +@[simps (config := { fullyApplied := false }) toPartialEquiv apply] def piecewise (e e' : PartialHomeomorph α β) (s : Set α) (t : Set β) [∀ x, Decidable (x ∈ s)] [∀ y, Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t) (Hs : e.source ∩ frontier s = e'.source ∩ frontier s) (Heq : EqOn e e' (e.source ∩ frontier s)) : PartialHomeomorph α β where - toLocalEquiv := e.toLocalEquiv.piecewise e'.toLocalEquiv s t H H' + toPartialEquiv := e.toPartialEquiv.piecewise e'.toPartialEquiv s t H H' open_source := e.open_source.ite e'.open_source Hs open_target := e.open_target.ite e'.open_target <| H.frontier.inter_eq_of_inter_eq_of_eqOn H'.frontier Hs Heq @@ -1487,8 +1491,8 @@ def disjointUnion (e e' : PartialHomeomorph α β) [∀ x, Decidable (x ∈ e.so (e'.isImage_source_target_of_disjoint e Hs.symm Ht.symm) (by rw [e.open_source.inter_frontier_eq, (Hs.symm.frontier_right e'.open_source).inter_eq]) (by rw [e.open_source.inter_frontier_eq]; exact eq_on_empty _ _)).replaceEquiv - (e.toLocalEquiv.disjointUnion e'.toLocalEquiv Hs Ht) - (LocalEquiv.disjointUnion_eq_piecewise _ _ _ _).symm + (e.toPartialEquiv.disjointUnion e'.toPartialEquiv Hs Ht) + (PartialEquiv.disjointUnion_eq_piecewise _ _ _ _).symm #align local_homeomorph.disjoint_union PartialHomeomorph.disjointUnion -/ @@ -1501,10 +1505,10 @@ variable {ι : Type _} [Fintype ι] {Xi Yi : ι → Type _} [∀ i, TopologicalS #print PartialHomeomorph.pi /- /-- The product of a finite family of `local_homeomorph`s. -/ -@[simps toLocalEquiv] +@[simps toPartialEquiv] def pi : PartialHomeomorph (∀ i, Xi i) (∀ i, Yi i) where - toLocalEquiv := LocalEquiv.pi fun i => (ei i).toLocalEquiv + toPartialEquiv := PartialEquiv.pi fun i => (ei i).toPartialEquiv open_source := isOpen_set_pi finite_univ fun i hi => (ei i).open_source open_target := isOpen_set_pi finite_univ fun i hi => (ei i).open_target continuous_toFun := @@ -1714,7 +1718,7 @@ theorem symm_toPartialHomeomorph : e.symm.toPartialHomeomorph = e.toPartialHomeo @[simp, mfld_simps] theorem trans_toPartialHomeomorph : (e.trans e').toPartialHomeomorph = e.toPartialHomeomorph.trans e'.toPartialHomeomorph := - PartialHomeomorph.eq_of_localEquiv_eq <| Equiv.trans_toLocalEquiv _ _ + PartialHomeomorph.eq_of_localEquiv_eq <| Equiv.trans_toPartialEquiv _ _ #align homeomorph.trans_to_local_homeomorph Homeomorph.trans_toPartialHomeomorph -/ @@ -1729,7 +1733,7 @@ variable (f : α → β) (h : OpenEmbedding f) is all of `α`. The converse is also true; see `local_homeomorph.to_open_embedding`. -/ @[simps (config := mfld_cfg) apply source target] noncomputable def toPartialHomeomorph [Nonempty α] : PartialHomeomorph α β := - PartialHomeomorph.ofContinuousOpen ((h.toEmbedding.inj.InjOn univ).toLocalEquiv _ _) + PartialHomeomorph.ofContinuousOpen ((h.toEmbedding.inj.InjOn univ).toPartialEquiv _ _) h.Continuous.ContinuousOn h.IsOpenMap isOpen_univ #align open_embedding.to_local_homeomorph OpenEmbedding.toPartialHomeomorph -/ diff --git a/Mathbin/Topology/VectorBundle/Hom.lean b/Mathbin/Topology/VectorBundle/Hom.lean index 23429fc1c3..8567bc194f 100644 --- a/Mathbin/Topology/VectorBundle/Hom.lean +++ b/Mathbin/Topology/VectorBundle/Hom.lean @@ -198,7 +198,7 @@ theorem continuousLinearMap_apply (p : TotalSpace (F₁ →SL[σ] F₂) fun x => #print Pretrivialization.continuousLinearMap_symm_apply /- theorem continuousLinearMap_symm_apply (p : B × (F₁ →SL[σ] F₂)) : - (continuousLinearMap σ e₁ e₂).toLocalEquiv.symm p = + (continuousLinearMap σ e₁ e₂).toPartialEquiv.symm p = ⟨p.1, ContinuousLinearMap.comp (e₂.symmL 𝕜₂ p.1) (p.2.comp (e₁.continuousLinearMapAt 𝕜₁ p.1 : E₁ p.1 →L[𝕜₁] F₁) : E₁ p.1 →SL[σ] F₂)⟩ := diff --git a/lake-manifest.json b/lake-manifest.json index 26f53d8f6a..23c3774106 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -49,19 +49,19 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "00056bcbe30c02bf7f225b8308af3a0e203d4c34", + "rev": "6bb383b09ebd407aabadf1dde2aef5017ac69b0f", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "00056bcbe30c02bf7f225b8308af3a0e203d4c34", + "inputRev": "6bb383b09ebd407aabadf1dde2aef5017ac69b0f", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/lean3port.git", "type": "git", "subDir": null, - "rev": "9af70e78c237870ad1491aeecee7e33e9c8e3991", + "rev": "1aec722805ddb2395a033c1c7523ac6863fe49df", "name": "lean3port", "manifestFile": "lake-manifest.json", - "inputRev": "9af70e78c237870ad1491aeecee7e33e9c8e3991", + "inputRev": "1aec722805ddb2395a033c1c7523ac6863fe49df", "inherited": false, "configFile": "lakefile.lean"}], "name": "mathlib3port", diff --git a/lakefile.lean b/lakefile.lean index 542bd0b91f..f5311840dc 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -4,7 +4,7 @@ open Lake DSL System -- Usually the `tag` will be of the form `nightly-2021-11-22`. -- If you would like to use an artifact from a PR build, -- it will be of the form `pr-branchname-sha`. -def tag : String := "nightly-2023-12-13-12" +def tag : String := "nightly-2023-12-14-06" def releaseRepo : String := "leanprover-community/mathport" def oleanTarName : String := "mathlib3-binport.tar.gz" @@ -38,7 +38,7 @@ target fetchOleans (_pkg) : Unit := do untarReleaseArtifact releaseRepo tag oleanTarName libDir return .nil -require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"9af70e78c237870ad1491aeecee7e33e9c8e3991" +require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"1aec722805ddb2395a033c1c7523ac6863fe49df" @[default_target] lean_lib Mathbin where