forall_isConj — Mathlib

English

For any predicate p on ConjClasses α, (for all a, p(a)) holds if and only if (for all a ∈ α, p(mk a)) holds.

Русский

Для любого предиката p на ConjClasses α выполняется эквивалентно: (для всех a, p(a)) эквивалентно (для всех a в α, p(mk(a))).

LaTeX

$$$( \forall A : ConjClasses \alpha, p(A) ) \iff ( \forall a : \alpha, p( ConjClasses.mk(a) ) )$$$

Lean4

theorem forall_isConj {p : ConjClasses α → Prop} : (∀ a, p a) ↔ ∀ a, p (ConjClasses.mk a) :=
  Iff.intro (fun h _ => h _) fun h a => Quotient.inductionOn a h

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