feat(linear_algebra/affine_space/basis): reindex API (#18190)

Rename and change arguments to `affine_basis.comp_equiv` so that it matches `basis.reindex`. Provide lemmas for its interaction with other `affine_basis` constructions.

Make `affine_basis` follow the `fun_like` design, replacing `affine_basis.points` by a function coercion.

Fix a few names all around:
* `affine_basis.coord_apply_neq` → `affine_basis.coord_apply_ne`
* `convex_hull_affine_basis_eq_nonneg_barycentric` → `affine_basis.convex_hull_eq_nonneg_coord`

src/analysis/convex/combination.lean

@@ -461,19 +461,18 @@ lemma mem_Icc_of_mem_std_simplex (hf : f ∈ std_simplex R ι) (x) :
 
 /-- The convex hull of an affine basis is the intersection of the half-spaces defined by the
 corresponding barycentric coordinates. -/
-lemma convex_hull_affine_basis_eq_nonneg_barycentric {ι : Type*} (b : affine_basis ι R E) :
-  convex_hull R (range b.points) = { x | ∀ i, 0 ≤ b.coord i x } :=
+lemma affine_basis.convex_hull_eq_nonneg_coord {ι : Type*} (b : affine_basis ι R E) :
+  convex_hull R (range b) = {x | ∀ i, 0 ≤ b.coord i x} :=
 begin
   rw convex_hull_range_eq_exists_affine_combination,
   ext x,
-  split,
+  refine ⟨_, λ hx, _⟩,
   { rintros ⟨s, w, hw₀, hw₁, rfl⟩ i,
     by_cases hi : i ∈ s,
     { rw b.coord_apply_combination_of_mem hi hw₁,
       exact hw₀ i hi, },
     { rw b.coord_apply_combination_of_not_mem hi hw₁, }, },
-  { intros hx,
-    have hx' : x ∈ affine_span R (range b.points),
+  { have hx' : x ∈ affine_span R (range b),
     { rw b.tot, exact affine_subspace.mem_top R E x, },
     obtain ⟨s, w, hw₁, rfl⟩ := (mem_affine_span_iff_eq_affine_combination R E).mp hx',
     refine ⟨s, w, _, hw₁, rfl⟩,

src/analysis/inner_product_space/pi_L2.lean

@@ -470,9 +470,9 @@ end
   ⇑(b.reindex e) = ⇑b ∘ ⇑(e.symm) :=
 funext (b.reindex_apply e)
 
-@[simp] protected lemma reindex_repr
+@[simp] protected lemma repr_reindex
   (b : orthonormal_basis ι 𝕜 E) (e : ι ≃ ι') (x : E) (i' : ι') :
-  ((b.reindex e).repr x) i' = (b.repr x) (e.symm i') :=
+  (b.reindex e).repr x i' = b.repr x (e.symm i') :=
 by { classical,
   rw [orthonormal_basis.repr_apply_apply, b.repr_apply_apply, orthonormal_basis.coe_reindex] }
 

src/analysis/normed_space/add_torsor_bases.lean

@@ -56,17 +56,17 @@ TODO Restate this result for affine spaces (instead of vector spaces) once the d
 convexity is generalised to this setting. -/
 lemma affine_basis.interior_convex_hull {ι E : Type*} [finite ι] [normed_add_comm_group E]
   [normed_space ℝ E] (b : affine_basis ι ℝ E) :
-  interior (convex_hull ℝ (range b.points)) = {x | ∀ i, 0 < b.coord i x} :=
+  interior (convex_hull ℝ (range b)) = {x | ∀ i, 0 < b.coord i x} :=
 begin
   casesI subsingleton_or_nontrivial ι,
   { -- The zero-dimensional case.
-    have : range (b.points) = univ,
+    have : range b = univ,
       from affine_subspace.eq_univ_of_subsingleton_span_eq_top (subsingleton_range _) b.tot,
     simp [this] },
   { -- The positive-dimensional case.
     haveI : finite_dimensional ℝ E := b.finite_dimensional,
-    have : convex_hull ℝ (range b.points) = ⋂ i, (b.coord i)⁻¹' Ici 0,
-    { rw [convex_hull_affine_basis_eq_nonneg_barycentric b, set_of_forall], refl },
+    have : convex_hull ℝ (range b) = ⋂ i, (b.coord i)⁻¹' Ici 0,
+    { rw [b.convex_hull_eq_nonneg_coord, set_of_forall], refl },
     ext,
     simp only [this, interior_Inter, ← is_open_map.preimage_interior_eq_interior_preimage
       (is_open_map_barycentric_coord b _) (continuous_barycentric_coord b _),
@@ -132,7 +132,7 @@ top_unique $ is_open_interior.affine_span_eq_top hs ▸
   (affine_span_mono _ interior_subset).trans_eq (affine_span_convex_hull _)
 
 lemma affine_basis.centroid_mem_interior_convex_hull {ι} [fintype ι] (b : affine_basis ι ℝ V) :
-  finset.univ.centroid ℝ b.points ∈ interior (convex_hull ℝ (range b.points)) :=
+  finset.univ.centroid ℝ b ∈ interior (convex_hull ℝ (range b)) :=
 begin
   haveI := b.nonempty,
   simp only [b.interior_convex_hull, mem_set_of_eq, b.coord_apply_centroid (finset.mem_univ _),
@@ -144,7 +144,7 @@ lemma interior_convex_hull_nonempty_iff_affine_span_eq_top [finite_dimensional 
 begin
   refine ⟨affine_span_eq_top_of_nonempty_interior, λ h, _⟩,
   obtain ⟨t, hts, b, hb⟩ := affine_basis.exists_affine_subbasis h,
-  suffices : (interior (convex_hull ℝ (range b.points))).nonempty,
+  suffices : (interior (convex_hull ℝ (range b))).nonempty,
   { rw [hb, subtype.range_coe_subtype, set_of_mem_eq] at this,
     refine this.mono _,
     mono* },

src/data/set/image.lean

@@ -29,13 +29,13 @@ import data.set.basic
 set, sets, image, preimage, pre-image, range
 
 -/
-universes u v
 
-open function
+open function set
 
-namespace set
+universes u v
+variables {α β γ : Type*} {ι ι' : Sort*}
 
-variables {α β γ : Type*} {ι : Sort*}
+namespace set
 
 /-! ### Inverse image -/
 
@@ -914,8 +914,7 @@ end subsingleton
 end set
 
 namespace function
-
-variables {ι : Sort*} {α : Type*} {β : Type*} {f : α → β}
+variables {f : α → β}
 
 open set
 
@@ -949,7 +948,7 @@ lemma surjective.preimage_subset_preimage_iff {s t : set β} (hf : surjective f)
   f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t :=
 by { apply preimage_subset_preimage_iff, rw [hf.range_eq], apply subset_univ }
 
-lemma surjective.range_comp {ι' : Sort*} {f : ι → ι'} (hf : surjective f) (g : ι' → α) :
+lemma surjective.range_comp {f : ι → ι'} (hf : surjective f) (g : ι' → α) :
   range (g ∘ f) = range g :=
 ext $ λ y, (@surjective.exists _ _ _ hf (λ x, g x = y)).symm
 
@@ -981,13 +980,20 @@ by rw [← preimage_comp, h.comp_eq_id, preimage_id]
 
 end function
 
+namespace equiv_like
+variables {E : Type*} [equiv_like E ι ι']
+include ι
+
+@[simp] lemma range_comp (f : ι' → α) (e : E) : set.range (f ∘ e) = set.range f :=
+(equiv_like.surjective _).range_comp _
+
+end equiv_like
+
 /-! ### Image and preimage on subtypes -/
 
 namespace subtype
 open set
 
-variable {α : Type*}
-
 lemma coe_image {p : α → Prop} {s : set (subtype p)} :
   coe '' s = {x | ∃h : p x, (⟨x, h⟩ : subtype p) ∈ s} :=
 set.ext $ assume a,
@@ -1109,9 +1115,9 @@ open function
 /-! ### Injectivity and surjectivity lemmas for image and preimage -/
 
 section image_preimage
-variables {α : Type u} {β : Type v} {f : α → β}
-@[simp]
-lemma preimage_injective : injective (preimage f) ↔ surjective f :=
+variables {f : α → β}
+
+@[simp] lemma preimage_injective : injective (preimage f) ↔ surjective f :=
 begin
   refine ⟨λ h y, _, surjective.preimage_injective⟩,
   obtain ⟨x, hx⟩ : (f ⁻¹' {y}).nonempty,
@@ -1156,7 +1162,7 @@ end set
 /-! ### Disjoint lemmas for image and preimage -/
 
 section disjoint
-variables {α β γ : Type*} {f : α → β} {s t : set α}
+variables {f : α → β} {s t : set α}
 
 lemma disjoint.preimage (f : α → β) {s t : set β} (h : disjoint s t) :
   disjoint (f ⁻¹' s) (f ⁻¹' t) :=