forall_and_right

Mathlib.Logic.Basic

URI: https://scilib.ai/kg/mathlib#forall_and_right

English

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

Русский

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

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru