exists_fin_succ_pi — Mathlib

English

There exists an x with property P iff there exist a and v with P (Fin.cons a v).

Русский

Существует x со свойством P тогда и только тогда, когда существуют a и v с P(Fin.cons a v).

LaTeX

$$$\\\\exists x, P x \\\\Leftrightarrow \\\\exists a,v, P(\\\\mathrm{Fin.cons} a v)$$$

Lean4

theorem exists_fin_succ_pi {P : (∀ i, α i) → Prop} : (∃ x, P x) ↔ ∃ a v, P (Fin.cons a v) :=
  ⟨fun ⟨x, h⟩ ↦ ⟨x 0, tail x, (cons_self_tail x).symm ▸ h⟩, fun ⟨_, _, h⟩ ↦ ⟨_, h⟩⟩

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