forall — Mathlib

English

A property P holds for all subgroups of H if and only if P holds for all subgroups of G contained in H, transported via subgroupOf.

Русский

Свойство P выполняется для всех подгрупп H тогда и только тогда, когда P выполняется для всех подгрупп G, вложенных в H, через отображение subgroupOf.

LaTeX

$$\\forall H', P(H') \\iff \\forall H' ≤ H, P(H'.subgroupOf H)$$

Lean4

@[to_additive]
protected theorem «forall» {H : Subgroup G} {P : Subgroup H → Prop} :
    (∀ H' : Subgroup H, P H') ↔ (∀ H' ≤ H, P (H'.subgroupOf H)) := by simp [(MapSubtype.orderIso H).forall_congr_left]

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