attachFin — Mathlib

English

The operation attachFin embeds a finite set of natural numbers contained in {0,...,n-1} into Fin n by pairing each element m with a witness hm < n, producing a Finset of Fin n.

Русский

Операция attachFin внедряет конечное множество чисел натуральным в Fin n, сопоставляя каждому элементу пару (m, hm) с доказательством hm < n.

LaTeX

$$\\text{attachFin}(s,h) is the Finset of all elements $\\langle m, hm\\rangle$ with $m\\in s$ and $hm

Lean4

/-- Given a Finset `s` of `ℕ` contained in `{0,..., n-1}`, the corresponding Finset in `Fin n`
is `s.attachFin h` where `h` is a proof that all elements of `s` are less than `n`. -/
def attachFin (s : Finset ℕ) {n : ℕ} (h : ∀ m ∈ s, m < n) : Finset (Fin n) :=
  ⟨s.1.pmap (fun a ha ↦ ⟨a, ha⟩) h, s.nodup.pmap fun _ _ _ _ ↦ Fin.val_eq_of_eq⟩

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