Theorems · Theorem · general topology
RestrictedProduct.one_apply
∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
{B : (i : ι) → S i} [inst_1 : (i : ι) → One (R i)] [inst_2 : ∀ (i : ι), OneMemClass (S i) (R i)] (i : ι), 1 i = 1- Cited by
- 0 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses no axioms
- Assumes
- SetLikeOneOneMemClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- SetLike.coestatement · cited by 8,199
- Filterstatement and proof · cited by 8,121
- SetLikestatement and proof · cited by 1,084
- RestrictedProductstatement · cited by 117
- OneMemClassstatement and proof · cited by 21
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.