Theorems · Definition · Lie groups

RestrictedProduct.mkUnit

{ι : Type u_1} →
  {R : ι → Type u_2} →
    [inst : (i : ι) → Monoid (R i)] →
      {S : ι → Type u_3} →
        [inst_1 : (i : ι) → SetLike (S i) (R i)] →
          [inst_2 : ∀ (i : ι), SubmonoidClass (S i) (R i)] →
            {B : (i : ι) → S i} →
              {𝓕 : Filter ι} →
                (x : (i : ι) → (R i)ˣ) →
                  (∀ᶠ (i : ι) in 𝓕, x i ∈ (Submonoid.ofClass (B i)).units) →
                    (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)ˣ

Constructs a unit in a restricted product Πʳ i, [R i, B i]_[𝓕] given an element x of the usual product and the condition that x is eventually in the units of B i along 𝓕.

Defined in

Mathlib.Topology.Algebra.RestrictedProduct.Units

Cited by

0 results in Mathlib

Foundations

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

Assumes

MonoidSetLikeSubmonoidClass