English
Let D be the direct limit of a directed system (F_i) with transition maps f_i_j. If C is a ternary relation on elements of D such that C holds for any triple coming from a single index i (i.e., for all i and x,y,z in F_i, C(ι_i(x), ι_i(y), ι_i(z)) holds), then C holds for all triples of elements of D. Equivalently, any property that is checked on representatives from a single stage is forced to hold for all elements of the direct limit when the representatives are compatible.
Русский
Пусть D = lim→ F_i. Пусть C — бинарная отношение над тройками элементов D. Если для каждого i и любых x,y,z∈F_i выполняется C(ι_i(x), ι_i(y), ι_i(z)), то C выполняется для любых a,b,c∈D. То есть любая свойство, проверяемое на представителях на одном этапе, переносится на весь прямой предел
LaTeX
$$$\\forall C:\\mathrm{DirectLimit}(F,f)\\to\\mathrm{DirectLimit}(F,f)\\to\\mathrm{DirectLimit}(F,f)\\to\\mathrm{Prop},\\;\\Big(\\forall i:\\iota_i\\colon F_i\\to \\mathrm{DirectLimit}(F,f),\\;\\forall x,y,z\\in F_i,\\; C(\\iota_i(x),\\iota_i(y),\\iota_i(z))\\Big)\\;\\Rightarrow\\; \\forall a,b,c\\in \\mathrm{DirectLimit}(F,f),\\; C(a,b,c) \\)$$
Lean4
@[elab_as_elim]
protected theorem induction₃ {C : DirectLimit F f → DirectLimit F f → DirectLimit F f → Prop}
(ih : ∀ i x y z, C ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧ ⟦⟨i, z⟩⟧) (x y z : DirectLimit F f) : C x y z := by
obtain ⟨_, _, _, _, rfl, rfl, rfl⟩ := exists_eq_mk₃ f x y z; apply ih
