forall_or_right — Mathlib

English

Let α be a type, p: α → Prop and q a Prop. Then (∀ x, p x ∨ q) ↔ (∀ x, p x) ∨ q, under classical logic.

Русский

Пусть α — множество, p : α → Prop и q — Prop. При классической логике выполняется (∀ x, p x ∨ q) ↔ (∀ x, p x) ∨ q.

LaTeX

$$$(\forall x, p x \lor q) \iff (\forall x, p x) \lor q$$$

Lean4

theorem forall_or_right {q} {p : α → Prop} : (∀ x, p x ∨ q) ↔ (∀ x, p x) ∨ q :=
  open scoped Classical in Decidable.forall_or_right

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