nonempty_fiber_pi_of_nonempty_of_finite

English

If ι is finite and each X i has a nonempty fiber, then the fiber of the coproduct ∏ᶜ X also has a nonempty fiber.

Русский

Если индекс множество ι конечно, и каждого X_i имеет непустую фибру, то и фибра произведения соп coproduct ∏ᶜ X непустая.

LaTeX

$$$\operatorname{Nonempty}\bigl( F.obj (\prod^\mathrm{c} X) \bigr)$$$

Lean4

/-- If `X : ι → C` is a finite family of objects with non-empty fiber, then
also `∏ᶜ X` has non-empty fiber. -/
instance nonempty_fiber_pi_of_nonempty_of_finite {ι : Type*} [Finite ι] (X : ι → C) [∀ i, Nonempty (F.obj (X i))] :
    Nonempty (F.obj (∏ᶜ X)) := by
  cases nonempty_fintype ι
  let f (i : ι) : FintypeCat.{w} := F.obj (X i)
  let i : F.obj (∏ᶜ X) ≅ ∏ᶜ f := PreservesProduct.iso F _
  exact Nonempty.elim inferInstance fun x : (∏ᶜ f : FintypeCat.{w}) ↦ ⟨i.inv x⟩

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