exists_eq_mk₃ — Mathlib

English

Two direct limit elements correspond to representatives with a common index.

Русский

Два элемента прямого предела соответствуют представителям с общим индексом.

LaTeX

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

Lean4

theorem exists_eq_mk₃ (w u v : DirectLimit F f) : ∃ i x y z, w = ⟦⟨i, x⟩⟧ ∧ u = ⟦⟨i, y⟩⟧ ∧ v = ⟦⟨i, z⟩⟧ :=
  w.inductionOn₃ u v fun x y z ↦
    have ⟨i, hxi, hyi, hzi⟩ := directed_of₃ (· ≤ ·) x.1 y.1 z.1
    ⟨i, _, _, _, eq_of_le x i hxi, eq_of_le y i hyi, eq_of_le z i hzi⟩

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