Theorems · Definition · general topology

RestrictedProduct.mulSingle

{ι : Type u_1} →
  {S : ι → Type u_3} →
    {G : ι → Type u_4} →
      [inst : (i : ι) → SetLike (S i) (G i)] →
        (A : (i : ι) → S i) →
          [DecidableEq ι] →
            [inst_2 : (i : ι) → One (G i)] →
              [∀ (i : ι), OneMemClass (S i) (G i)] →
                (i : ι) → G i → RestrictedProduct (fun i => G i) (fun i => ↑(A i)) Filter.cofinite

The function supported at i, with value x there, and 1 elsewhere.

Defined in

Mathlib.Topology.Algebra.RestrictedProduct.Basic

Cited by

16 results in Mathlib

Foundations

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

Assumes

SetLikeDecidableEqOneOneMemClass