exists_fin_zero_pi — Mathlib

English

There exists an x of type Fin 0 → α such that P x if and only if P finZeroElim.

Русский

Существует x типа Fin 0 → α такое, что P x тогда и только тогда, когда P finZeroElim.

LaTeX

$$$(\\\\exists x, P x) \\\\Leftrightarrow P(\\\\mathrm{finZeroElim})$$$

Lean4

@[simp]
theorem exists_fin_zero_pi {α : Fin 0 → Sort*} {P : (∀ i, α i) → Prop} : (∃ x, P x) ↔ P finZeroElim :=
  ⟨fun ⟨x, h⟩ ↦ Subsingleton.elim x finZeroElim ▸ h, fun h ↦ ⟨_, h⟩⟩

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