forall_apply_eq_imp_iff' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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