Theorems · Definition · Lie groups

addHomOfMemClosureRangeCoe

{M₁ : Type u_6} →
  {M₂ : Type u_7} →
    [inst : TopologicalSpace M₂] →
      [T2Space M₂] →
        [inst_2 : Add M₁] →
          [inst_3 : Add M₂] →
            [ContinuousAdd M₂] →
              {F : Type u_8} →
                [inst_5 : FunLike F M₁ M₂] →
                  [AddHomClass F M₁ M₂] → (f : M₁ → M₂) → f ∈ closure (Set.range fun f x => f x) → M₁ →ₙ+ M₂

Construct a bundled additive semigroup homomorphism M₁ →ₙ+ M₂ from a function f and a proof that it belongs to the closure of the range of the coercion from M₁ →ₙ+ M₂ (or another type of bundled homomorphisms that has an AddHomClass instance) to M₁ → M₂.

Defined in

Mathlib.Topology.Algebra.Monoid

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceT2SpaceAddAddContinuousAddFunLikeAddHomClass