all_cons — Mathlib

English

All_of_get: If for any h and s, h implies p for any element retrieved by get?, then for every x in s, p x.

Русский

All_of_get: если для любого h и s, любой x, извлекаемый через get? удовлетворяет p, то для всех x ∈ s верно p x.

LaTeX

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

Lean4

theorem all_cons {p : α → Prop} {hd : α} {tl : Seq α} (h_hd : p hd) (h_tl : ∀ x ∈ tl, p x) :
    (∀ x ∈ (cons hd tl), p x) := by
  simp only [mem_cons_iff, forall_eq_or_imp] at *
  exact ⟨h_hd, h_tl⟩

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