fin_embedding — Mathlib

English

A finite subset s of α can be represented as the range of an embedding from Fin n into α.

Русский

Любое конечное подмножество s ≤ α можно выразить как образ внедрения из Fin n в α.

LaTeX

$$$\\exists n,\\exists f : Fin n \\hookrightarrow \\alpha,\\ \\mathrm{range}(f) = s$$$

Lean4

theorem fin_embedding {s : Set α} (h : s.Finite) : ∃ (n : ℕ) (f : Fin n ↪ α), range f = s :=
  ⟨_, (Fintype.equivFin (h.toFinset : Set α)).symm.asEmbedding, by
    simp only [Finset.coe_sort_coe, Equiv.asEmbedding_range, Finite.coe_toFinset, setOf_mem_eq]⟩

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