English
If two indexed families are similar, they remain similar after replacing indices via an equivalence.
Русский
Если две семейства по индексам подобны, то после замены индексов через эквивалентность они остаются подобными.
LaTeX
$$Given h: v1 ∼ v2 and f: ι' ≃ ι, then (v1 ∘ f) ∼ (v2 ∘ f).$$
Lean4
/-- Let `R : α → ℝ` be a (possibly discontinuous) function on a proper metric space.
Let `s` be a closed set in `α` such that `R` is positive on `s`. Then there exists a collection of
pairs of balls `Metric.ball (c i) (r i)`, `Metric.ball (c i) (r' i)` such that
* all centers belong to `s`;
* for all `i` we have `0 < r i < r' i < R (c i)`;
* the family of balls `Metric.ball (c i) (r' i)` is locally finite;
* the balls `Metric.ball (c i) (r i)` cover `s`.
This is a simple corollary of `refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set`
and `exists_subset_iUnion_ball_radius_pos_lt`. -/
theorem exists_locallyFinite_subset_iUnion_ball_radius_lt (hs : IsClosed s) {R : α → ℝ} (hR : ∀ x ∈ s, 0 < R x) :
∃ (ι : Type u) (c : ι → α) (r r' : ι → ℝ),
(∀ i, c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
(LocallyFinite fun i => ball (c i) (r' i)) ∧ s ⊆ ⋃ i, ball (c i) (r i) :=
by
have : ∀ x ∈ s, (𝓝 x).HasBasis (fun r : ℝ => 0 < r ∧ r < R x) fun r => ball x r := fun x hx =>
nhds_basis_uniformity (uniformity_basis_dist_lt (hR x hx))
rcases refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set hs this with ⟨ι, c, r', hr', hsub', hfin⟩
rcases exists_subset_iUnion_ball_radius_pos_lt (fun i => (hr' i).2.1) hs (fun x _ => hfin.point_finite x) hsub' with
⟨r, hsub, hlt⟩
exact ⟨ι, c, r, r', fun i => ⟨(hr' i).1, (hlt i).1, (hlt i).2, (hr' i).2.2⟩, hfin, hsub⟩
