induction_on — Mathlib

English

There exist indices i, x, y such that both z and w are represented by the same index i in the direct limit.

Русский

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

LaTeX

$$$\\exists i\\; \\exists x\\; \\exists y, \\; \\text{of}(i,x)=z \\land \\text{of}(i,y)=w$$$

Lean4

@[elab_as_elim]
protected theorem induction_on [Nonempty ι] [IsDirected ι (· ≤ ·)] {C : DirectLimit G f → Prop} (z : DirectLimit G f)
    (ih : ∀ i x, C (of R ι G f i x)) : C z :=
  let ⟨i, x, h⟩ := exists_of z
  h ▸ ih i x

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