ind — Mathlib

English

For any predicate β on Trunc α, if β(mk a) holds for every a in α, then β(q) holds for every q in Trunc α.

Русский

Для любого предиката β на Trunc α, если β(mk a) истинно для каждого a ∈ α, то β(q) истинно для каждого q ∈ Trunc α.

LaTeX

$$$\\big( \\forall a:\\, \\alpha,\\beta(\\mathrm{mk}\\,a) \\big) \\Rightarrow \\forall q:\\, \\mathrm{Trunc}(\\alpha),\\ \\beta(q)$$$

Lean4

theorem ind {β : Trunc α → Prop} : (∀ a : α, β (mk a)) → ∀ q : Trunc α, β q :=
  Quot.ind

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