English
If f is an increasing bijection from Fin k into α with image in s, then f equals s.orderEmbOfFin h.
Русский
Если f является возрастющим биекциям из Fin k в α с образом в s, то f = s.orderEmbOfFin h.
LaTeX
$$f = s.orderEmbOfFin h$$
Lean4
/-- Any increasing map `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 → α} (hfs : ∀ x, f x ∈ s)
(hmono : StrictMono f) : f = s.orderEmbOfFin h :=
by
rw [← hmono.range_inj (s.orderEmbOfFin h).strictMono, range_orderEmbOfFin, ← Set.image_univ, ← coe_univ, ← coe_image,
coe_inj]
refine eq_of_subset_of_card_le (fun x hx => ?_) ?_
· rcases mem_image.1 hx with ⟨x, _, rfl⟩
exact hfs x
· rw [h, card_image_of_injective _ hmono.injective, card_univ, Fintype.card_fin]
