forall_mem_ofFn_iff — Mathlib

English

For any P : α → Prop, the statement ∀ l, P l is equivalent to ∀ n, ∀ f : Fin n → α, P (List.ofFn f).

Русский

Для любого P: α → Prop, утверждение ∀ l, P l эквивалентно ∀ n, ∀ f : Fin n → α, P (List.ofFn f).

LaTeX

$$$ \\forall P, \\ (\\forall l:\\List\\ α, P l) \\iff \\forall n (f : Fin n → α), P(\\operatorname{List.ofFn} f) $$$

Lean4

theorem forall_mem_ofFn_iff {n : ℕ} {f : Fin n → α} {P : α → Prop} : (∀ i ∈ ofFn f, P i) ↔ ∀ j : Fin n, P (f j) := by
  simp

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