toEventualRanges_finite — Mathlib

English

If F is Mittag-Leffler, then for any f : j ⟶ i, the eventual range at i equals the image of F.map f on the eventual range at j.

Русский

Если F удовлетворяет Mittag-Leffler, тогда F.eventualRange(i) равно образу F.map f на F.eventualRange(j).

LaTeX

$$$FIsMittagLeffler \Rightarrow F.eventualRange(i) = \mathrm{image}(F.map f)(F.eventualRange(j)).$$$

Lean4

instance toEventualRanges_finite [∀ j, Finite (F.obj j)] : ∀ j, Finite (F.toEventualRanges.obj j) := fun _ =>
  Subtype.finite

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