forall_mem_range — Mathlib

English

Let p be a predicate on α. Then p holds for every element of the image of f if and only if p holds for every value f(i).

Русский

Пусть p — предикат на α. Тогда p(a) верно для каждого элемента a из образа f тогда и только тогда, когда p(f(i)) верно для всех i.

LaTeX

$$$ ( \\forall a \\in \\operatorname{range} f,\ p(a)) \\;\\Leftrightarrow\\; \\forall i\\, p(f(i)) $$$

Lean4

theorem forall_mem_range {p : α → Prop} : (∀ a ∈ range f, p a) ↔ ∀ i, p (f i) := by simp

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