forall — Mathlib

English

The universal quantification over a discrete type is equivalent to the universal quantification over the underlying type.

Русский

Обобщение по дискретному типу эквивалентно обобщению по базовому типу.

LaTeX

$$$\\forall a:\\mathrm{Discrete}(\\alpha),\\; p(a) \\quad\\Leftrightarrow\\quad \\forall a'\\in\\alpha,\\; p(\\langle a'\\rangle)$$$

Lean4

@[simp]
theorem «forall» {α : Type*} {p : Discrete α → Prop} : (∀ (a : Discrete α), p a) ↔ ∀ (a' : α), p ⟨a'⟩ :=
  by
  rw [iff_iff_eq, discreteEquiv.forall_congr_left]
  simp [discreteEquiv]

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