Theorems · Theorem · Lie groups

AddMonoidHom.isStrictMap_prodMap_iff

∀ {G : Type u_1} {H : Type u_2} {G' : Type u_3} {H' : Type u_4} [inst : AddGroup G'] [inst_1 : AddGroup H']
  [inst_2 : AddGroup G] [inst_3 : AddGroup H] {f : G →+ H} {g : G' →+ H'} [inst_4 : TopologicalSpace G]
  [inst_5 : TopologicalSpace H] [IsTopologicalAddGroup G] [inst_7 : TopologicalSpace G'] [IsTopologicalAddGroup G']
  [inst_9 : TopologicalSpace H'],
  Topology.IsStrictMap ⇑(f.prodMap g) ↔ Topology.IsStrictMap ⇑f ∧ Topology.IsStrictMap ⇑g

The product (in the sense of AddMonoidHom.prodMap) of additive group homomorphisms is strict if and only if both homomorphisms are strict.

Defined in

Mathlib.Topology.Maps.Strict.Group

Cited by

2 results in Mathlib

Foundations

Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroupAddGroupAddGroupAddGroupTopologicalSpaceTopologicalSpaceIsTopologicalAddGroupTopologicalSpaceIsTopologicalAddGroupTopologicalSpace