all_get — Mathlib

English

All_of_get: If for any n, x, s.get? n = Some x → p x, then for all x, if x ∈ s then p x.

Русский

All Get: если для любого n, x, s.get? n = Some x → p x, то для всех x, если x ∈ s, то p x.

LaTeX

$$$(\forall n x,\ s.get? n = .some\ x \rightarrow p\ x) \rightarrow \forall x\in s,\ p\ x$$$

Lean4

theorem all_get {p : α → Prop} {s : Seq α} (h : ∀ x ∈ s, p x) {n : ℕ} {x : α} (hx : s.get? n = .some x) : p x := by
  exact h _ (get?_mem hx)

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