forall_associated — Mathlib

English

Let p be a predicate on the set of associate classes of a monoid M. Then p holds for every class if and only if p holds for the class of a for every a in M.

Русский

Пусть p — свойство на множестве классов ассоциаций моноида M. Тогда выполняется: свойство p верно для каждого класса если и только если для каждого a ∈ M верно p(Associates.mk(a)).

LaTeX

$$$ (\forall \alpha : \operatorname{Associates}(M), p(\alpha)) \iff (\forall a : M, p(\operatorname{Associates.mk} a)) $$$

Lean4

theorem forall_associated [Monoid M] {p : Associates M → Prop} : (∀ a, p a) ↔ ∀ a, p (Associates.mk a) :=
  Iff.intro (fun h _ => h _) fun h a => Quotient.inductionOn a h

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