forall_or_of_or_forall — Mathlib

English

If h is either b or ∀ x, p x, then for every x, b implies (p x) or b; more precisely, from Or b (Forall x, p x) deduce ∀ x, Or b (p x).

Русский

Если h имеет вид: либо b, либо ∀ x, p x, тогда для каждого x верно: либо b, либо p(x).

LaTeX

$$$$\\text{Or}\\, b\, (\\forall x, p x) \\to \\forall x, \\; \\text{Or}\\, b\\,(p x).$$$$

Lean4

theorem forall_or_of_or_forall {α : Sort*} {p : α → Prop} {b : Prop} (h : b ∨ ∀ x, p x) (x : α) : b ∨ p x :=
  h.imp_right fun h₂ ↦ h₂ x

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