imp_forall_iff_forall — Mathlib

English

Let A be a proposition and B : A → Prop. Then (A → ∀ h ∈ A, B h) is equivalent to ∀ h ∈ A, B h; i.e., if A is true, then every proof h of A satisfies B h.

Русский

Пусть A — proposition, B : A → Prop. Тогда (A → ∀ h ∈ A, B h) эквивалентно ∀ h ∈ A, B h; то есть если A истинна, то для каждого доказательства A выполняется B h.

LaTeX

$$$$\\left(A \\rightarrow \\forall h:A, B\\,h\\right) \\iff \\forall h:A, B\\,h.$$$$

Lean4

theorem imp_forall_iff_forall (A : Prop) (B : A → Prop) : (A → ∀ h : A, B h) ↔ ∀ h : A, B h := by
  by_cases h : A <;> simp [h]

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