forall_mem_map — Mathlib

English

For any f, o, p, the predicate p holds for all elements of o.map f iff it holds for all f-applied elements of o.

Русский

Для любой функции f, множества o и предиката p верно: p ко всем элементам o.map f тогда и только тогда, когда p выполняется для всех элементов o после применения f.

LaTeX

$$$$ (\forall y \in o.map f, p(y)) \iff (\forall x \in o, p(f(x))). $$$$

Lean4

theorem forall_mem_map {f : α → β} {o : Option α} {p : β → Prop} : (∀ y ∈ o.map f, p y) ↔ ∀ x ∈ o, p (f x) := by simp

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