English
Two parametrizations s.orderEmbOfFin h and s.orderEmbOfFin h' yield the same element on i and j only when i = j (as natural numbers).
Русский
Два параметрирования s.orderEmbOfFin h и s.orderEmbOfFin h' дают одинаковые значения на i и j тогда и только тогда, когда i = j (как натуральные числа).
LaTeX
$$s.orderEmbOfFin h i = s.orderEmbOfFin h' j \iff (i : \mathbb{N}) = (j : \mathbb{N})$$
Lean4
/-- An order embedding `f` from `Fin k` to a finset of cardinality `k` has to coincide with
the increasing bijection `orderEmbOfFin s h`. -/
theorem orderEmbOfFin_unique' {s : Finset α} {k : ℕ} (h : s.card = k) {f : Fin k ↪o α} (hfs : ∀ x, f x ∈ s) :
f = s.orderEmbOfFin h :=
RelEmbedding.ext <| funext_iff.1 <| orderEmbOfFin_unique h hfs f.strictMono
