Theorems · Theorem · group theory
AddSubmonoid.iSup_map_single_le
∀ {ι : Type u_4} {M : ι → Type u_5} [inst : (i : ι) → AddZeroClass (M i)] [inst_1 : DecidableEq ι] {I : Set ι}
{S : (i : ι) → AddSubmonoid (M i)}, ⨆ i, AddSubmonoid.map (AddMonoidHom.single M i) (S i) ≤ AddSubmonoid.pi I S- Cited by
- 1 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddZeroClassDecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- AddMonoidHomstatement · cited by 3,230
- iSupstatement · cited by 2,415
- AddZeroClassstatement and proof · cited by 1,237
- AddSubmonoidstatement and proof · cited by 1,178
- iSup_leproof · cited by 190
- AddSubmonoid.mapstatement · cited by 99
- AddSubmonoid.pistatement · cited by 20
- AddMonoidHom.singlestatement · cited by 19
- AddSubmonoid.map_le_iff_le_comapproof · cited by 3
- AddSubmonoid.le_comap_single_piproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- AddSubmonoid.iSup_map_singleproof · cited by 1