Theorems · Theorem · Lie groups

Continuous.fun_sub

∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Sub G]
  [ContinuousSub G] {f g : X → G}, Continuous f → Continuous g → Continuous fun i => f i - g i

Eta-expanded form of Continuous.sub

Defined in

Mathlib.Topology.Algebra.Group.Defs

Cited by

53 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceSubContinuousSub