forall_and_left — Mathlib

English

If α is nonempty, then for q and p, (∀ x, q ∧ p x) is equivalent to (q ∧ ∀ x, p x).

Русский

Если множество α непусто, то (∀ x, q ∧ p(x)) эквивалентно (q ∧ ∀ x, p(x)).

LaTeX

$$$\forall x\in\mathbb{A}\, (q \land p(x)) \;\Leftrightarrow\; (q \land \forall x\, p(x)).$$$

Lean4

theorem forall_and_left [Nonempty α] (q : Prop) (p : α → Prop) : (∀ x, q ∧ p x) ↔ (q ∧ ∀ x, p x) := by
  rw [forall_and, forall_const]

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