forall_mem_eraseNone — Mathlib

English

For any finite s of Option α and predicate p on Option α, the universal claim over eraseNone s is equivalent to p holding for none and p for some elements in s.

Русский

Для любого s ∈ Finset(Option α) и предиката p, всеобщее утверждение над eraseNone s эквивалентно p none и p (Some a) для всех a∈s.

LaTeX

$$$(\\forall o \\in \\text{eraseNone}(s), p(o)) \\iff (p(\\text{none}) \\land \\forall a \\in s, p(\\text{some}(a))).$$$

Lean4

theorem forall_mem_eraseNone {s : Finset (Option α)} {p : Option α → Prop} :
    (∀ a ∈ eraseNone s, p a) ↔ ∀ a : α, (a : Option α) ∈ s → p a := by simp

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