exists_of — Mathlib

English

Every element of the direct limit arises from some component.

Русский

Каждый элемент прямого предела порождается компонентой.

LaTeX

$$$\\exists i,x\\; \\text{such that } z = \\mathrm{of}(i,x)$$$

Lean4

/-- Every element of the direct limit corresponds to some element in
some component of the directed system. -/
theorem exists_of (z : DirectLimit G f) : ∃ i x, of L ι G f i x = z :=
  ⟨z.out.1, z.out.2, by simp⟩

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