forall₂_and — Mathlib

English

The universal quantification commutes with conjunction: for all x, P x h and Q x h hold iff (for all x h, P x h) and (for all x h, Q x h).

Русский

Все x и h удовлетворяют P x h и Q x h тогда и только тогда, когда выполняются одновременно все x,h P x h и все x,h Q x h.

LaTeX

$$$\bigl(\forall x,h\, (P(x,h)\land Q(x,h))\bigr) \iff \bigl(\forall x,h\, P(x,h)\bigr) \land \bigl(\forall x,h\, Q(x,h)\bigr).$$$

Lean4

theorem forall₂_and : (∀ x h, P x h ∧ Q x h) ↔ (∀ x h, P x h) ∧ ∀ x h, Q x h :=
  Iff.trans (forall_congr' fun _ ↦ forall_and) forall_and

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