English
If every F.obj j is finite, then each object (F.toPreimages s).obj j is finite.
Русский
Если каждый F.obj j конечен, то каждый объект (F.toPreimages s).obj j конечен.
LaTeX
$$$\forall j,\ Finite (F.obj j) \Rightarrow \ Finite((F.toPreimages s).obj j).$$$
Lean4
theorem isMittagLeffler_of_exists_finite_range (h : ∀ j : J, ∃ (i : _) (f : i ⟶ j), (range <| F.map f).Finite) :
F.IsMittagLeffler := by
intro j
obtain ⟨i, hi, hf⟩ := h j
obtain ⟨m, ⟨i, f, hm⟩, hmin⟩ :=
Finset.wellFoundedLT.wf.has_min {s : Finset (F.obj j) | ∃ (i : _) (f : i ⟶ j), ↑s = range (F.map f)}
⟨_, i, hi, hf.coe_toFinset⟩
refine
⟨i, f, fun k g => (directedOn_range.mp <| F.ranges_directed j).is_bot_of_is_min ⟨⟨i, f⟩, rfl⟩ ?_ _ ⟨⟨k, g⟩, rfl⟩⟩
rintro _ ⟨⟨k', g'⟩, rfl⟩ hl
refine (eq_of_le_of_not_lt hl ?_).ge
have := hmin _ ⟨k', g', (m.finite_toSet.subset <| hm.substr hl).coe_toFinset⟩
rwa [Finset.lt_iff_ssubset, ← Finset.coe_ssubset, Set.Finite.coe_toFinset, hm] at this
