forall_mk — Mathlib

English

A property on α / s holds for all quotient elements if and only if it holds for all representatives in α.

Русский

Свойство на α / s выполняется для всех элементов косета тогда и только тогда, когда выполняется для всех представителей в α.

LaTeX

$${C: α / s → Prop} : (∀ x, C x) ↔ ∀ x, C (QuotientGroup.mk x)$$

Lean4

@[to_additive]
theorem forall_mk {C : α ⧸ s → Prop} : (∀ x : α ⧸ s, C x) ↔ ∀ x : α, C x :=
  mk_surjective.forall

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