Nuprl Definition : norm_subgrp

NormSubGrp{i}(g) ==  {s:|g| ⟶ ℙSubGrp of g ∧ norm_subset_p(g;s)} 

Definitions occuring in Statement :  norm_subset_p: norm_subset_p(g;s) subgrp_p: SubGrp of g grp_car: |g| prop: and: P ∧ Q set: {x:A| B[x]}  function: x:A ⟶ B[x]
Definitions occuring in definition :  set: {x:A| B[x]}  function: x:A ⟶ B[x] grp_car: |g| prop: and: P ∧ Q subgrp_p: SubGrp of g norm_subset_p: norm_subset_p(g;s)

NormSubGrp\{i\}(g)  ==    \{s:|g|  {}\mrightarrow{}  \mBbbP{}|  s  SubGrp  of  g  \mwedge{}  norm\_subset\_p(g;s)\} 

Date html generated: 2016_05_15-PM-00_08_55
Last ObjectModification: 2015_09_23-AM-06_24_23

Theory : groups_1

Home Index