all_of_get — Mathlib

English

All_of_Get: For any p, s, and relation on get? results, if for all n x, get? n equals some x implies p x, then for any x, if there exists i with get? i = some x, then p x.

Русский

All_of_Get: для любых p, s и условия по get?, если для всех n x get? n = some x ⇒ p x, тогда для любого x, если существует i такое, что get? i = some x, тогда p x.

LaTeX

$$$(\forall n x, s.get? n = .some\ x \rightarrow p\ x) \rightarrow ∀ x, (Exists i, s.get? i = .some\ x) → p\ x$$$

Lean4

theorem all_of_get {p : α → Prop} {s : Seq α} (h : ∀ n x, s.get? n = .some x → p x) : ∀ x ∈ s, p x :=
  by
  simp only [mem_iff_exists_get?]
  grind

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