forall_iff — Mathlib

English

For any predicate P on Under X, (for all Y, P(Y)) is equivalent to (for all Y and f: X ⟶ Y, P(Under.mk f)).

Русский

Для любого предиката P на Under X имеем: (для всех Y, P(Y)) эквивалентно (для всех Y и f: X ⟶ Y, P(Under.mk f)).

LaTeX

$$ (P : Under X → Prop) : (∀ Y, P Y) ⇔ (∀ (Y) (f : X ⟶ Y), P (Under.mk f))$$

Lean4

theorem forall_iff (P : Under X → Prop) : (∀ Y, P Y) ↔ (∀ (Y) (f : X ⟶ Y), P (.mk f)) := by aesop

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