English
If f: Fin n → E is a function with ∥f i∥ ≤ 2 and pairwise distances satisfy 1−goodδ ≤ ∥f i − f j∥, then n ≤ multiplicity E.
Русский
Если f: Fin n → E удовлетворяет ∥f i∥ ≤ 2 и расстояния между различными i,j удовлетворяют 1−goodδ ≤ ∥f i − f j∥, то n ≤ multiplicity E.
LaTeX
$$$$n \\le multiplicity(E)$$$$
Lean4
theorem le_multiplicity_of_δ_of_fin {n : ℕ} (f : Fin n → E) (h : ∀ i, ‖f i‖ ≤ 2)
(h' : Pairwise fun i j => 1 - goodδ E ≤ ‖f i - f j‖) : n ≤ multiplicity E := by
classical
have finj : Function.Injective f := by
intro i j hij
by_contra h
have : 1 - goodδ E ≤ ‖f i - f j‖ := h' h
simp only [hij, norm_zero, sub_self] at this
linarith [goodδ_lt_one E]
let s := Finset.image f Finset.univ
have s_card : s.card = n := by rw [Finset.card_image_of_injective _ finj]; exact Finset.card_fin n
have hs : ∀ c ∈ s, ‖c‖ ≤ 2 := by
simp only [s, h, forall_apply_eq_imp_iff, forall_exists_index, Finset.mem_univ, Finset.mem_image, imp_true_iff,
true_and]
have h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - goodδ E ≤ ‖c - d‖ :=
by
simp only [s, forall_apply_eq_imp_iff, forall_exists_index, Finset.mem_univ, Finset.mem_image, Ne,
forall_apply_eq_imp_iff, true_and]
intro i j hij
have : i ≠ j := fun h => by rw [h] at hij; exact hij rfl
exact h' this
have : s.card ≤ multiplicity E := card_le_multiplicity_of_δ hs h's
rwa [s_card] at this
