forall₂_or_left — Mathlib

English

The statement (∀ x, p x ∨ q x → r x) is equivalent to (∀ x, p x → r x) ∧ ∀ x, q x → r x.

Русский

Утверждение (∀ x, p x ∨ q x → r x) эквивалентно (∀ x, p x → r x) и ∀ x, q x → r x.

LaTeX

$$$\bigl(\forall x,\, p(x) \lor q(x) \to r(x)\bigr) \iff \bigl(\forall x,\, p(x)\to r(x)\bigr) \land \forall x,\, q(x)\to r(x).$$$

Lean4

theorem forall₂_or_left : (∀ x, p x ∨ q x → r x) ↔ (∀ x, p x → r x) ∧ ∀ x, q x → r x :=
  Iff.trans (forall_congr' fun _ ↦ or_imp) forall_and

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