induction — Mathlib

English

Two elements of the direct limit are represented by the same index i with possibly different representatives.

Русский

Два элемента прямого предела задаются одинаковым индексом i и разными представителями.

LaTeX

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

Lean4

@[elab_as_elim]
protected theorem induction {C : DirectLimit F f → Prop} (ih : ∀ i x, C ⟦⟨i, x⟩⟧) (x : DirectLimit F f) : C x :=
  Quotient.ind (fun _ ↦ ih _ _) x

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