forall_or_right — Mathlib

English

Let α be a type, p: α → Prop and q a Prop. If q is decidable, then (∀ x, p x ∨ q) ↔ (∀ x, p x) ∨ q.

Русский

Пусть α — множество, p : α → Prop и q — Prop. Пусть q разрешимо. Тогда (∀ x, p x ∨ q) ↔ (∀ x, p x) ∨ q.

LaTeX

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

Lean4

protected theorem forall_or_right {q} {p : α → Prop} [Decidable q] : (∀ x, p x ∨ q) ↔ (∀ x, p x) ∨ q := by
  simp [or_comm, Decidable.forall_or_left]

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