English
For a finite index set I, a family of subobjects P i of B indexed by I, and a morphism f: A → B, if there exists some i ∈ I with (P i) factoring f, then the supremum over all i of P i also factors through f.
Русский
Для конечного множества индексов I и семейства подпредметов P_i ⊆ B, если существует i ∈ I such that P_i факторизуется через f: A → B, то их супремум факторизуется через f.
LaTeX
$$$\exists i\in s\; (P(i).Factors f)\;\Rightarrow\; (s.sup P).Factors f$.$$
Lean4
theorem finset_sup_factors {I : Type*} {A B : C} {s : Finset I} {P : I → Subobject B} {f : A ⟶ B}
(h : ∃ i ∈ s, (P i).Factors f) : (s.sup P).Factors f := by
classical
revert h
induction s using Finset.induction_on with
| empty => rintro ⟨_, ⟨⟨⟩, _⟩⟩
| insert _ _ _ ih =>
rintro ⟨j, ⟨m, h⟩⟩
simp only [Finset.sup_insert]
simp only [Finset.mem_insert] at m
rcases m with (rfl | m)
· exact sup_factors_of_factors_left h
· exact sup_factors_of_factors_right (ih ⟨j, ⟨m, h⟩⟩)
