induction₂ — Mathlib

English

There exist i,x,y,z giving three elements of the direct limit with a common index.

Русский

Существуют i,x,y,z такие, что три элемента прямого предела имеют общий индекс.

LaTeX

$$$\exists i\,\exists x\,\exists y\exists z, w=⟦⟨i,x⟩⟧, u=⟦⟨i,y⟩⟧, v=⟦⟨i,z⟩⟧.$$$

Lean4

@[elab_as_elim]
protected theorem induction₂ {C : DirectLimit F f → DirectLimit F f → Prop} (ih : ∀ i x y, C ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧)
    (x y : DirectLimit F f) : C x y := by obtain ⟨_, _, _, rfl, rfl⟩ := exists_eq_mk₂ f x y; apply ih

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