exists_eq_mk₂ — Mathlib

English

Three elements of the direct limit can be simultaneously represented by a single index i and elements x,y,z.

Русский

Три элемента прямого предела могут быть одновременно представлены одним индексом i и элементами x,y,z.

LaTeX

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

Lean4

theorem exists_eq_mk₂ (z w : DirectLimit F f) : ∃ i x y, z = ⟦⟨i, x⟩⟧ ∧ w = ⟦⟨i, y⟩⟧ :=
  z.inductionOn₂ w fun x y ↦
    have ⟨i, hxi, hyi⟩ := exists_ge_ge x.1 y.1
    ⟨i, _, _, eq_of_le x i hxi, eq_of_le y i hyi⟩

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