English
If J is nonempty and F.sections is finite, there exists an index j such that for every i and every f : i ⟶ j, the map F.map f is injective.
Русский
Если множество объектов J непусто и F.sections конечен, существует такой индекс j, что для каждого i и каждого f : i ⟶ j отображение F.map f инъективно.
LaTeX
$$$\exists j,\forall i,\forall f : i \to j, \ F.map f\text{ injective}.$$$
Lean4
theorem eventually_injective [Nonempty J] [Finite F.sections] : ∃ j, ∀ (i) (f : i ⟶ j), (F.map f).Injective :=
by
haveI : ∀ j, Fintype (F.obj j) := fun j => Fintype.ofFinite (F.obj j)
haveI : Fintype F.sections := Fintype.ofFinite F.sections
have card_le : ∀ j, Fintype.card (F.obj j) ≤ Fintype.card F.sections := fun j =>
Fintype.card_le_of_surjective _ (F.eval_section_surjective_of_surjective Fsur j)
let fn j := Fintype.card F.sections - Fintype.card (F.obj j)
refine
⟨fn.argmin, fun i f =>
((Fintype.bijective_iff_surjective_and_card _).2
⟨Fsur f, le_antisymm ?_ (Fintype.card_le_of_surjective _ <| Fsur f)⟩).1⟩
rw [← Nat.sub_le_sub_iff_left (card_le i)]
apply fn.argmin_le
