imp_forall_iff — Mathlib

English

Let α be a type, p a proposition, q : α → Prop. Then (p → ∀ x, q x) is equivalent to ∀ x, p → q x.

Русский

Пусть α — множество, p — proposition, q: α → Prop. Тогда (p → ∀ x, q x) эквивалентно ∀ x, p → q x.

LaTeX

$$$$\\left(p \\rightarrow \\forall x, q\\,x\\right) \\Longleftrightarrow \\forall x, p \\rightarrow q\\,x.$$$$

Lean4

/-- We intentionally restrict the type of `α` in this lemma so that this is a safer to use in simp
than `forall_swap`. -/
theorem imp_forall_iff {α : Type*} {p : Prop} {q : α → Prop} : (p → ∀ x, q x) ↔ ∀ x, p → q x :=
  forall_swap

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