toEventualRanges_nonempty — Mathlib

English

If F is Mittag-Leffler and each F.obj j is nonempty, then each eventual range F.toEventualRanges.obj j is also nonempty.

Русский

Если F удовлетворяет Миттаг-Леффлеру и каждый F.obj j непуст, то и предельные диапазоны F.toEventualRanges.obj j непусты.

LaTeX

$$$ \text{Nonempty}(F.toEventualRanges.obj j)$$$

Lean4

/-- If `F` is nonempty at each index and Mittag-Leffler, then so is `F.toEventualRanges`. -/
theorem toEventualRanges_nonempty (h : F.IsMittagLeffler) [∀ j : J, Nonempty (F.obj j)] (j : J) :
    Nonempty (F.toEventualRanges.obj j) :=
  by
  let ⟨i, f, h⟩ := F.isMittagLeffler_iff_eventualRange.1 h j
  rw [toEventualRanges_obj, h]
  infer_instance

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