English
If p is a GroupSeminorm on E and f: F →* E is a monoid homomorphism, then the composition p ∘ f defines a GroupSeminorm on F.
Русский
Если p — GroupSeminorm на E и f: F →* E — моноидный гомоморфизм, то композиция p ∘ f задаёт GroupSeminorm на F.
LaTeX
$$$\forall f:\, F \to^* E,\ \exists p': F \to E\, (p' = p \circ f) \Rightarrow p' \text{ является GroupSeminorm на } F.$$$
Lean4
/-- Composition of a group seminorm with a monoid homomorphism as a group seminorm. -/
@[to_additive /-- Composition of an additive group seminorm with an additive monoid homomorphism as
an additive group seminorm. -/
]
def comp (p : GroupSeminorm E) (f : F →* E) : GroupSeminorm F
where
toFun x := p (f x)
map_one' := by simp_rw [f.map_one, map_one_eq_zero p]
mul_le' _ _ := (congr_arg p <| f.map_mul _ _).trans_le <| map_mul_le_add p _ _
inv' x := by simp_rw [map_inv, map_inv_eq_map p]
