exists_iff_castSucc — Mathlib

English

There exists i with P i iff P(last n) or there exists i in Fin n with P i.castSucc.

Русский

Существует i, такое что P i, если и только если P(last n) или существует i в Fin n с P(i.castSucc).

LaTeX

$$$\\\\exists i, P i \\\\iff P(\\\\mathrm{last} n) \\\\lor \\\\exists i : Fin n, P i.castSucc$$$

Lean4

theorem exists_iff_castSucc {P : Fin (n + 1) → Prop} : (∃ i, P i) ↔ P (last n) ∨ ∃ i : Fin n, P i.castSucc
    where
  mp := by
    rintro ⟨i, hi⟩
    cases i using lastCases with
    | last => exact .inl hi
    | cast _ => exact .inr ⟨_, hi⟩
  mpr := by rintro (h | ⟨i, hi⟩) <;> exact ⟨_, ‹_›⟩

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