forall_or_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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