forall_or_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

protected theorem forall_or_left {q : Prop} {p : α → Prop} [Decidable q] : (∀ x, q ∨ p x) ↔ q ∨ ∀ x, p x :=
  ⟨fun h ↦ if hq : q then Or.inl hq else Or.inr fun x ↦ (h x).resolve_left hq, forall_or_of_or_forall⟩

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