exists_of₂ — Mathlib

English

Induction principle: to prove a property for all elements of the direct limit, it suffices to prove it for images of elements in each component.

Русский

Принцип индукции по прямому пределу: для доказательства свойства для всех элементов достаточно доказать его для образов элементов в каждой компоненте.

LaTeX

$$$\\forall z, \\mathrm{DirectLimit}.induction\_on(z)\\; (P(z) )$$$

Lean4

theorem exists_of₂ [Nonempty ι] [IsDirected ι (· ≤ ·)] (z w : DirectLimit G f) :
    ∃ i x y, of R ι G f i x = z ∧ of R ι G f i y = w :=
  have ⟨i, x, hx⟩ := exists_of z
  have ⟨j, y, hy⟩ := exists_of w
  have ⟨k, hik, hjk⟩ := exists_ge_ge i j
  ⟨k, f i k hik x, f j k hjk y, by rw [of_f, hx], by rw [of_f, hy]⟩

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