fin_param — Mathlib

English

There exists n and an injective map f: Fin n → α with range s.

Русский

Существует n и инъективное отображение f: Fin n → α с образцом s.

LaTeX

$$$\\exists n,\\exists f : Fin n \\to \\alpha,\\text{ Injective}(f) \\land \\text{range}(f) = s$$$

Lean4

theorem fin_param {s : Set α} (h : s.Finite) : ∃ (n : ℕ) (f : Fin n → α), Injective f ∧ range f = s :=
  let ⟨n, f, hf⟩ := h.fin_embedding
  ⟨n, f, f.injective, hf⟩

Похожие утверждения