forall_eq_apply_imp_iff' — Mathlib

English

For f: α → β and predicate p on β, the statement (for all a,b, b = f a → p b) is equivalent to (for all a, p (f a)).

Русский

Для f: α → β и предиката p на β: (для всех a,b, b = f a → p b) эквивалентно (для всех a, p(f(a))).

LaTeX

$$$$\\forall a\\,\\forall b,\\; b = f(a) \\to p(b) \\leftrightarrow \\forall a, p(f(a)).$$$$

Lean4

theorem forall_eq_apply_imp_iff' {f : α → β} {p : β → Prop} : (∀ a b, b = f a → p b) ↔ ∀ a, p (f a) := by simp

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