widePushout_exists_rep' — Mathlib

English

A strengthening of exists rep: with a nonempty index set, some i and y always exist such that ι f i y = x.

Русский

Усиление существования представления: при непустом индексе найдется i и y такие, что ι f i y = x.

LaTeX

$$$\\exists i:\\\ \\alpha, \\exists y:ToType(X_i),\\ ι f i y = x$$$

Lean4

theorem widePushout_exists_rep' {B : C} {α : Type _} [Nonempty α] {X : α → C} (f : ∀ j : α, B ⟶ X j)
    [HasWidePushout.{v} B X f] [PreservesColimit (wideSpan B X f) (forget C)] (x : ToType (widePushout B X f)) :
    ∃ (i : α) (y : ToType (X i)), ι f i y = x :=
  by
  rcases Concrete.widePushout_exists_rep f x with (⟨y, rfl⟩ | ⟨i, y, rfl⟩)
  · inhabit α
    use default, f _ y
    simp only [← arrow_ι _ default, ConcreteCategory.comp_apply]
  · use i, y

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