Theorems · Theorem · general topology

Filter.Germ.value_smul

∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X} {α : Type u_4} {β : Type u_5} [inst_1 : SMul α β]
  (φ : (nhds x).Germ α) (ψ : (nhds x).Germ β), (φ • ψ).value = φ.value • ψ.value

Defined in

Mathlib.Topology.Germ

Cited by

0 results in Mathlib

Foundations

Depth 63 from the axioms · uses propext, Quot.sound

Assumes

TopologicalSpaceSMul