isMittagLeffler_of_surjective — Mathlib

English

If every map F.map f is surjective, then F is Mittag-Leffler.

Русский

Если каждый отображение F.map f сюръективно, то F удовлетворяет условию Mittag-Leffler.

LaTeX

$$$\big( \forall i, j, \ f : i \to j, \ F.map f \text{ is surjective} \big) \Rightarrow FIsMittagLeffler.$$$

Lean4

theorem isMittagLeffler_of_surjective (h : ∀ ⦃i j : J⦄ (f : i ⟶ j), (F.map f).Surjective) : F.IsMittagLeffler :=
  fun j => ⟨j, 𝟙 j, fun k g => by rw [map_id, types_id, range_id, (h g).range_eq]⟩

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